Theorem: ℤω.re_of_coe (Mordell4/Eisenstein.lean)

State before:
a b c : ℤω
⊢ (OneHom.toFun (↑↑inclusion) a).re = ↑a.x - ↑a.y / 2
Tactic:
change (toℂ a).re = a.x - a.y / 2
State after:
a b c : ℤω
⊢ (toℂ a).re = ↑a.x - ↑a.y / 2

State before:
a b c : ℤω
⊢ (toℂ a).re = ↑a.x - ↑a.y / 2
Tactic:
unfold toℂ
State after:
a b c : ℤω
⊢ (↑a.x + ↑a.y * complexω).re = ↑a.x - ↑a.y / 2

State before:
a b c : ℤω
⊢ (↑a.x + ↑a.y * complexω).re = ↑a.x - ↑a.y / 2
Tactic:
unfold complexω
State after:
a b c : ℤω
⊢ (↑a.x + ↑a.y * { re := -1 / 2, im := rt3 / 2 }).re = ↑a.x - ↑a.y / 2

State before:
a b c : ℤω
⊢ (↑a.x + ↑a.y * { re := -1 / 2, im := rt3 / 2 }).re = ↑a.x - ↑a.y / 2
Tactic:
simp only [add_re, int_cast_re, mul_re, int_cast_im, MulZeroClass.zero_mul, tsub_zero]
State after:
a b c : ℤω
⊢ ↑a.x + ↑a.y * (-1 / 2) = ↑a.x - ↑a.y / 2

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