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

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

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

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

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