Theorem: ℤω.coe_neg (Mordell4/Eisenstein.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.x) + ↑(-a.y) * complexω = -(↑a.x + ↑a.y * complexω)

State before:
a b c : ℤω
⊢ ↑(-a.x) + ↑(-a.y) * complexω = -(↑a.x + ↑a.y * complexω)
Tactic:
norm_num
State after:
a b c : ℤω
⊢ -↑a.x + -(↑a.y * complexω) = -(↑a.y * complexω) + -↑a.x

State before:
a b c : ℤω
⊢ -↑a.x + -(↑a.y * complexω) = -(↑a.y * complexω) + -↑a.x
Tactic:
ring
State after:
no goals