simp only [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk, cast_add, cast_mul,
cast_pow, int_cast_ofNat,toℂ]
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)
case mk
b c : ℤα
x y : ℤ
⊢ (↑x + ↑y * complexα).re ^ 2 + (↑x + ↑y * complexα).im ^ 2 = ↑x * ↑y + ↑x ^ 2 + ↑y ^ 2 * 2