The sandwich theorem

Introduction

The sandwich theorem, or squeeze theorem, for real sequences is the statement that if $(a_n)$, $(b_n)$, and $(c_n)$ are three real-valued sequences satisfying $a_n≤ b_n≤ c_n$ for all $n$, and if furthermore $a_n→ℓ$ and $c_n→ℓ$, then $b_n→ℓ$. The idea of the proof is straightforward -- if we want to ensure that $|b_n-ℓ|<ε$ then it suffices to show that $|a_n-ℓ|<ε$ and $|c_n-ℓ|<ε$, and we can choose $N$ large enough such that this is true for all $n≥ N$.

Lemma
If $(a_n)$, $(b_n)$, and $(c_n)$ are three real-valued sequences satisfying $a_n ≤ b_n ≤ c_n$ for all $n$, and if furthermore $a_n→ℓ$ and $c_n→ℓ$, then $b_n→ℓ$.
theorem sandwich (a b c :   )
  (l : ) (ha : is_limit a l) (hc : is_limit c l) 
  (hab :  n, a n  b n) (hbc :  n, b n  c n) : is_limit b l :=
Proof
We need to show that for all $ε>0$ there exists $N$ such that $n≥N$ implies $|b_n-ℓ|<ε$. So choose ε > 0.
  intros ε ,
a b c :   ,
l : ,
ha : is_limit a l,
hc : is_limit c l,
hab :  (n : ), a n  b n,
hbc :  (n : ), b n  c n
 is_limit b l
a b c :   ,
l : ,
ha : is_limit a l,
hc : is_limit c l,
hab :  (n : ), a n  b n,
hbc :  (n : ), b n  c n,
ε : ,
 : ε > 0
  (N : ),  (n : ), n  N  |b n - l| < ε
We now need an $N$. As usual it is the max of two other N's, one coming from $(a_n)$ and one from $(c_n)$. Choose $N_a$ and $N_c$ such that $|a_n - l| < ε$ for $n ≥ N_a$ and $|c_n - l| < ε$ for $n ≥ N_c$.
  cases ha ε  with Na Ha,
a b c :   ,
l : ,
ha : is_limit a l,
hc : is_limit c l,
hab :  (n : ), a n  b n,
hbc :  (n : ), b n  c n,
ε : ,
 : ε > 0
  (N : ),  (n : ), n  N  |b n - l| < ε
a b c :   ,
l : ,
ha : is_limit a l,
hc : is_limit c l,
hab :  (n : ), a n  b n,
hbc :  (n : ), b n  c n,
ε : ,
 : ε > 0,
Na : ,
Ha :  (n : ), n  Na  |a n - l| < ε
  (N : ),  (n : ), n  N  |b n - l| < ε
  cases hc ε  with Nc Hc,
a b c :   ,
l : ,
ha : is_limit a l,
hc : is_limit c l,
hab :  (n : ), a n  b n,
hbc :  (n : ), b n  c n,
ε : ,
 : ε > 0,
Na : ,
Ha :  (n : ), n  Na  |a n - l| < ε
  (N : ),  (n : ), n  N  |b n - l| < ε
a b c :   ,
l : ,
ha : is_limit a l,
hc : is_limit c l,
hab :  (n : ), a n  b n,
hbc :  (n : ), b n  c n,
ε : ,
 : ε > 0,
Na : ,
Ha :  (n : ), n  Na  |a n - l| < ε,
Nc : ,
Hc :  (n : ), n  Nc  |c n - l| < ε
  (N : ),  (n : ), n  N  |b n - l| < ε
Now let $N$ be the max of $N_a$ and $N_c$; we claim that this works.
  let N := max Na Nc,
a b c :   ,
l : ,
ha : is_limit a l,
hc : is_limit c l,
hab :  (n : ), a n  b n,
hbc :  (n : ), b n  c n,
ε : ,
 : ε > 0,
Na : ,
Ha :  (n : ), n  Na  |a n - l| < ε,
Nc : ,
Hc :  (n : ), n  Nc  |c n - l| < ε
  (N : ),  (n : ), n  N  |b n - l| < ε
a b c :   ,
l : ,
ha : is_limit a l,
hc : is_limit c l,
hab :  (n : ), a n  b n,
hbc :  (n : ), b n  c n,
ε : ,
 : ε > 0,
Na : ,
Ha :  (n : ), n  Na  |a n - l| < ε,
Nc : ,
Hc :  (n : ), n  Nc  |c n - l| < ε,
N :  := max Na Nc
  (N : ),  (n : ), n  N  |b n - l| < ε
  use N,
