Theorem: ℤα.complexα_sq (Mordell4/Rt7Ring.lean)

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

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

case a
a b c : ℤα
⊢ (complexα * complexα).im = (complexα - 2).im

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

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

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

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

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

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

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

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

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

State before:
case a
a b c : ℤα
⊢ rt7 * (↑1 / 2) = -0 + rt7 * (↑1 / 2)
Tactic:
norm_cast
State after:
case a
a b c : ℤα
⊢ rt7 * ↑(Rat.divInt 1 2) = ↑(-0) + rt7 * ↑(Rat.divInt 1 2)

State before:
case a
a b c : ℤα
⊢ rt7 * ↑(Rat.divInt 1 2) = ↑(-0) + rt7 * ↑(Rat.divInt 1 2)
Tactic:
ring_nf
State after:
no goals