Theorem: uniq_limit (GlimpseOfLean/Solutions/Topics/SequenceLimits.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:
calc
  |l - l'| ≤ |l - u (max N N')| + |u (max N N') - l'| := by apply abs_sub_le
         _ = |u (max N N') - l| + |u (max N N') - l'| := by rw [abs_sub_comm]
         _ ≤ ε := by linarith [hN _ (le_max_left N N'), hN' _ (le_max_right N N')]
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 : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε / 2
N' : ℕ
hN' : ∀ n ≥ N', |u n - l'| ≤ ε / 2
⊢ |l - l'| ≤ |l - u (max N N')| + |u (max N N') - l'|
Tactic:
apply abs_sub_le
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
N' : ℕ
hN' : ∀ n ≥ N', |u 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 : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε / 2
N' : ℕ
hN' : ∀ n ≥ N', |u n - l'| ≤ ε / 2
⊢ |u (max N N') - l| + |u (max N N') - l'| ≤ ε
Tactic:
linarith [hN _ (le_max_left N N'), hN' _ (le_max_right N N')]
State after:
no goals