a b c :   ,
l : ,
ha : is_limit a l,
hc : is_limit c l,
hab :  (n : ), a n  b n,
hbc :  (n : ), b n  c n,
ε : ,
 : ε > 0,
Na : ,
Ha :  (n : ), n  Na  |a n - l| < ε,
Nc : ,
Hc :  (n : ), n  Nc  |c n - l| < ε,
N :  := max Na Nc
  (N : ),  (n : ), n  N  |b n - l| < ε
a b c :   ,
l : ,
ha : is_limit a l,
hc : is_limit c l,
hab :  (n : ), a n  b n,
hbc :  (n : ), b n  c n,
ε : ,
 : ε > 0,
Na : ,
Ha :  (n : ), n  Na  |a n - l| < ε,
Nc : ,
Hc :  (n : ), n  Nc  |c n - l| < ε,
N :  := max Na Nc
  (n : ), n  N  |b n - l| < ε
Note that $N ≥ N_a$ and $N ≥ N_c$,
  have HNa : Na  N := by obvious_ineq,  
a b c :   ,
l : ,
ha : is_limit a l,
hc : is_limit c l,
hab :  (n : ), a n  b n,
hbc :  (n : ), b n  c n,
ε : ,
 : ε > 0,
Na : ,
Ha :  (n : ), n  Na  |a n - l| < ε,
Nc : ,
Hc :  (n : ), n  Nc  |c n - l| < ε,
N :  := max Na Nc
  (n : ), n  N  |b n - l| < ε
a b c :   ,
l : ,
ha : is_limit a l,
hc : is_limit c l,
hab :  (n : ), a n  b n,
hbc :  (n : ), b n  c n,
ε : ,
 : ε > 0,
Na : ,
Ha :  (n : ), n  Na  |a n - l| < ε,
Nc : ,
Hc :  (n : ), n  Nc  |c n - l| < ε,
N :  := max Na Nc,
HNa : Na  N
  (n : ), n  N  |b n - l| < ε
  have HNc : Nc  N := by obvious_ineq,
a b c :   ,
l : ,
ha : is_limit a l,
hc : is_limit c l,
hab :  (n : ), a n  b n,
hbc :  (n : ), b n  c n,
ε : ,
 : ε > 0,
Na : ,
Ha :  (n : ), n  Na  |a n - l| < ε,
Nc : ,
Hc :  (n : ), n  Nc  |c n - l| < ε,
N :  := max Na Nc,
HNa : Na  N
  (n : ), n  N  |b n - l| < ε
a b c :   ,
l : ,
ha : is_limit a l,
hc : is_limit c l,
hab :  (n : ), a n  b n,
hbc :  (n : ), b n  c n,
ε : ,
 : ε > 0,
Na : ,
Ha :  (n : ), n  Na  |a n - l| < ε,
Nc : ,
Hc :  (n : ), n  Nc  |c n - l| < ε,
N :  := max Na Nc,
HNa : Na  N,
HNc : Nc  N
  (n : ), n  N  |b n - l| < ε
so for all $n ≥ N$,
  intros n Hn,
a b c :   ,
l : ,
ha : is_limit a l,
hc : is_limit c l,
hab :  (n : ), a n  b n,
hbc :  (n : ), b n  c n,
ε : ,
 : ε > 0,
Na : ,
Ha :  (n : ), n  Na  |a n - l| < ε,
Nc : ,
Hc :  (n : ), n  Nc  |c n - l| < ε,
N :  := max Na Nc,
HNa : Na  N,
HNc : Nc  N
  (n : ), n  N  |b n - l| < ε
a b c :   ,
l : ,
ha : is_limit a l,
hc : is_limit c l,
hab :  (n : ), a n  b n,
hbc :  (n : ), b n  c n,
ε : ,
 : ε > 0,
Na : ,
Ha :  (n : ), n  Na  |a n - l| < ε,
Nc : ,
Hc :  (n : ), n  Nc  |c n - l| < ε,
N :  := max Na Nc,
HNa : Na  N,
HNc : Nc  N,
n : ,
Hn : n  N
 |b n - l| < ε
we have $a_n ≤ b_n ≤ c_n$, and $|a_n - l|, |b_n - l|$ are both less than $ε$.
  have h1 : a n  b n := hab n,
a b c :   ,
l : ,
ha : is_limit a l,
hc : is_limit c l,
hab :  (n : ), a n  b n,
hbc :  (n : ), b n  c n,
ε : ,
 : ε > 0,
