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:
have h := tendsTo_sub hs ht
State after:
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : TendsTo (fun n => a n - a n) (s - t)
⊢ s = t

State before:
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : TendsTo (fun n => a n - a n) (s - t)
⊢ s = t
Tactic:
suffices ∀ ε > 0, |t - s| < ε by linarith [eq_zero_of_abs_lt_eps this]
State after:
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : TendsTo (fun n => a n - a n) (s - t)
⊢ ∀ ε > 0, |t - s| < ε

State before:
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : TendsTo (fun n => a n - a n) (s - t)
⊢ ∀ ε > 0, |t - s| < ε
Tactic:
intro ε hε
State after:
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : TendsTo (fun n => a n - a n) (s - t)
ε : ℝ
hε : ε > 0
⊢ |t - s| < ε

State before:
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : TendsTo (fun n => a n - a n) (s - t)
ε : ℝ
hε : ε > 0
⊢ |t - s| < ε
Tactic:
obtain ⟨X, hX⟩ := h ε hε
State after:
case intro
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : TendsTo (fun n => a n - a n) (s - t)
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |(fun n => a n - a n) n - (s - t)| < ε
⊢ |t - s| < ε

State before:
case intro
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : TendsTo (fun n => a n - a n) (s - t)
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |(fun n => a n - a n) n - (s - t)| < ε
⊢ |t - s| < ε
Tactic:
specialize hX X (by rfl)
State after:
case intro
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : TendsTo (fun n => a n - a n) (s - t)
ε : ℝ
hε : ε > 0
X : ℕ
hX : |(fun n => a n - a n) X - (s - t)| < ε
⊢ |t - s| < ε

State before:
case intro
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : TendsTo (fun n => a n - a n) (s - t)
ε : ℝ
hε : ε > 0
X : ℕ
hX : |(fun n => a n - a n) X - (s - t)| < ε
⊢ |t - s| < ε
Tactic:
simpa using hX
State after:
no goals

State before:
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : TendsTo (fun n => a n - a n) (s - t)
this : ∀ ε > 0, |t - s| < ε
⊢ s = t
Tactic:
linarith [eq_zero_of_abs_lt_eps this]
State after:
no goals

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