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

State before:
a b c : ℤω
⊢ ↑a.y = 2 * rt3⁻¹ * (OneHom.toFun (↑↑inclusion) a).im
Tactic:
cases' a with x y
State after:
case mk
b c : ℤω
x y : ℤ
⊢ ↑{ x := x, y := y }.y = 2 * rt3⁻¹ * (OneHom.toFun ↑↑inclusion { x := x, y := y }).im

State before:
case mk
b c : ℤω
x y : ℤ
⊢ ↑{ x := x, y := y }.y = 2 * rt3⁻¹ * (OneHom.toFun ↑↑inclusion { x := x, y := y }).im
Tactic:
simp only [coe_of_mk]
State after:
case mk
b c : ℤω
x y : ℤ
⊢ ↑y = 2 * rt3⁻¹ * (↑y * rt3 / 2)

State before:
case mk
b c : ℤω
x y : ℤ
⊢ ↑y = 2 * rt3⁻¹ * (↑y * rt3 / 2)
Tactic:
ring_nf
State after:
case mk
b c : ℤω
x y : ℤ
⊢ ↑y = rt3 * rt3⁻¹ * ↑y

State before:
case mk
b c : ℤω
x y : ℤ
⊢ ↑y = rt3 * rt3⁻¹ * ↑y
Tactic:
rw [mul_comm rt3]
State after:
case mk
b c : ℤω
x y : ℤ
⊢ ↑y = rt3⁻¹ * rt3 * ↑y

State before:
case mk
b c : ℤω
x y : ℤ
⊢ ↑y = rt3⁻¹ * rt3 * ↑y
Tactic:
simp only [sqrt3_inv_hMul_self, _root_.one_mul, Int.cast_inj, eq_self_iff_true]
State after:
no goals