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

State before:
a b c : ℤω
x y : ℤ
⊢ OneHom.toFun ↑↑inclusion { x := x, y := y } = { re := ↑x - ↑y / 2, im := ↑y * rt3 / 2 }
Tactic:
change toℂ ⟨x, y⟩ = ⟨x - y / 2, y * rt3 / 2⟩
State after:
a b c : ℤω
x y : ℤ
⊢ toℂ { x := x, y := y } = { re := ↑x - ↑y / 2, im := ↑y * rt3 / 2 }

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

State before:
a b c : ℤω
x y : ℤ
⊢ ↑{ x := x, y := y }.x + ↑{ x := x, y := y }.y * complexω = { re := ↑x - ↑y / 2, im := ↑y * rt3 / 2 }
Tactic:
dsimp
State after:
a b c : ℤω
x y : ℤ
⊢ ↑x + ↑y * complexω = { re := ↑x - ↑y / 2, im := ↑y * rt3 / 2 }

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

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

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

State before:
case a
a b c : ℤω
x y : ℤ
⊢ (↑x + ↑y * { re := -1 / 2, im := rt3 / 2 }).re = { re := ↑x - ↑y / 2, im := ↑y * rt3 / 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 := rt3 / 2 }).im = { re := ↑x - ↑y / 2, im := ↑y * rt3 / 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 * (rt3 / 2) = ↑y * rt3 / 2

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