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

State before:
a b c : ℤα
⊢ ↑normSq (OneHom.toFun (↑↑inclusion) a) = ↑(norm a)
Tactic:
cases' a with x y
State after:
case mk
b c : ℤα
x y : ℤ
⊢ ↑normSq (OneHom.toFun ↑↑inclusion { z := x, w := y }) = ↑(norm { z := x, w := y })

State before:
case mk
b c : ℤα
x y : ℤ
⊢ ↑normSq (OneHom.toFun ↑↑inclusion { z := x, w := y }) = ↑(norm { z := x, w := y })
Tactic:
simp [normSq, norm]
State after:
case mk
b c : ℤα
x y : ℤ
⊢ (↑inclusion { z := x, w := y }).re * (↑inclusion { z := x, w := y }).re +
      (↑inclusion { z := x, w := y }).im * (↑inclusion { z := x, w := y }).im =
    ↑x ^ 2 + ↑x * ↑y + 2 * ↑y ^ 2

State before:
case mk
b c : ℤα
x y : ℤ
⊢ (↑inclusion { z := x, w := y }).re * (↑inclusion { z := x, w := y }).re +
      (↑inclusion { z := x, w := y }).im * (↑inclusion { z := x, w := y }).im =
    ↑x ^ 2 + ↑x * ↑y + 2 * ↑y ^ 2
Tactic:
ring_nf
State after:
case mk
b c : ℤα
x y : ℤ
⊢ (↑inclusion { z := x, w := y }).re ^ 2 + (↑inclusion { z := x, w := y }).im ^ 2 = ↑x * ↑y + ↑x ^ 2 + ↑y ^ 2 * 2

State before:
case mk
b c : ℤα
x y : ℤ
⊢ (↑inclusion { z := x, w := y }).re ^ 2 + (↑inclusion { z := x, w := y }).im ^ 2 = ↑x * ↑y + ↑x ^ 2 + ↑y ^ 2 * 2
Tactic:
norm_cast
State after:
case mk
b c : ℤα
x y : ℤ
⊢ (↑inclusion { z := x, w := y }).re ^ 2 + (↑inclusion { z := x, w := y }).im ^ 2 = ↑(x * y + x ^ 2 + y ^ 2 * 2)

State before:
case mk
b c : ℤα
x y : ℤ
⊢ (↑inclusion { z := x, w := y }).re ^ 2 + (↑inclusion { z := x, w := y }).im ^ 2 = ↑(x * y + x ^ 2 + y ^ 2 * 2)
Tactic:
rw [inclusion]
State after:
case mk
b c : ℤα
x y : ℤ
⊢ (↑{ toMonoidHom := { toOneHom := { toFun := toℂ, map_one' := my_map_one }, map_mul' := my_map_mul },
                map_zero' := my_map_zero, map_add' := my_map_add }
            { z := x, w := y }).re ^
        2 +
      (↑{ toMonoidHom := { toOneHom := { toFun := toℂ, map_one' := my_map_one }, map_mul' := my_map_mul },
                map_zero' := my_map_zero, map_add' := my_map_add }
            { z := x, w := y }).im ^
        2 =
    ↑(x * y + x ^ 2 + y ^ 2 * 2)

State before:
case mk
b c : ℤα
x y : ℤ
⊢ (↑{ toMonoidHom := { toOneHom := { toFun := toℂ, map_one' := my_map_one }, map_mul' := my_map_mul },
                map_zero' := my_map_zero, map_add' := my_map_add }
            { z := x, w := y }).re ^
        2 +
      (↑{ toMonoidHom := { toOneHom := { toFun := toℂ, map_one' := my_map_one }, map_mul' := my_map_mul },
                map_zero' := my_map_zero, map_add' := my_map_add }
            { z := x, w := y }).im ^
        2 =
    ↑(x * y + x ^ 2 + y ^ 2 * 2)
Tactic:
simp only [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk, cast_add, cast_mul,
cast_pow, int_cast_ofNat,toℂ]
State after:
case mk
b c : ℤα
x y : ℤ
⊢ (↑x + ↑y * complexα).re ^ 2 + (↑x + ↑y * complexα).im ^ 2 = ↑x * ↑y + ↑x ^ 2 + ↑y ^ 2 * 2

State before:
case mk
b c : ℤα
x y : ℤ
⊢ (↑x + ↑y * complexα).re ^ 2 + (↑x + ↑y * complexα).im ^ 2 = ↑x * ↑y + ↑x ^ 2 + ↑y ^ 2 * 2
Tactic:
simp only [complexα,re_of_coe, im_of_coe]
State after:
case mk
b c : ℤα
x y : ℤ
⊢ (↑x + ↑y * { re := 1 / 2, im := rt7 / 2 }).re ^ 2 + (↑x + ↑y * { re := 1 / 2, im := rt7 / 2 }).im ^ 2 =
    ↑x * ↑y + ↑x ^ 2 + ↑y ^ 2 * 2

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

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

State before:
case mk
b c : ℤα
x y : ℤ
⊢ (↑x + ↑y * (1 / 2)) ^ 2 + (↑y * (rt7 * (1 / 2))) ^ 2 = ↑x * ↑y + ↑x ^ 2 + ↑y ^ 2 * 2
Tactic:
rw [pow_two]
State after:
case mk
b c : ℤα
x y : ℤ
⊢ (↑x + ↑y * (1 / 2)) * (↑x + ↑y * (1 / 2)) + (↑y * (rt7 * (1 / 2))) ^ 2 = ↑x * ↑y + ↑x ^ 2 + ↑y ^ 2 * 2

State before:
case mk
b c : ℤα
x y : ℤ
⊢ (↑x + ↑y * (1 / 2)) * (↑x + ↑y * (1 / 2)) + (↑y * (rt7 * (1 / 2))) ^ 2 = ↑x * ↑y + ↑x ^ 2 + ↑y ^ 2 * 2
Tactic:
ring
State after:
case mk
b c : ℤα
x y : ℤ
⊢ ↑x * ↑y + ↑x ^ 2 + ↑y ^ 2 * (↑(ofNat 1) / ↑4) + ↑y ^ 2 * rt7 ^ 2 * (↑(ofNat 1) / ↑4) = ↑x * ↑y + ↑x ^ 2 + ↑y ^ 2 * 2

State before:
case mk
b c : ℤα
x y : ℤ
⊢ ↑x * ↑y + ↑x ^ 2 + ↑y ^ 2 * (↑(ofNat 1) / ↑4) + ↑y ^ 2 * rt7 ^ 2 * (↑(ofNat 1) / ↑4) = ↑x * ↑y + ↑x ^ 2 + ↑y ^ 2 * 2
Tactic:
rw [rt7_sq]
State after:
case mk
b c : ℤα
x y : ℤ
⊢ ↑x * ↑y + ↑x ^ 2 + ↑y ^ 2 * (↑(ofNat 1) / ↑4) + ↑y ^ 2 * 7 * (↑(ofNat 1) / ↑4) = ↑x * ↑y + ↑x ^ 2 + ↑y ^ 2 * 2

State before:
case mk
b c : ℤα
x y : ℤ
⊢ ↑x * ↑y + ↑x ^ 2 + ↑y ^ 2 * (↑(ofNat 1) / ↑4) + ↑y ^ 2 * 7 * (↑(ofNat 1) / ↑4) = ↑x * ↑y + ↑x ^ 2 + ↑y ^ 2 * 2
Tactic:
ring_nf
State after:
no goals