Theorem: use_me (LeanCourse/Assignments/Solutions/Solutions3.lean)

State before:
⊢ SequentialLimit (fun n => -1 / (↑n + 1)) 0
Tactic:
have : SequentialLimit (fun n ↦ (-1) * (1 / (n+1))) (-1 * 0) :=
  convergesTo_mul_const (-1) exercise3_5
State after:
this : SequentialLimit (fun n => -1 * (1 / (↑n + 1))) (-1 * 0)
⊢ SequentialLimit (fun n => -1 / (↑n + 1)) 0

State before:
this : SequentialLimit (fun n => -1 * (1 / (↑n + 1))) (-1 * 0)
⊢ SequentialLimit (fun n => -1 / (↑n + 1)) 0
Tactic:
simp at this
State after:
this : SequentialLimit (fun n => -(↑n + 1)⁻¹) 0
⊢ SequentialLimit (fun n => -1 / (↑n + 1)) 0

State before:
this : SequentialLimit (fun n => -(↑n + 1)⁻¹) 0
⊢ SequentialLimit (fun n => -1 / (↑n + 1)) 0
Tactic:
simp [neg_div, this]
State after:
no goals