case intro.intro.intro
F : Type ?u.140244
α : Type u_1
β : Type u_2
𝕜 : Type ?u.140253
E : Type ?u.140256
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s✝ t✝ : Finset α
n : ℕ
s : Finset α
t : Finset β
u : Finset α
hus : u ⊆ s
hucard : card u = ↑mulRothNumber s
hu : MulSalemSpencer ↑u
⊢ ↑mulRothNumber s * ↑mulRothNumber t ≤ ↑mulRothNumber (s ×ˢ t)
F : Type ?u.140244
α : Type u_1
β : Type u_2
𝕜 : Type ?u.140253
E : Type ?u.140256
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s✝ t✝ : Finset α
n : ℕ
s : Finset α
t : Finset β
⊢ ↑mulRothNumber s * ↑mulRothNumber t ≤ ↑mulRothNumber (s ×ˢ t)
obtain ⟨u, hus, hucard, hu⟩ := mulRothNumber_spec s
case intro.intro.intro.intro.intro.intro
F : Type ?u.140244
α : Type u_1
β : Type u_2
𝕜 : Type ?u.140253
E : Type ?u.140256
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s✝ t✝ : Finset α
n : ℕ
s : Finset α
t : Finset β
u : Finset α
hus : u ⊆ s
hucard : card u = ↑mulRothNumber s
hu : MulSalemSpencer ↑u
v : Finset β
hvt : v ⊆ t
hvcard : card v = ↑mulRothNumber t
hv : MulSalemSpencer ↑v
⊢ ↑mulRothNumber s * ↑mulRothNumber t ≤ ↑mulRothNumber (s ×ˢ t)
case intro.intro.intro
F : Type ?u.140244
α : Type u_1
β : Type u_2
𝕜 : Type ?u.140253
E : Type ?u.140256
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s✝ t✝ : Finset α
n : ℕ
s : Finset α
t : Finset β
u : Finset α
hus : u ⊆ s
hucard : card u = ↑mulRothNumber s
hu : MulSalemSpencer ↑u
⊢ ↑mulRothNumber s * ↑mulRothNumber t ≤ ↑mulRothNumber (s ×ˢ t)
obtain ⟨v, hvt, hvcard, hv⟩ := mulRothNumber_spec t
case intro.intro.intro.intro.intro.intro
F : Type ?u.140244
α : Type u_1
β : Type u_2
𝕜 : Type ?u.140253
E : Type ?u.140256
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s✝ t✝ : Finset α
n : ℕ
s : Finset α
t : Finset β
u : Finset α
hus : u ⊆ s
hucard : card u = ↑mulRothNumber s
hu : MulSalemSpencer ↑u
v : Finset β
hvt : v ⊆ t
hvcard : card v = ↑mulRothNumber t
hv : MulSalemSpencer ↑v
⊢ card (u ×ˢ v) ≤ ↑mulRothNumber (s ×ˢ t)
case intro.intro.intro.intro.intro.intro
F : Type ?u.140244
α : Type u_1
β : Type u_2
𝕜 : Type ?u.140253
E : Type ?u.140256
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s✝ t✝ : Finset α
n : ℕ
s : Finset α
t : Finset β
u : Finset α
hus : u ⊆ s
hucard : card u = ↑mulRothNumber s
hu : MulSalemSpencer ↑u
v : Finset β
hvt : v ⊆ t
hvcard : card v = ↑mulRothNumber t
hv : MulSalemSpencer ↑v
⊢ ↑mulRothNumber s * ↑mulRothNumber t ≤ ↑mulRothNumber (s ×ˢ t)
rw [← hucard, ← hvcard, ← card_product]
case intro.intro.intro.intro.intro.intro
F : Type ?u.140244
α : Type u_1
β : Type u_2
𝕜 : Type ?u.140253
E : Type ?u.140256
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s✝ t✝ : Finset α
n : ℕ
s : Finset α
t : Finset β
u : Finset α
hus : u ⊆ s
hucard : card u = ↑mulRothNumber s
hu : MulSalemSpencer ↑u
v : Finset β
hvt : v ⊆ t
hvcard : card v = ↑mulRothNumber t
hv : MulSalemSpencer ↑v
⊢ MulSalemSpencer ↑(u ×ˢ v)
case intro.intro.intro.intro.intro.intro
F : Type ?u.140244
α : Type u_1
β : Type u_2
𝕜 : Type ?u.140253
E : Type ?u.140256
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s✝ t✝ : Finset α
n : ℕ
s : Finset α
t : Finset β
u : Finset α
hus : u ⊆ s
hucard : card u = ↑mulRothNumber s
hu : MulSalemSpencer ↑u
v : Finset β
hvt : v ⊆ t
hvcard : card v = ↑mulRothNumber t
hv : MulSalemSpencer ↑v
⊢ card (u ×ˢ v) ≤ ↑mulRothNumber (s ×ˢ t)
refine' MulSalemSpencer.le_mulRothNumber _ (product_subset_product hus hvt)
case intro.intro.intro.intro.intro.intro
F : Type ?u.140244
α : Type u_1
β : Type u_2
𝕜 : Type ?u.140253
E : Type ?u.140256
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s✝ t✝ : Finset α
n : ℕ
s : Finset α
t : Finset β
u : Finset α
hus : u ⊆ s
hucard : card u = ↑mulRothNumber s
hu : MulSalemSpencer ↑u
v : Finset β
hvt : v ⊆ t
hvcard : card v = ↑mulRothNumber t
hv : MulSalemSpencer ↑v
⊢ MulSalemSpencer (↑u ×ˢ ↑v)
case intro.intro.intro.intro.intro.intro
F : Type ?u.140244
α : Type u_1
β : Type u_2
𝕜 : Type ?u.140253
E : Type ?u.140256
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s✝ t✝ : Finset α
n : ℕ
s : Finset α
t : Finset β
u : Finset α
hus : u ⊆ s
hucard : card u = ↑mulRothNumber s
hu : MulSalemSpencer ↑u
v : Finset β
hvt : v ⊆ t
hvcard : card v = ↑mulRothNumber t
hv : MulSalemSpencer ↑v
⊢ MulSalemSpencer ↑(u ×ˢ v)
rw [coe_product]
no goals
case intro.intro.intro.intro.intro.intro
F : Type ?u.140244
α : Type u_1
β : Type u_2
𝕜 : Type ?u.140253
E : Type ?u.140256
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s✝ t✝ : Finset α
n : ℕ
s : Finset α
t : Finset β
u : Finset α
hus : u ⊆ s
hucard : card u = ↑mulRothNumber s
hu : MulSalemSpencer ↑u
v : Finset β
hvt : v ⊆ t
hvcard : card v = ↑mulRothNumber t
hv : MulSalemSpencer ↑v
⊢ MulSalemSpencer (↑u ×ˢ ↑v)
exact hu.prod hv