Theorem: Smt.Reconstruct.Arith.arithTransSineSymmetry (Smt/Reconstruct/Arith/TransFns/ArithTransSineSymmetry.lean)

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

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

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