case refine'_1
F : Type ?u.143344
α : Type u_1
β : Type ?u.143350
𝕜 : Type ?u.143353
E : Type ?u.143356
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
⊢ ↑mulRothNumber (map (mulLeftEmbedding a) s) ≤ ↑mulRothNumber s

case refine'_2
F : Type ?u.143344
α : Type u_1
β : Type ?u.143350
𝕜 : Type ?u.143353
E : Type ?u.143356
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
⊢ ↑mulRothNumber s ≤ ↑mulRothNumber (map (mulLeftEmbedding a) s)
F : Type ?u.143344
α : Type u_1
β : Type ?u.143350
𝕜 : Type ?u.143353
E : Type ?u.143356
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
⊢ ↑mulRothNumber (map (mulLeftEmbedding a) s) = ↑mulRothNumber s
refine' le_antisymm _ _
case refine'_1.intro.intro.intro
F : Type ?u.143344
α : Type u_1
β : Type ?u.143350
𝕜 : Type ?u.143353
E : Type ?u.143356
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ map (mulLeftEmbedding a) s
hcard : card u = ↑mulRothNumber (map (mulLeftEmbedding a) s)
hu : MulSalemSpencer ↑u
⊢ ↑mulRothNumber (map (mulLeftEmbedding a) s) ≤ ↑mulRothNumber s
case refine'_1
F : Type ?u.143344
α : Type u_1
β : Type ?u.143350
𝕜 : Type ?u.143353
E : Type ?u.143356
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
⊢ ↑mulRothNumber (map (mulLeftEmbedding a) s) ≤ ↑mulRothNumber s
obtain ⟨u, hus, hcard, hu⟩ := mulRothNumber_spec (s.map <| mulLeftEmbedding a)
case refine'_1.intro.intro.intro
F : Type ?u.143344
α : Type u_1
β : Type ?u.143350
𝕜 : Type ?u.143353
E : Type ?u.143356
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : ∃ u_1 x, u = map (mulLeftEmbedding a) u_1
hcard : card u = ↑mulRothNumber (map (mulLeftEmbedding a) s)
hu : MulSalemSpencer ↑u
⊢ ↑mulRothNumber (map (mulLeftEmbedding a) s) ≤ ↑mulRothNumber s
case refine'_1.intro.intro.intro
F : Type ?u.143344
α : Type u_1
β : Type ?u.143350
𝕜 : Type ?u.143353
E : Type ?u.143356
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ map (mulLeftEmbedding a) s
hcard : card u = ↑mulRothNumber (map (mulLeftEmbedding a) s)
hu : MulSalemSpencer ↑u
⊢ ↑mulRothNumber (map (mulLeftEmbedding a) s) ≤ ↑mulRothNumber s
rw [subset_map_iff] at hus
case refine'_1.intro.intro.intro.intro.intro
F : Type ?u.143344
α : Type u_1
β : Type ?u.143350
𝕜 : Type ?u.143353
E : Type ?u.143356
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : card (map (mulLeftEmbedding a) u) = ↑mulRothNumber (map (mulLeftEmbedding a) s)
hu : MulSalemSpencer ↑(map (mulLeftEmbedding a) u)
⊢ ↑mulRothNumber (map (mulLeftEmbedding a) s) ≤ ↑mulRothNumber s
case refine'_1.intro.intro.intro
F : Type ?u.143344
α : Type u_1
β : Type ?u.143350
𝕜 : Type ?u.143353
E : Type ?u.143356
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : ∃ u_1 x, u = map (mulLeftEmbedding a) u_1
hcard : card u = ↑mulRothNumber (map (mulLeftEmbedding a) s)
hu : MulSalemSpencer ↑u
⊢ ↑mulRothNumber (map (mulLeftEmbedding a) s) ≤ ↑mulRothNumber s
obtain ⟨u, hus, rfl⟩ := hus
case refine'_1.intro.intro.intro.intro.intro
F : Type ?u.143344
α : Type u_1
β : Type ?u.143350
𝕜 : Type ?u.143353
E : Type ?u.143356
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : card (map (mulLeftEmbedding a) u) = ↑mulRothNumber (map (mulLeftEmbedding a) s)
hu : MulSalemSpencer (↑(mulLeftEmbedding a) '' ↑u)
⊢ ↑mulRothNumber (map (mulLeftEmbedding a) s) ≤ ↑mulRothNumber s
case refine'_1.intro.intro.intro.intro.intro
F : Type ?u.143344
α : Type u_1
β : Type ?u.143350
𝕜 : Type ?u.143353
E : Type ?u.143356
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : card (map (mulLeftEmbedding a) u) = ↑mulRothNumber (map (mulLeftEmbedding a) s)
hu : MulSalemSpencer ↑(map (mulLeftEmbedding a) u)
⊢ ↑mulRothNumber (map (mulLeftEmbedding a) s) ≤ ↑mulRothNumber s
rw [coe_map] at hu
case refine'_1.intro.intro.intro.intro.intro
F : Type ?u.143344
α : Type u_1
β : Type ?u.143350
𝕜 : Type ?u.143353
E : Type ?u.143356
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : card (map (mulLeftEmbedding a) u) = ↑mulRothNumber (map (mulLeftEmbedding a) s)
hu : MulSalemSpencer (↑(mulLeftEmbedding a) '' ↑u)
⊢ card u ≤ ↑mulRothNumber s
case refine'_1.intro.intro.intro.intro.intro
F : Type ?u.143344
α : Type u_1
β : Type ?u.143350
𝕜 : Type ?u.143353
E : Type ?u.143356
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : card (map (mulLeftEmbedding a) u) = ↑mulRothNumber (map (mulLeftEmbedding a) s)
hu : MulSalemSpencer (↑(mulLeftEmbedding a) '' ↑u)
⊢ ↑mulRothNumber (map (mulLeftEmbedding a) s) ≤ ↑mulRothNumber s
rw [← hcard, card_map]
no goals
case refine'_1.intro.intro.intro.intro.intro
F : Type ?u.143344
α : Type u_1
β : Type ?u.143350
𝕜 : Type ?u.143353
E : Type ?u.143356
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : card (map (mulLeftEmbedding a) u) = ↑mulRothNumber (map (mulLeftEmbedding a) s)
hu : MulSalemSpencer (↑(mulLeftEmbedding a) '' ↑u)
⊢ card u ≤ ↑mulRothNumber s
exact (mulSalemSpencer_mul_left_iff.1 hu).le_mulRothNumber hus
case refine'_2.intro.intro.intro
F : Type ?u.143344
α : Type u_1
β : Type ?u.143350
𝕜 : Type ?u.143353
E : Type ?u.143356
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : card u = ↑mulRothNumber s
hu : MulSalemSpencer ↑u
⊢ ↑mulRothNumber s ≤ ↑mulRothNumber (map (mulLeftEmbedding a) s)
case refine'_2
F : Type ?u.143344
α : Type u_1
β : Type ?u.143350
𝕜 : Type ?u.143353
E : Type ?u.143356
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
⊢ ↑mulRothNumber s ≤ ↑mulRothNumber (map (mulLeftEmbedding a) s)
obtain ⟨u, hus, hcard, hu⟩ := mulRothNumber_spec s
case refine'_2.intro.intro.intro
F : Type ?u.143344
α : Type u_1
β : Type ?u.143350
𝕜 : Type ?u.143353
E : Type ?u.143356
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : card u = ↑mulRothNumber s
hu : MulSalemSpencer ↑u
h : MulSalemSpencer ↑(map (mulLeftEmbedding a) u)
⊢ ↑mulRothNumber s ≤ ↑mulRothNumber (map (mulLeftEmbedding a) s)
case refine'_2.intro.intro.intro
F : Type ?u.143344
α : Type u_1
β : Type ?u.143350
𝕜 : Type ?u.143353
E : Type ?u.143356
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : card u = ↑mulRothNumber s
hu : MulSalemSpencer ↑u
⊢ ↑mulRothNumber s ≤ ↑mulRothNumber (map (mulLeftEmbedding a) s)
have h : MulSalemSpencer (u.map <| mulLeftEmbedding a : Set α) := by
  rw [coe_map]
  exact hu.mul_left
