Theorem: ℤα.coe_neg (Mordell4/Rt7Ring.lean)

State before:
a b c : ℤα
⊢ OneHom.toFun (↑↑inclusion) (-a) = -OneHom.toFun (↑↑inclusion) a
Tactic:
change toℂ (neg a) = -toℂ a
State after:
a b c : ℤα
⊢ toℂ (neg a) = -toℂ a

State before:
a b c : ℤα
⊢ toℂ (neg a) = -toℂ a
Tactic:
simp only [neg, toℂ]
State after:
a b c : ℤα
⊢ ↑(-a.z) + ↑(-a.w) * complexα = -(↑a.z + ↑a.w * complexα)

State before:
a b c : ℤα
⊢ ↑(-a.z) + ↑(-a.w) * complexα = -(↑a.z + ↑a.w * complexα)
Tactic:
norm_num
State after:
a b c : ℤα
⊢ -↑a.z + -(↑a.w * complexα) = -(↑a.w * complexα) + -↑a.z

State before:
a b c : ℤα
⊢ -↑a.z + -(↑a.w * complexα) = -(↑a.w * complexα) + -↑a.z
Tactic:
ring
State after:
no goals