Theorem: Section2sheet5solutions.tendsTo_neg (FormalisingMathematics2024/Solutions/Section02reals/Sheet5.lean)

State before:
a : ℕ → ℝ
t : ℝ
ha : TendsTo a t
⊢ TendsTo (fun n => -a n) (-t)
Tactic:
rw [tendsTo_def] at *
State after:
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
⊢ ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |-a n - -t| < ε

State before:
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
⊢ ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |-a n - -t| < ε
Tactic:
have h : ∀ n, |a n - t| = |-a n - -t| := by
  intro n
  rw [abs_sub_comm]
  congr 1
  ring
State after:
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
h : ∀ (n : ℕ), |a n - t| = |-a n - -t|
⊢ ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |-a n - -t| < ε

State before:
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
h : ∀ (n : ℕ), |a n - t| = |-a n - -t|
⊢ ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |-a n - -t| < ε
Tactic:
simpa [h] using ha
State after:
no goals

State before:
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
⊢ ∀ (n : ℕ), |a n - t| = |-a n - -t|
Tactic:
intro n
State after:
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
n : ℕ
⊢ |a n - t| = |-a n - -t|

State before:
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
n : ℕ
⊢ |a n - t| = |-a n - -t|
Tactic:
rw [abs_sub_comm]
State after:
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
n : ℕ
⊢ |t - a n| = |-a n - -t|

State before:
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
n : ℕ
⊢ |t - a n| = |-a n - -t|
Tactic:
congr 1
State after:
case e_a
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
n : ℕ
⊢ t - a n = -a n - -t

State before:
case e_a
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
n : ℕ
⊢ t - a n = -a n - -t
Tactic:
ring
State after:
no goals