Theorem: Section2sheet6Solutions.tendsTo_unique (FormalisingMathematics2024/Solutions/Section02reals/Sheet6.lean)

State before:
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
⊢ s = t
Tactic:
by_contra h
State after:
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
⊢ False

State before:
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
⊢ False
Tactic:
wlog h2 : s < t
State after:
case inr
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
this : ∀ (a : ℕ → ℝ) (s t : ℝ), TendsTo a s → TendsTo a t → ¬s = t → s < t → False
h2 : ¬s < t
⊢ False

a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
h2 : s < t
⊢ False

State before:
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
h2 : s < t
⊢ False
Tactic:
set ε := t - s with hε
State after:
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
h2 : s < t
ε : ℝ := t - s
hε : ε = t - s
⊢ False

State before:
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
h2 : s < t
ε : ℝ := t - s
hε : ε = t - s
⊢ False
Tactic:
have hε : 0 < ε := sub_pos.mpr h2
State after:
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
h2 : s < t
ε : ℝ := t - s
hε✝ : ε = t - s
hε : 0 < ε
⊢ False

State before:
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
h2 : s < t
ε : ℝ := t - s
hε✝ : ε = t - s
hε : 0 < ε
⊢ False
Tactic:
obtain ⟨X, hX⟩ := hs (ε / 2) (by linarith)
State after:
case intro
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
h2 : s < t
ε : ℝ := t - s
hε✝ : ε = t - s
hε : 0 < ε
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - s| < ε / 2
⊢ False

State before:
case intro
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
h2 : s < t
ε : ℝ := t - s
hε✝ : ε = t - s
hε : 0 < ε
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - s| < ε / 2
⊢ False
Tactic:
obtain ⟨Y, hY⟩ := ht (ε / 2) (by linarith)
State after:
case intro.intro
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
h2 : s < t
ε : ℝ := t - s
hε✝ : ε = t - s
hε : 0 < ε
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - s| < ε / 2
Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |a n - t| < ε / 2
⊢ False

State before:
case intro.intro
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
h2 : s < t
ε : ℝ := t - s
hε✝ : ε = t - s
hε : 0 < ε
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - s| < ε / 2
Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |a n - t| < ε / 2
⊢ False
Tactic:
specialize hX (max X Y) (le_max_left X Y)
State after:
case intro.intro
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
h2 : s < t
ε : ℝ := t - s
hε✝ : ε = t - s
hε : 0 < ε
X Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |a n - t| < ε / 2
hX : |a (max X Y) - s| < ε / 2
⊢ False

State before:
case intro.intro
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
h2 : s < t
ε : ℝ := t - s
hε✝ : ε = t - s
hε : 0 < ε
X Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |a n - t| < ε / 2
hX : |a (max X Y) - s| < ε / 2
⊢ False
Tactic:
specialize hY (max X Y) (le_max_right X Y)
State after:
case intro.intro
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
h2 : s < t
ε : ℝ := t - s
hε✝ : ε = t - s
hε : 0 < ε
X Y : ℕ
hX : |a (max X Y) - s| < ε / 2
hY : |a (max X Y) - t| < ε / 2
⊢ False

State before:
case intro.intro
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
h2 : s < t
ε : ℝ := t - s
hε✝ : ε = t - s
hε : 0 < ε
X Y : ℕ
hX : |a (max X Y) - s| < ε / 2
hY : |a (max X Y) - t| < ε / 2
⊢ False
Tactic:
rw [abs_lt] at hX hY
State after:
case intro.intro
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
h2 : s < t
ε : ℝ := t - s
hε✝ : ε = t - s
hε : 0 < ε
X Y : ℕ
hX : -(ε / 2) < a (max X Y) - s ∧ a (max X Y) - s < ε / 2
hY : -(ε / 2) < a (max X Y) - t ∧ a (max X Y) - t < ε / 2
⊢ False

State before:
case intro.intro
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
h2 : s < t
ε : ℝ := t - s
hε✝ : ε = t - s
hε : 0 < ε
X Y : ℕ
hX : -(ε / 2) < a (max X Y) - s ∧ a (max X Y) - s < ε / 2
hY : -(ε / 2) < a (max X Y) - t ∧ a (max X Y) - t < ε / 2
⊢ False
Tactic:
linarith
State after:
no goals

State before:
case inr
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
this : ∀ (a : ℕ → ℝ) (s t : ℝ), TendsTo a s → TendsTo a t → ¬s = t → s < t → False
h2 : ¬s < t
⊢ False
Tactic:
cases' Ne.lt_or_lt h with h3 h3
State after:
case inr.inl
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
this : ∀ (a : ℕ → ℝ) (s t : ℝ), TendsTo a s → TendsTo a t → ¬s = t → s < t → False
h2 : ¬s < t
h3 : s < t
⊢ False

case inr.inr
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
this : ∀ (a : ℕ → ℝ) (s t : ℝ), TendsTo a s → TendsTo a t → ¬s = t → s < t → False
h2 : ¬s < t
h3 : t < s
⊢ False

State before:
case inr.inl
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
this : ∀ (a : ℕ → ℝ) (s t : ℝ), TendsTo a s → TendsTo a t → ¬s = t → s < t → False
h2 : ¬s < t
h3 : s < t
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
case inr.inr
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
this : ∀ (a : ℕ → ℝ) (s t : ℝ), TendsTo a s → TendsTo a t → ¬s = t → s < t → False
h2 : ¬s < t
h3 : t < s
⊢ False
Tactic:
apply this _ _ _ ht hs _ h3
State after:
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
this : ∀ (a : ℕ → ℝ) (s t : ℝ), TendsTo a s → TendsTo a t → ¬s = t → s < t → False
h2 : ¬s < t
h3 : t < s
⊢ ¬t = s

State before:
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
this : ∀ (a : ℕ → ℝ) (s t : ℝ), TendsTo a s → TendsTo a t → ¬s = t → s < t → False
h2 : ¬s < t
h3 : t < s
⊢ ¬t = s
Tactic:
exact ne_comm.mp h
State after:
no goals

State before:
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
h2 : s < t
ε : ℝ := t - s
hε✝ : ε = t - s
hε : 0 < ε
⊢ ε / 2 > 0
Tactic:
linarith
State after:
no goals

State before:
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
h2 : s < t
ε : ℝ := t - s
hε✝ : ε = t - s
hε : 0 < ε
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - s| < ε / 2
⊢ ε / 2 > 0
Tactic:
linarith
State after:
no goals