Theorem: unique_limit (GlimpseOfLean/Library/Basic.lean)

State before:
u : ℕ → ℝ
l l' : ℝ
⊢ seq_limit u l → seq_limit u l' → l = l'
Tactic:
intros hl hl'
State after:
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
⊢ l = l'

State before:
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
⊢ l = l'
Tactic:
apply eq_of_abs_sub_le_all
State after:
case a
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
⊢ ∀ ε > 0, |l - l'| ≤ ε

State before:
case a
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
⊢ ∀ ε > 0, |l - l'| ≤ ε
Tactic:
intros ε ε_pos
State after:
case a
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
⊢ |l - l'| ≤ ε

State before:
case a
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
⊢ |l - l'| ≤ ε
Tactic:
rcases hl (ε/2) (by linarith) with ⟨N, hN⟩
State after:
case a.intro
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε / 2
⊢ |l - l'| ≤ ε

State before:
case a.intro
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε / 2
⊢ |l - l'| ≤ ε
Tactic:
rcases hl' (ε/2) (by linarith) with ⟨N', hN'⟩
State after:
case a.intro.intro
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε / 2
N' : ℕ
hN' : ∀ n ≥ N', |u n - l'| ≤ ε / 2
⊢ |l - l'| ≤ ε

State before:
case a.intro.intro
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε / 2
N' : ℕ
hN' : ∀ n ≥ N', |u n - l'| ≤ ε / 2
⊢ |l - l'| ≤ ε
Tactic:
specialize hN (max N N') (le_max_left _ _)
State after:
case a.intro.intro
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
N N' : ℕ
hN' : ∀ n ≥ N', |u n - l'| ≤ ε / 2
hN : |u (max N N') - l| ≤ ε / 2
⊢ |l - l'| ≤ ε

State before:
case a.intro.intro
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
N N' : ℕ
hN' : ∀ n ≥ N', |u n - l'| ≤ ε / 2
hN : |u (max N N') - l| ≤ ε / 2
⊢ |l - l'| ≤ ε
Tactic:
specialize hN' (max N N') (le_max_right _ _)
State after:
case a.intro.intro
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
N N' : ℕ
hN : |u (max N N') - l| ≤ ε / 2
hN' : |u (max N N') - l'| ≤ ε / 2
⊢ |l - l'| ≤ ε

State before:
case a.intro.intro
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
N N' : ℕ
hN : |u (max N N') - l| ≤ ε / 2
hN' : |u (max N N') - l'| ≤ ε / 2
⊢ |l - l'| ≤ ε
Tactic:
calc |l - l'| = |(l-u (max N N')) + (u (max N N') -l')| := by ring_nf
_ ≤ |l - u (max N N')| + |u (max N N') - l'| := by apply abs_add
_ = |u (max N N') - l| + |u (max N N') - l'| := by rw [abs_sub_comm]
_ ≤ ε/2 + ε/2 := by linarith
_ = ε := by ring
State after:
no goals

State before:
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
⊢ ε / 2 > 0
Tactic:
linarith
State after:
no goals

State before:
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε / 2
⊢ ε / 2 > 0
Tactic:
linarith
State after:
no goals

State before:
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
N N' : ℕ
hN : |u (max N N') - l| ≤ ε / 2
hN' : |u (max N N') - l'| ≤ ε / 2
⊢ |l - l'| = |l - u (max N N') + (u (max N N') - l')|
Tactic:
ring_nf
State after:
no goals

State before:
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
N N' : ℕ
hN : |u (max N N') - l| ≤ ε / 2
hN' : |u (max N N') - l'| ≤ ε / 2
⊢ |l - u (max N N') + (u (max N N') - l')| ≤ |l - u (max N N')| + |u (max N N') - l'|
Tactic:
apply abs_add
State after:
no goals

State before:
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
N N' : ℕ
hN : |u (max N N') - l| ≤ ε / 2
hN' : |u (max N N') - l'| ≤ ε / 2
⊢ |l - u (max N N')| + |u (max N N') - l'| = |u (max N N') - l| + |u (max N N') - l'|
Tactic:
rw [abs_sub_comm]
State after:
no goals

State before:
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
N N' : ℕ
hN : |u (max N N') - l| ≤ ε / 2
hN' : |u (max N N') - l'| ≤ ε / 2
⊢ |u (max N N') - l| + |u (max N N') - l'| ≤ ε / 2 + ε / 2
Tactic:
linarith
State after:
no goals

State before:
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
N N' : ℕ
hN : |u (max N N') - l| ≤ ε / 2
hN' : |u (max N N') - l'| ≤ ε / 2
⊢ ε / 2 + ε / 2 = ε
Tactic:
ring
State after:
no goals