rcases sosy with ⟨c, d, yeq⟩
case intro.intro
α : Type u_1
inst✝ : CommRing α
x y : α
sosy : SumOfSquares y
a b : α
xeq : x = a ^ 2 + b ^ 2
⊢ SumOfSquares (x * y)
case intro.intro.intro.intro
α : Type u_1
inst✝ : CommRing α
x y a b : α
xeq : x = a ^ 2 + b ^ 2
c d : α
yeq : y = c ^ 2 + d ^ 2
⊢ SumOfSquares (x * y)