Na : ,
Ha :  (n : ), n  Na  |a n - l| < ε,
Nc : ,
Hc :  (n : ), n  Nc  |c n - l| < ε,
N :  := max Na Nc,
HNa : Na  N,
HNc : Nc  N,
n : ,
Hn : n  N
 |b n - l| < ε
a b c :   ,
l : ,
ha : is_limit a l,
hc : is_limit c l,
hab :  (n : ), a n  b n,
hbc :  (n : ), b n  c n,
ε : ,
 : ε > 0,
Na : ,
Ha :  (n : ), n  Na  |a n - l| < ε,
Nc : ,
Hc :  (n : ), n  Nc  |c n - l| < ε,
N :  := max Na Nc,
HNa : Na  N,
HNc : Nc  N,
n : ,
Hn : n  N,
h1 : a n  b n
 |b n - l| < ε
  have h2 : b n  c n := hbc n,
a b c :   ,
l : ,
ha : is_limit a l,
hc : is_limit c l,
hab :  (n : ), a n  b n,
hbc :  (n : ), b n  c n,
ε : ,
 : ε > 0,
Na : ,
Ha :  (n : ), n  Na  |a n - l| < ε,
Nc : ,
Hc :  (n : ), n  Nc  |c n - l| < ε,
N :  := max Na Nc,
HNa : Na  N,
HNc : Nc  N,
n : ,
Hn : n  N,
h1 : a n  b n
 |b n - l| < ε
a b c :   ,
l : ,
ha : is_limit a l,
hc : is_limit c l,
hab :  (n : ), a n  b n,
hbc :  (n : ), b n  c n,
ε : ,
 : ε > 0,
Na : ,
Ha :  (n : ), n  Na  |a n - l| < ε,
Nc : ,
Hc :  (n : ), n  Nc  |c n - l| < ε,
N :  := max Na Nc,
HNa : Na  N,
HNc : Nc  N,
n : ,
Hn : n  N,
h1 : a n  b n,
h2 : b n  c n
 |b n - l| < ε
  have h3 : |a n - l| < ε := Ha n (le_trans HNa Hn),
a b c :   ,
l : ,
ha : is_limit a l,
hc : is_limit c l,
hab :  (n : ), a n  b n,
hbc :  (n : ), b n  c n,
ε : ,
 : ε > 0,
Na : ,
Ha :  (n : ), n  Na  |a n - l| < ε,
Nc : ,
Hc :  (n : ), n  Nc  |c n - l| < ε,
N :  := max Na Nc,
HNa : Na  N,
HNc : Nc  N,
n : ,
Hn : n  N,
h1 : a n  b n,
h2 : b n  c n
 |b n - l| < ε
a b c :   ,
l : ,
ha : is_limit a l,
hc : is_limit c l,
hab :  (n : ), a n  b n,
hbc :  (n : ), b n  c n,
ε : ,
 : ε > 0,
Na : ,
Ha :  (n : ), n  Na  |a n - l| < ε,
Nc : ,
Hc :  (n : ), n  Nc  |c n - l| < ε,
N :  := max Na Nc,
HNa : Na  N,
HNc : Nc  N,
n : ,
Hn : n  N,
h1 : a n  b n,
h2 : b n  c n,
h3 : |a n - l| < ε
 |b n - l| < ε
  have h4 : |c n - l| < ε := Hc n (le_trans HNc Hn),
a b c :   ,
l : ,
ha : is_limit a l,
hc : is_limit c l,
hab :  (n : ), a n  b n,
hbc :  (n : ), b n  c n,
ε : ,
 : ε > 0,
Na : ,
Ha :  (n : ), n  Na  |a n - l| < ε,
Nc : ,
Hc :  (n : ), n  Nc  |c n - l| < ε,
N :  := max Na Nc,
HNa : Na  N,
HNc : Nc  N,
n : ,
Hn : n  N,
h1 : a n  b n,
h2 : b n  c n,
h3 : |a n - l| < ε
 |b n - l| < ε
a b c :   ,
l : ,
ha : is_limit a l,
hc : is_limit c l,
hab :  (n : ), a n  b n,
hbc :  (n : ), b n  c n,
ε : ,
 : ε > 0,
Na : ,
Ha :  (n : ), n  Na  |a n - l| < ε,
Nc : ,
Hc :  (n : ), n  Nc  |c n - l| < ε,
N :  := max Na Nc,
HNa : Na  N,
HNc : Nc  N,
n : ,
Hn : n  N,
h1 : a n  b n,
h2 : b n  c n,
h3 : |a n - l| < ε,
h4 : |c n - l| < ε
 |b n - l| < ε
