-- Mathlib/Combinatorics/Additive/AP/Three/Defs.lean
theorem le_mulRothNumber_product (s : Finset α) (t : Finset β) :
    mulRothNumber s * mulRothNumber t ≤ mulRothNumber (s ×ˢ t)

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s : Finset α
t : Finset β
u : Finset α
hus : u ⊆ s
hucard : #u = mulRothNumber s
hu : ThreeGPFree ↑u
v : Finset β
hvt : v ⊆ t
hvcard : #v = mulRothNumber t
hv : ThreeGPFree ↑v
⊢ mulRothNumber s * mulRothNumber t ≤ mulRothNumber (s ×ˢ t)

Tactic:
rw [← hucard, ← hvcard, ← card_product]

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s : Finset α
t : Finset β
u : Finset α
hus : u ⊆ s
hucard : #u = mulRothNumber s
hu : ThreeGPFree ↑u
v : Finset β
hvt : v ⊆ t
hvcard : #v = mulRothNumber t
hv : ThreeGPFree ↑v
⊢ #(u ×ˢ v) ≤ mulRothNumber (s ×ˢ t)

Proof state:
case intro.intro.intro
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s : Finset α
t : Finset β
u : Finset α
hus : u ⊆ s
hucard : #u = mulRothNumber s
hu : ThreeGPFree ↑u
⊢ mulRothNumber s * mulRothNumber t ≤ mulRothNumber (s ×ˢ t)

Tactic:
obtain ⟨v, hvt, hvcard, hv⟩ := mulRothNumber_spec t

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s : Finset α
t : Finset β
u : Finset α
hus : u ⊆ s
hucard : #u = mulRothNumber s
hu : ThreeGPFree ↑u
v : Finset β
hvt : v ⊆ t
hvcard : #v = mulRothNumber t
hv : ThreeGPFree ↑v
⊢ mulRothNumber s * mulRothNumber t ≤ mulRothNumber (s ×ˢ t)

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s : Finset α
t : Finset β
u : Finset α
hus : u ⊆ s
hucard : #u = mulRothNumber s
hu : ThreeGPFree ↑u
v : Finset β
hvt : v ⊆ t
hvcard : #v = mulRothNumber t
hv : ThreeGPFree ↑v
⊢ ThreeGPFree ↑(u ×ˢ v)

Tactic:
rw [coe_product]

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s : Finset α
t : Finset β
u : Finset α
hus : u ⊆ s
hucard : #u = mulRothNumber s
hu : ThreeGPFree ↑u
v : Finset β
hvt : v ⊆ t
hvcard : #v = mulRothNumber t
hv : ThreeGPFree ↑v
⊢ ThreeGPFree (↑u ×ˢ ↑v)

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s : Finset α
t : Finset β
u : Finset α
hus : u ⊆ s
hucard : #u = mulRothNumber s
hu : ThreeGPFree ↑u
v : Finset β
hvt : v ⊆ t
hvcard : #v = mulRothNumber t
hv : ThreeGPFree ↑v
⊢ #(u ×ˢ v) ≤ mulRothNumber (s ×ˢ t)

Tactic:
refine ThreeGPFree.le_mulRothNumber ?_ (product_subset_product hus hvt)

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s : Finset α
t : Finset β
u : Finset α
hus : u ⊆ s
hucard : #u = mulRothNumber s
hu : ThreeGPFree ↑u
v : Finset β
hvt : v ⊆ t
hvcard : #v = mulRothNumber t
hv : ThreeGPFree ↑v
⊢ ThreeGPFree ↑(u ×ˢ v)

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s : Finset α
t : Finset β
⊢ mulRothNumber s * mulRothNumber t ≤ mulRothNumber (s ×ˢ t)

Tactic:
obtain ⟨u, hus, hucard, hu⟩ := mulRothNumber_spec s

Result:
case intro.intro.intro
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s : Finset α
t : Finset β
u : Finset α
hus : u ⊆ s
hucard : #u = mulRothNumber s
hu : ThreeGPFree ↑u
⊢ mulRothNumber s * mulRothNumber t ≤ mulRothNumber (s ×ˢ t)

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s : Finset α
t : Finset β
u : Finset α
hus : u ⊆ s
hucard : #u = mulRothNumber s
hu : ThreeGPFree ↑u
v : Finset β
hvt : v ⊆ t
hvcard : #v = mulRothNumber t
hv : ThreeGPFree ↑v
⊢ ThreeGPFree (↑u ×ˢ ↑v)

Tactic:
exact hu.prod hv

Result:
no goals