no goals
𝕜 : Type ?u.74050
E : Type u_1
α : Type ?u.74056
inst✝³ : NormedRing E
inst✝² : StarRing E
inst✝¹ : CstarRing E
inst✝ : Nontrivial E
U : { x // x ∈ unitary E }
⊢ ‖↑U‖ = 1
rw [← sq_eq_sq (norm_nonneg _) zero_le_one, one_pow 2, sq, ← CstarRing.norm_star_mul_self,
  unitary.coe_star_mul_self, CstarRing.norm_one]