Theorem: SciLean.norm₂_squared_nat (SciLean/Core/Objects/SemiInnerProductSpace.lean)

State before:
R : Type u_1
K : Type u_2
X : Type u_3
inst✝¹ : Scalar R K
inst✝ : Norm2 K X
x : X
⊢ ‖x‖₂ ^ 2 = ‖x‖₂²
Tactic:
sorry_proof
State after:
no goals