rw [rt7_sq]
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
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