norm_num
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
case mk
b c : ℤα
x y : ℤ
⊢ (↑x + ↑y * (1 / 2)) ^ 2 + (↑y * (rt7 * (1 / 2))) ^ 2 = ↑x * ↑y + ↑x ^ 2 + ↑y ^ 2 * 2