Theorem: ℤω.complexω_sq (Mordell4/Eisenstein.lean)

State before:
a b c : ℤω
⊢ complexω ^ 2 = -complexω - 1
Tactic:
rw [pow_two]
State after:
a b c : ℤω
⊢ complexω * complexω = -complexω - 1

State before:
a b c : ℤω
⊢ complexω * complexω = -complexω - 1
Tactic:
ext
State after:
case a
a b c : ℤω
⊢ (complexω * complexω).re = (-complexω - 1).re

case a
a b c : ℤω
⊢ (complexω * complexω).im = (-complexω - 1).im

State before:
case a
a b c : ℤω
⊢ (complexω * complexω).re = (-complexω - 1).re
Tactic:
simp only [Complex.mul_re]
State after:
case a
a b c : ℤω
⊢ complexω.re * complexω.re - complexω.im * complexω.im = (-complexω - 1).re

State before:
case a
a b c : ℤω
⊢ complexω.re * complexω.re - complexω.im * complexω.im = (-complexω - 1).re
Tactic:
simp only [complexω]
State after:
case a
a b c : ℤω
⊢ -1 / 2 * (-1 / 2) - rt3 / 2 * (rt3 / 2) = (-{ re := -1 / 2, im := rt3 / 2 } - 1).re

State before:
case a
a b c : ℤω
⊢ -1 / 2 * (-1 / 2) - rt3 / 2 * (rt3 / 2) = (-{ re := -1 / 2, im := rt3 / 2 } - 1).re
Tactic:
ring_nf
State after:
case a
a b c : ℤω
⊢ ↑(ofNat 1) / ↑4 + rt3 ^ 2 * ↑(negOfNat 1) * (↑(ofNat 1) / ↑4) =
    (-1 - { re := ↑(negOfNat 1) * (↑(ofNat 1) / ↑2), im := rt3 * (↑(ofNat 1) / ↑2) }).re

State before:
case a
a b c : ℤω
⊢ ↑(ofNat 1) / ↑4 + rt3 ^ 2 * ↑(negOfNat 1) * (↑(ofNat 1) / ↑4) =
    (-1 - { re := ↑(negOfNat 1) * (↑(ofNat 1) / ↑2), im := rt3 * (↑(ofNat 1) / ↑2) }).re
Tactic:
rw [rt3_sq]
State after:
case a
a b c : ℤω
⊢ ↑(ofNat 1) / ↑4 + 3 * ↑(negOfNat 1) * (↑(ofNat 1) / ↑4) =
    (-1 - { re := ↑(negOfNat 1) * (↑(ofNat 1) / ↑2), im := rt3 * (↑(ofNat 1) / ↑2) }).re

State before:
case a
a b c : ℤω
⊢ ↑(ofNat 1) / ↑4 + 3 * ↑(negOfNat 1) * (↑(ofNat 1) / ↑4) =
    (-1 - { re := ↑(negOfNat 1) * (↑(ofNat 1) / ↑2), im := rt3 * (↑(ofNat 1) / ↑2) }).re
Tactic:
norm_num
State after:
no goals

State before:
case a
a b c : ℤω
⊢ (complexω * complexω).im = (-complexω - 1).im
Tactic:
rw [Complex.mul_im]
State after:
case a
a b c : ℤω
⊢ complexω.re * complexω.im + complexω.im * complexω.re = (-complexω - 1).im

State before:
case a
a b c : ℤω
⊢ complexω.re * complexω.im + complexω.im * complexω.re = (-complexω - 1).im
Tactic:
simp only [complexω]
State after:
case a
a b c : ℤω
⊢ -1 / 2 * (rt3 / 2) + rt3 / 2 * (-1 / 2) = (-{ re := -1 / 2, im := rt3 / 2 } - 1).im

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

State before:
case a
a b c : ℤω
⊢ rt3 * ↑(negOfNat 1) * (↑(ofNat 1) / ↑2) =
    (-1 - { re := ↑(negOfNat 1) * (↑(ofNat 1) / ↑2), im := rt3 * (↑(ofNat 1) / ↑2) }).im
Tactic:
dsimp
State after:
case a
a b c : ℤω
⊢ rt3 * ↑(negOfNat 1) * (↑1 / 2) = -0 - rt3 * (↑1 / 2)

State before:
case a
a b c : ℤω
⊢ rt3 * ↑(negOfNat 1) * (↑1 / 2) = -0 - rt3 * (↑1 / 2)
Tactic:
ring_nf
State after:
no goals