rw [inclusion]
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)
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)