Theorem: sequentialLimit_unique (LeanCourse/Lectures/Lecture5.lean)

State before:
u : ℕ → ℝ
l l' : ℝ
⊢ SequentialLimit u l → SequentialLimit u l' → l = l'
Tactic:
intro hl hl'
State after:
u : ℕ → ℝ
l l' : ℝ
hl : SequentialLimit u l
hl' : SequentialLimit u l'
⊢ l = l'

State before:
u : ℕ → ℝ
l l' : ℝ
hl : SequentialLimit u l
hl' : SequentialLimit u l'
⊢ l = l'
Tactic:
by_contra hll'
State after:
u : ℕ → ℝ
l l' : ℝ
hl : SequentialLimit u l
hl' : SequentialLimit u l'
hll' : ¬l = l'
⊢ False

State before:
u : ℕ → ℝ
l l' : ℝ
hl : SequentialLimit u l
hl' : SequentialLimit u l'
hll' : ¬l = l'
⊢ False
Tactic:
have : |l - l'| > 0
State after:
case this
u : ℕ → ℝ
l l' : ℝ
hl : SequentialLimit u l
hl' : SequentialLimit u l'
hll' : ¬l = l'
⊢ |l - l'| > 0

u : ℕ → ℝ
l l' : ℝ
hl : SequentialLimit u l
hl' : SequentialLimit u l'
hll' : ¬l = l'
this : |l - l'| > 0
⊢ False

State before:
u : ℕ → ℝ
l l' : ℝ
hl : SequentialLimit u l
hl' : SequentialLimit u l'
hll' : ¬l = l'
this : |l - l'| > 0
⊢ False
Tactic:
rw [SequentialLimit] at hl hl'
State after:
u : ℕ → ℝ
l l' : ℝ
hl : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| < ε
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this : |l - l'| > 0
⊢ False

State before:
u : ℕ → ℝ
l l' : ℝ
hl : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| < ε
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this : |l - l'| > 0
⊢ False
Tactic:
specialize hl (|l - l'| / 2) (by linarith)
State after:
u : ℕ → ℝ
l l' : ℝ
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this : |l - l'| > 0
hl : ∃ N, ∀ n ≥ N, |u n - l| < |l - l'| / 2
⊢ False

State before:
u : ℕ → ℝ
l l' : ℝ
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this : |l - l'| > 0
hl : ∃ N, ∀ n ≥ N, |u n - l| < |l - l'| / 2
⊢ False
Tactic:
obtain ⟨N, hN⟩ := hl
State after:
case intro
u : ℕ → ℝ
l l' : ℝ
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this : |l - l'| > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| < |l - l'| / 2
⊢ False

State before:
case intro
u : ℕ → ℝ
l l' : ℝ
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this : |l - l'| > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| < |l - l'| / 2
⊢ False
Tactic:
obtain ⟨N', hN'⟩ := hl' (|l - l'| / 2) (by linarith)
State after:
case intro.intro
u : ℕ → ℝ
l l' : ℝ
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this : |l - l'| > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| < |l - l'| / 2
N' : ℕ
hN' : ∀ n ≥ N', |u n - l'| < |l - l'| / 2
⊢ False

State before:
case intro.intro
u : ℕ → ℝ
l l' : ℝ
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this : |l - l'| > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| < |l - l'| / 2
N' : ℕ
hN' : ∀ n ≥ N', |u n - l'| < |l - l'| / 2
⊢ False
Tactic:
let N₀ := max N N'
State after:
case intro.intro
u : ℕ → ℝ
l l' : ℝ
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this : |l - l'| > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| < |l - l'| / 2
N' : ℕ
hN' : ∀ n ≥ N', |u n - l'| < |l - l'| / 2
N₀ : ℕ := max N N'
⊢ False

State before:
case intro.intro
u : ℕ → ℝ
l l' : ℝ
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this : |l - l'| > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| < |l - l'| / 2
N' : ℕ
hN' : ∀ n ≥ N', |u n - l'| < |l - l'| / 2
N₀ : ℕ := max N N'
⊢ False
Tactic:
specialize hN N₀ (Nat.le_max_left N N')
State after:
case intro.intro
u : ℕ → ℝ
l l' : ℝ
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this : |l - l'| > 0
N N' : ℕ
hN' : ∀ n ≥ N', |u n - l'| < |l - l'| / 2
N₀ : ℕ := max N N'
hN : |u N₀ - l| < |l - l'| / 2
⊢ False

State before:
case intro.intro
u : ℕ → ℝ
l l' : ℝ
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this : |l - l'| > 0
N N' : ℕ
hN' : ∀ n ≥ N', |u n - l'| < |l - l'| / 2
N₀ : ℕ := max N N'
hN : |u N₀ - l| < |l - l'| / 2
⊢ False
Tactic:
specialize hN' N₀ (Nat.le_max_right N N')
State after:
case intro.intro
u : ℕ → ℝ
l l' : ℝ
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this : |l - l'| > 0
N N' : ℕ
N₀ : ℕ := max N N'
hN : |u N₀ - l| < |l - l'| / 2
hN' : |u N₀ - l'| < |l - l'| / 2
⊢ False

