Theorem: Smt.Reconstruct.Arith.sin_neg' (Smt/Reconstruct/Arith/TransFns/ArithTransSineTangentZero.lean)

State before:
⊢ ∀ (t : ℝ), t.sin = -(-t).sin
Tactic:
intro t
State after:
t : ℝ
⊢ t.sin = -(-t).sin

State before:
t : ℝ
⊢ t.sin = -(-t).sin
Tactic:
rw [sin_neg t]
State after:
t : ℝ
⊢ t.sin = - -t.sin

State before:
t : ℝ
⊢ t.sin = - -t.sin
Tactic:
simp
State after:
no goals