rw [add_comm] at h
case mp.right
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
h : x ^ 2 + y ^ 2 = 0
⊢ y = 0
case mp.right
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
h : y ^ 2 + x ^ 2 = 0
⊢ y = 0