Theorem: CvxLean.norm2₂_eq_norm2 (CvxLean/Tactic/DCP/AtomLibrary/Fns/Norm.lean)

State before:
x y : ℝ
⊢ ‖![x, y]‖ = (x ^ 2 + y ^ 2).sqrt
Tactic:
simp [Norm.norm, sqrt_eq_rpow]
State after:
no goals