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

State before:
a b c : ℤα
x y : ℤ
⊢ OneHom.toFun ↑↑inclusion { z := x, w := y } = { re := ↑x + ↑y / 2, im := ↑y * rt7 / 2 }
Tactic:
change toℂ ⟨x, y⟩ = ⟨x + y / 2, y * rt7 / 2⟩
State after:
a b c : ℤα
x y : ℤ
⊢ toℂ { z := x, w := y } = { re := ↑x + ↑y / 2, im := ↑y * rt7 / 2 }

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

State before:
a b c : ℤα
x y : ℤ
⊢ ↑{ z := x, w := y }.z + ↑{ z := x, w := y }.w * complexα = { re := ↑x + ↑y / 2, im := ↑y * rt7 / 2 }
Tactic:
dsimp
State after:
a b c : ℤα
x y : ℤ
⊢ ↑x + ↑y * complexα = { re := ↑x + ↑y / 2, im := ↑y * rt7 / 2 }

State before:
a b c : ℤα
x y : ℤ
⊢ ↑x + ↑y * complexα = { re := ↑x + ↑y / 2, im := ↑y * rt7 / 2 }
Tactic:
unfold complexα
State after:
a b c : ℤα
x y : ℤ
⊢ ↑x + ↑y * { re := 1 / 2, im := rt7 / 2 } = { re := ↑x + ↑y / 2, im := ↑y * rt7 / 2 }

State before:
a b c : ℤα
x y : ℤ
⊢ ↑x + ↑y * { re := 1 / 2, im := rt7 / 2 } = { re := ↑x + ↑y / 2, im := ↑y * rt7 / 2 }
Tactic:
ext
State after:
case a
a b c : ℤα
x y : ℤ
⊢ (↑x + ↑y * { re := 1 / 2, im := rt7 / 2 }).re = { re := ↑x + ↑y / 2, im := ↑y * rt7 / 2 }.re

case a
a b c : ℤα
x y : ℤ
⊢ (↑x + ↑y * { re := 1 / 2, im := rt7 / 2 }).im = { re := ↑x + ↑y / 2, im := ↑y * rt7 / 2 }.im

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

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

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

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