State before:
case intro.intro
u : ℕ → ℝ
l l' : ℝ
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this : |l - l'| > 0
N N' : ℕ
N₀ : ℕ := max N N'
hN : |u N₀ - l| < |l - l'| / 2
hN' : |u N₀ - l'| < |l - l'| / 2
⊢ False
Tactic:
have : |l - l'| < |l - l'| := by
  calc |l - l'|
      = |l - u N₀ + (u N₀ - l')| := by ring
    _ ≤ |l - u N₀| + |u N₀ - l'| := by exact abs_add (l - u N₀) (u N₀ - l')
    _ = |u N₀ - l| + |u N₀ - l'| := by rw [abs_sub_comm]
    _ < |l - l'| := by linarith
State after:
case intro.intro
u : ℕ → ℝ
l l' : ℝ
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this✝ : |l - l'| > 0
N N' : ℕ
N₀ : ℕ := max N N'
hN : |u N₀ - l| < |l - l'| / 2
hN' : |u N₀ - l'| < |l - l'| / 2
this : |l - l'| < |l - l'|
⊢ False

State before:
case intro.intro
u : ℕ → ℝ
l l' : ℝ
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this✝ : |l - l'| > 0
N N' : ℕ
N₀ : ℕ := max N N'
hN : |u N₀ - l| < |l - l'| / 2
hN' : |u N₀ - l'| < |l - l'| / 2
this : |l - l'| < |l - l'|
⊢ False
Tactic:
linarith
State after:
no goals

State before:
case this
u : ℕ → ℝ
l l' : ℝ
hl : SequentialLimit u l
hl' : SequentialLimit u l'
hll' : ¬l = l'
⊢ |l - l'| > 0
Tactic:
apply abs_pos.2
State after:
case this
u : ℕ → ℝ
l l' : ℝ
hl : SequentialLimit u l
hl' : SequentialLimit u l'
hll' : ¬l = l'
⊢ l - l' ≠ 0

State before:
case this
u : ℕ → ℝ
l l' : ℝ
hl : SequentialLimit u l
hl' : SequentialLimit u l'
hll' : ¬l = l'
⊢ l - l' ≠ 0
Tactic:
apply sub_ne_zero.2
State after:
case this
u : ℕ → ℝ
l l' : ℝ
hl : SequentialLimit u l
hl' : SequentialLimit u l'
hll' : ¬l = l'
⊢ l ≠ l'

State before:
case this
u : ℕ → ℝ
l l' : ℝ
hl : SequentialLimit u l
hl' : SequentialLimit u l'
hll' : ¬l = l'
⊢ l ≠ l'
Tactic:
exact hll'
State after:
no goals

State before:
u : ℕ → ℝ
l l' : ℝ
hl : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| < ε
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this : |l - l'| > 0
⊢ |l - l'| / 2 > 0
Tactic:
linarith
State after:
no goals

State before:
u : ℕ → ℝ
l l' : ℝ
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this : |l - l'| > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| < |l - l'| / 2
⊢ |l - l'| / 2 > 0
Tactic:
linarith
State after:
no goals

State before:
u : ℕ → ℝ
l l' : ℝ
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this : |l - l'| > 0
N N' : ℕ
N₀ : ℕ := max N N'
hN : |u N₀ - l| < |l - l'| / 2
hN' : |u N₀ - l'| < |l - l'| / 2
⊢ |l - l'| < |l - l'|
Tactic:
calc |l - l'|
    = |l - u N₀ + (u N₀ - l')| := by ring
  _ ≤ |l - u N₀| + |u N₀ - l'| := by exact abs_add (l - u N₀) (u N₀ - l')
  _ = |u N₀ - l| + |u N₀ - l'| := by rw [abs_sub_comm]
  _ < |l - l'| := by linarith
State after:
no goals

State before:
u : ℕ → ℝ
l l' : ℝ
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this : |l - l'| > 0
N N' : ℕ
N₀ : ℕ := max N N'
hN : |u N₀ - l| < |l - l'| / 2
hN' : |u N₀ - l'| < |l - l'| / 2
⊢ |l - l'| = |l - u N₀ + (u N₀ - l')|
Tactic:
ring
State after:
no goals

State before:
u : ℕ → ℝ
l l' : ℝ
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this : |l - l'| > 0
N N' : ℕ
N₀ : ℕ := max N N'
hN : |u N₀ - l| < |l - l'| / 2
hN' : |u N₀ - l'| < |l - l'| / 2
⊢ |l - u N₀ + (u N₀ - l')| ≤ |l - u N₀| + |u N₀ - l'|
Tactic:
exact abs_add (l - u N₀) (u N₀ - l')
State after:
no goals

State before:
u : ℕ → ℝ
l l' : ℝ
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this : |l - l'| > 0
N N' : ℕ
N₀ : ℕ := max N N'
hN : |u N₀ - l| < |l - l'| / 2
hN' : |u N₀ - l'| < |l - l'| / 2
⊢ |l - u N₀| + |u N₀ - l'| = |u N₀ - l| + |u N₀ - l'|
Tactic:
rw [abs_sub_comm]
State after:
no goals

State before:
u : ℕ → ℝ
l l' : ℝ
hl' : ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l'| < ε
hll' : ¬l = l'
this : |l - l'| > 0
N N' : ℕ
N₀ : ℕ := max N N'
hN : |u N₀ - l| < |l - l'| / 2
hN' : |u N₀ - l'| < |l - l'| / 2
⊢ |u N₀ - l| + |u N₀ - l'| < |l - l'|
Tactic:
linarith
State after:
no goals