The result now follows easily from these inequalities (as $l-ε < a_n ≤ b_n ≤ c_n < l+ε$ ).
  rw abs_sub_lt_iff at h3 h4 ,
a b c :   ,
l : ,
ha : is_limit a l,
hc : is_limit c l,
hab :  (n : ), a n  b n,
hbc :  (n : ), b n  c n,
ε : ,
 : ε > 0,
Na : ,
Ha :  (n : ), n  Na  |a n - l| < ε,
Nc : ,
Hc :  (n : ), n  Nc  |c n - l| < ε,
N :  := max Na Nc,
HNa : Na  N,
HNc : Nc  N,
n : ,
Hn : n  N,
h1 : a n  b n,
h2 : b n  c n,
h3 : |a n - l| < ε,
h4 : |c n - l| < ε
 |b n - l| < ε
a b c :   ,
l : ,
ha : is_limit a l,
hc : is_limit c l,
hab :  (n : ), a n  b n,
hbc :  (n : ), b n  c n,
ε : ,
 : ε > 0,
Na : ,
Ha :  (n : ), n  Na  |a n - l| < ε,
Nc : ,
Hc :  (n : ), n  Nc  |c n - l| < ε,
N :  := max Na Nc,
HNa : Na  N,
HNc : Nc  N,
n : ,
Hn : n  N,
h1 : a n  b n,
h2 : b n  c n,
h4 : c n - l < ε  l - c n < ε,
h3 : a n - l < ε  l - a n < ε
 b n - l < ε  l - b n < ε
  cases h3, cases h4,
a b c :   ,
l : ,
ha : is_limit a l,
hc : is_limit c l,
hab :  (n : ), a n  b n,
hbc :  (n : ), b n  c n,
ε : ,
 : ε > 0,
Na : ,
Ha :  (n : ), n  Na  |a n - l| < ε,
Nc : ,
Hc :  (n : ), n  Nc  |c n - l| < ε,
N :  := max Na Nc,
HNa : Na  N,
HNc : Nc  N,
n : ,
Hn : n  N,
h1 : a n  b n,
h2 : b n  c n,
h4 : c n - l < ε  l - c n < ε,
h3 : a n - l < ε  l - a n < ε
 b n - l < ε  l - b n < ε
a b c :   ,
l : ,
ha : is_limit a l,
hc : is_limit c l,
hab :  (n : ), a n  b n,
hbc :  (n : ), b n  c n,
ε : ,
 : ε > 0,
Na : ,
Ha :  (n : ), n  Na  |a n - l| < ε,
Nc : ,
Hc :  (n : ), n  Nc  |c n - l| < ε,
N :  := max Na Nc,
HNa : Na  N,
HNc : Nc  N,
n : ,
Hn : n  N,
h1 : a n  b n,
h2 : b n  c n,
h3_left : a n - l < ε,
h3_right : l - a n < ε,
h4_left : c n - l < ε,
h4_right : l - c n < ε
 b n - l < ε  l - b n < ε
  split;linarith
a b c :   ,
l : ,
ha : is_limit a l,
hc : is_limit c l,
hab :  (n : ), a n  b n,
hbc :  (n : ), b n  c n,
ε : ,
 : ε > 0,
Na : ,
Ha :  (n : ), n  Na  |a n - l| < ε,
Nc : ,
Hc :  (n : ), n  Nc  |c n - l| < ε,
N :  := max Na Nc,
HNa : Na  N,
HNc : Nc  N,
n : ,
Hn : n  N,
h1 : a n  b n,
h2 : b n  c n,
h3_left : a n - l < ε,
h3_right : l - a n < ε,
h4_left : c n - l < ε,
h4_right : l - c n < ε
 b n - l < ε  l - b n < ε
a b c :   ,
l : ,
ha : is_limit a l,
hc : is_limit c l,
hab :  (n : ), a n  b n,
hbc :  (n : ), b n  c n,
ε : ,
 : ε > 0,
Na : ,
Ha :  (n : ), n  Na  |a n - l| < ε,
Nc : ,
Hc :  (n : ), n  Nc  |c n - l| < ε,
N :  := max Na Nc,
HNa : Na  N,
HNc : Nc  N,
n : ,
Hn : n  N,
h1 : a n  b n,
h2 : b n  c n,
h3_left : a n - l < ε,
h3_right : l - a n < ε,
h4_left : c n - l < ε,
h4_right : l - c n < ε
 b n - l < ε  l - b n < ε
QED.

Note that Lean finds the last line of the proof automatically -- we do not need to explicitly tell it the inequality argument.

Tactic state