case h.e'_3
F : Type ?u.143344
α : Type u_1
β : Type ?u.143350
𝕜 : Type ?u.143353
E : Type ?u.143356
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : card u = ↑mulRothNumber s
hu : MulSalemSpencer ↑u
h : MulSalemSpencer ↑(map (mulLeftEmbedding a) u)
⊢ ↑mulRothNumber s = card (map (mulLeftEmbedding a) u)
case refine'_2.intro.intro.intro
F : Type ?u.143344
α : Type u_1
β : Type ?u.143350
𝕜 : Type ?u.143353
E : Type ?u.143356
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : card u = ↑mulRothNumber s
hu : MulSalemSpencer ↑u
h : MulSalemSpencer ↑(map (mulLeftEmbedding a) u)
⊢ ↑mulRothNumber s ≤ ↑mulRothNumber (map (mulLeftEmbedding a) s)
convert h.le_mulRothNumber (map_subset_map.2 hus) using 1
no goals
case h.e'_3
F : Type ?u.143344
α : Type u_1
β : Type ?u.143350
𝕜 : Type ?u.143353
E : Type ?u.143356
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : card u = ↑mulRothNumber s
hu : MulSalemSpencer ↑u
h : MulSalemSpencer ↑(map (mulLeftEmbedding a) u)
⊢ ↑mulRothNumber s = card (map (mulLeftEmbedding a) u)
rw [card_map, hcard]
F : Type ?u.143344
α : Type u_1
β : Type ?u.143350
𝕜 : Type ?u.143353
E : Type ?u.143356
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : card u = ↑mulRothNumber s
hu : MulSalemSpencer ↑u
⊢ MulSalemSpencer (↑(mulLeftEmbedding a) '' ↑u)
F : Type ?u.143344
α : Type u_1
β : Type ?u.143350
𝕜 : Type ?u.143353
E : Type ?u.143356
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : card u = ↑mulRothNumber s
hu : MulSalemSpencer ↑u
⊢ MulSalemSpencer ↑(map (mulLeftEmbedding a) u)
rw [coe_map]
no goals
F : Type ?u.143344
α : Type u_1
β : Type ?u.143350
𝕜 : Type ?u.143353
E : Type ?u.143356
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : card u = ↑mulRothNumber s
hu : MulSalemSpencer ↑u
⊢ MulSalemSpencer (↑(mulLeftEmbedding a) '' ↑u)
exact hu.mul_left