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, xeq⟩
State after:
case intro.intro
α : Type u_1
inst✝ : CommRing α
x y : α
sosy : SumOfSquares y
a b : α
xeq : x = a ^ 2 + b ^ 2
⊢ SumOfSquares (x * y)

State before:
case intro.intro
α : Type u_1
inst✝ : CommRing α
x y : α
sosy : SumOfSquares y
a b : α
xeq : x = a ^ 2 + b ^ 2
⊢ SumOfSquares (x * y)
Tactic:
rcases sosy with ⟨c, d, yeq⟩
State after:
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)

State before:
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)
Tactic:
rw [xeq, yeq]
State after:
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 ((a ^ 2 + b ^ 2) * (c ^ 2 + d ^ 2))

State before:
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 ((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 α
x y a b : α
xeq : x = a ^ 2 + b ^ 2
c d : α
yeq : y = c ^ 2 + d ^ 2
⊢ (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 α
x y a b : α
xeq : x = a ^ 2 + b ^ 2
c d : α
yeq : y = c ^ 2 + d ^ 2
⊢ (a ^ 2 + b ^ 2) * (c ^ 2 + d ^ 2) = (a * c - b * d) ^ 2 + (a * d + b * c) ^ 2
Tactic:
ring
State after:
no goals