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

State before:
a b c : ℤα
⊢ (OneHom.toFun (↑↑inclusion) a).im = ↑a.w * rt7 / 2
Tactic:
change (toℂ a).im = a.w * rt7 / 2
State after:
a b c : ℤα
⊢ (toℂ a).im = ↑a.w * rt7 / 2

State before:
a b c : ℤα
⊢ (toℂ a).im = ↑a.w * rt7 / 2
Tactic:
unfold toℂ
State after:
a b c : ℤα
⊢ (↑a.z + ↑a.w * complexα).im = ↑a.w * rt7 / 2

State before:
a b c : ℤα
⊢ (↑a.z + ↑a.w * complexα).im = ↑a.w * rt7 / 2
Tactic:
unfold complexα
State after:
a b c : ℤα
⊢ (↑a.z + ↑a.w * { re := 1 / 2, im := rt7 / 2 }).im = ↑a.w * rt7 / 2

State before:
a b c : ℤα
⊢ (↑a.z + ↑a.w * { re := 1 / 2, im := rt7 / 2 }).im = ↑a.w * rt7 / 2
Tactic:
simp only [add_im, int_cast_im, mul_im, int_cast_re, MulZeroClass.zero_mul, add_zero, zero_add]
State after:
a b c : ℤα
⊢ ↑a.w * (rt7 / 2) = ↑a.w * rt7 / 2

State before:
a b c : ℤα
⊢ ↑a.w * (rt7 / 2) = ↑a.w * rt7 / 2
Tactic:
ring
State after:
no goals