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