case intro.intro.intro
F : Type ?u.142257
α : Type u_1
β : Type ?u.142263
𝕜 : Type ?u.142266
E : Type ?u.142269
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s t✝ : Finset α
n : ℕ
h : ∀ (t : Finset α), t ∈ powersetLen n s → ¬MulSalemSpencer ↑t
t : Finset α
hts : t ⊆ s
hcard : card t = ↑mulRothNumber s
ht : MulSalemSpencer ↑t
⊢ ↑mulRothNumber s < n
F : Type ?u.142257
α : Type u_1
β : Type ?u.142263
𝕜 : Type ?u.142266
E : Type ?u.142269
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s t : Finset α
n : ℕ
h : ∀ (t : Finset α), t ∈ powersetLen n s → ¬MulSalemSpencer ↑t
⊢ ↑mulRothNumber s < n
obtain ⟨t, hts, hcard, ht⟩ := mulRothNumber_spec s
case intro.intro.intro
F : Type ?u.142257
α : Type u_1
β : Type ?u.142263
𝕜 : Type ?u.142266
E : Type ?u.142269
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s t✝ : Finset α
n : ℕ
h : ∀ (t : Finset α), t ∈ powersetLen n s → ¬MulSalemSpencer ↑t
t : Finset α
hts : t ⊆ s
hcard : card t = ↑mulRothNumber s
ht : MulSalemSpencer ↑t
⊢ ¬n ≤ card t
case intro.intro.intro
F : Type ?u.142257
α : Type u_1
β : Type ?u.142263
𝕜 : Type ?u.142266
E : Type ?u.142269
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s t✝ : Finset α
n : ℕ
h : ∀ (t : Finset α), t ∈ powersetLen n s → ¬MulSalemSpencer ↑t
t : Finset α
hts : t ⊆ s
hcard : card t = ↑mulRothNumber s
ht : MulSalemSpencer ↑t
⊢ ↑mulRothNumber s < n
rw [← hcard, ← not_le]
case intro.intro.intro
F : Type ?u.142257
α : Type u_1
β : Type ?u.142263
𝕜 : Type ?u.142266
E : Type ?u.142269
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s t✝ : Finset α
n : ℕ
h : ∀ (t : Finset α), t ∈ powersetLen n s → ¬MulSalemSpencer ↑t
t : Finset α
hts : t ⊆ s
hcard : card t = ↑mulRothNumber s
ht : MulSalemSpencer ↑t
hn : n ≤ card t
⊢ False
case intro.intro.intro
F : Type ?u.142257
α : Type u_1
β : Type ?u.142263
𝕜 : Type ?u.142266
E : Type ?u.142269
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s t✝ : Finset α
n : ℕ
h : ∀ (t : Finset α), t ∈ powersetLen n s → ¬MulSalemSpencer ↑t
t : Finset α
hts : t ⊆ s
hcard : card t = ↑mulRothNumber s
ht : MulSalemSpencer ↑t
⊢ ¬n ≤ card t
intro hn
case intro.intro.intro.intro.intro
F : Type ?u.142257
α : Type u_1
β : Type ?u.142263
𝕜 : Type ?u.142266
E : Type ?u.142269
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s t✝ t : Finset α
hts : t ⊆ s
hcard : card t = ↑mulRothNumber s
ht : MulSalemSpencer ↑t
u : Finset α
hut : u ⊆ t
h : ∀ (t : Finset α), t ∈ powersetLen (card u) s → ¬MulSalemSpencer ↑t
hn : card u ≤ card t
⊢ False
case intro.intro.intro
F : Type ?u.142257
α : Type u_1
β : Type ?u.142263
𝕜 : Type ?u.142266
E : Type ?u.142269
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s t✝ : Finset α
n : ℕ
h : ∀ (t : Finset α), t ∈ powersetLen n s → ¬MulSalemSpencer ↑t
t : Finset α
hts : t ⊆ s
hcard : card t = ↑mulRothNumber s
ht : MulSalemSpencer ↑t
hn : n ≤ card t
⊢ False
obtain ⟨u, hut, rfl⟩ := exists_smaller_set t n hn
no goals
case intro.intro.intro.intro.intro
F : Type ?u.142257
α : Type u_1
β : Type ?u.142263
𝕜 : Type ?u.142266
E : Type ?u.142269
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s t✝ t : Finset α
hts : t ⊆ s
hcard : card t = ↑mulRothNumber s
ht : MulSalemSpencer ↑t
u : Finset α
hut : u ⊆ t
h : ∀ (t : Finset α), t ∈ powersetLen (card u) s → ¬MulSalemSpencer ↑t
hn : card u ≤ card t
⊢ False
exact h _ (mem_powersetLen.2 ⟨hut.trans hts, rfl⟩) (ht.mono hut)