Theorem: C03S06.convergesTo_uniqueαα (MIL/C03_Logic/S06_Sequences_and_Convergence.lean)

State before:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
⊢ a = b
Tactic:
by_contra abne
State after:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
⊢ False

State before:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
⊢ False
Tactic:
let ε := |a - b| / 2
State after:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
⊢ False

State before:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
⊢ False
Tactic:
have εpos : ε > 0 := by
  change |a - b| / 2 > 0
  linarith
State after:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
⊢ False

State before:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
⊢ False
Tactic:
rcases sa ε εpos with ⟨Na, hNa⟩
State after:
case intro
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
⊢ False

State before:
case intro
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
⊢ False
Tactic:
rcases sb ε εpos with ⟨Nb, hNb⟩
State after:
case intro.intro
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
⊢ False

State before:
case intro.intro
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
⊢ False
Tactic:
let N := max Na Nb
State after:
case intro.intro
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
⊢ False

State before:
case intro.intro
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
⊢ False
Tactic:
have absa : |s N - a| < ε := by
  apply hNa
  apply le_max_left
State after:
case intro.intro
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
⊢ False

State before:
case intro.intro
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
⊢ False
Tactic:
have absb : |s N - b| < ε := by
  apply hNb
  apply le_max_right
State after:
case intro.intro
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
absb : |s N - b| < ε
⊢ False

State before:
case intro.intro
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
absb : |s N - b| < ε
⊢ False
Tactic:
have : |a - b| < |a - b|
State after:
case this
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
absb : |s N - b| < ε
⊢ |a - b| < |a - b|

case intro.intro
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this✝ : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
absb : |s N - b| < ε
this : |a - b| < |a - b|
⊢ False

State before:
case this
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
absb : |s N - b| < ε
⊢ |a - b| < |a - b|

case intro.intro
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this✝ : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
absb : |s N - b| < ε
this : |a - b| < |a - b|
⊢ False
Tactic:
calc
  |a - b| = |(-(s N - a)) + (s N - b)| := by
    congr
    ring
  _ ≤ |(-(s N - a))| + |s N - b| := (abs_add _ _)
  _ = |s N - a| + |s N - b| := by rw [abs_neg]
  _ < ε + ε := (add_lt_add absa absb)
  _ = |a - b| := by norm_num [ε]
State after:
case intro.intro
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this✝ : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
absb : |s N - b| < ε
this : |a - b| < |a - b|
⊢ False

State before:
case intro.intro
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this✝ : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
absb : |s N - b| < ε
this : |a - b| < |a - b|
⊢ False
Tactic:
exact lt_irrefl _ this
State after:
no goals

State before:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
⊢ |a - b| > 0
Tactic:
apply lt_of_le_of_ne
State after:
case a
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
⊢ 0 ≤ |a - b|

case a
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
⊢ 0 ≠ |a - b|

State before:
case a
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
⊢ 0 ≠ |a - b|
Tactic:
intro h''
State after:
case a
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
h'' : 0 = |a - b|
⊢ False

State before:
case a
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
h'' : 0 = |a - b|
⊢ False
Tactic:
apply abne
State after:
case a
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
h'' : 0 = |a - b|
⊢ a = b

State before:
case a
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
h'' : 0 = |a - b|
⊢ a = b
Tactic:
apply eq_of_abs_sub_eq_zero h''.symm
State after:
no goals

State before:
case a
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
⊢ 0 ≤ |a - b|
Tactic:
apply abs_nonneg
State after:
no goals

State before:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
⊢ ε > 0
Tactic:
change |a - b| / 2 > 0
State after:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
⊢ |a - b| / 2 > 0

State before:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
⊢ |a - b| / 2 > 0
Tactic:
linarith
State after:
no goals

State before:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
⊢ |s N - a| < ε
Tactic:
apply hNa
State after:
case a
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
⊢ N ≥ Na

State before:
case a
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
⊢ N ≥ Na
Tactic:
apply le_max_left
State after:
no goals

State before:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
⊢ |s N - b| < ε
Tactic:
apply hNb
State after:
case a
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
⊢ N ≥ Nb

State before:
case a
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
⊢ N ≥ Nb
Tactic:
apply le_max_right
State after:
no goals

State before:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
absb : |s N - b| < ε
⊢ |a - b| = |-(s N - a) + (s N - b)|
Tactic:
congr
State after:
case e_a
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
absb : |s N - b| < ε
⊢ a - b = -(s N - a) + (s N - b)

State before:
case e_a
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
absb : |s N - b| < ε
⊢ a - b = -(s N - a) + (s N - b)
Tactic:
ring
State after:
no goals

State before:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
absb : |s N - b| < ε
⊢ |(-(s N - a))| + |s N - b| = |s N - a| + |s N - b|
Tactic:
rw [abs_neg]
State after:
no goals

State before:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
absb : |s N - b| < ε
⊢ ε + ε = |a - b|
Tactic:
norm_num [ε]
State after:
no goals