Theorem: C03S02.sumOfSquares_mul' (LeanInRome/S3_Logic/S02_The_Existential_Quantifier.lean)

State before:
α : Type u_1
inst✝ : CommRing α
x y : α
sosx : SumOfSquares x
sosy : SumOfSquares y
⊢ SumOfSquares (x * y)
Tactic:
rcases sosx with ⟨a, b, rfl⟩
State after:
case intro.intro
α : Type u_1
inst✝ : CommRing α
y : α
sosy : SumOfSquares y
a b : α
⊢ SumOfSquares ((a ^ 2 + b ^ 2) * y)

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

State before:
case intro.intro.intro.intro
α : Type u_1
inst✝ : CommRing α
a b c d : α
⊢ SumOfSquares ((a ^ 2 + b ^ 2) * (c ^ 2 + d ^ 2))
Tactic:
use a * c - b * d, a * d + b * c
State after:
case h
α : Type u_1
inst✝ : CommRing α
a b c d : α
⊢ (a ^ 2 + b ^ 2) * (c ^ 2 + d ^ 2) = (a * c - b * d) ^ 2 + (a * d + b * c) ^ 2

State before:
case h
α : Type u_1
inst✝ : CommRing α
a b c d : α
⊢ (a ^ 2 + b ^ 2) * (c ^ 2 + d ^ 2) = (a * c - b * d) ^ 2 + (a * d + b * c) ^ 2
Tactic:
ring
State after:
no goals