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

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

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

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

State before:
case mk
b c : ℤα
x y : ℤ
⊢ ↑y = rt7 * rt7⁻¹ * ↑y
Tactic:
rw [mul_comm]
State after:
case mk
b c : ℤα
x y : ℤ
⊢ ↑y = ↑y * (rt7 * rt7⁻¹)

State before:
case mk
b c : ℤα
x y : ℤ
⊢ ↑y = ↑y * (rt7 * rt7⁻¹)
Tactic:
norm_num
State after:
no goals