[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
s t : Finset α
ht : Finset.Nonempty t
⊢ ∃ u, card u * card t ≤ card (s * t) ∧ s ⊆ u * t / t
[PROOFSTEP]
haveI : ∀ u, Decidable ((u : Set α).PairwiseDisjoint (· • t)) := fun u ↦ Classical.dec _
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
s t : Finset α
ht : Finset.Nonempty t
this : (u : Set α) → Decidable (Set.PairwiseDisjoint u fun x => x • t)
⊢ ∃ u, card u * card t ≤ card (s * t) ∧ s ⊆ u * t / t
[PROOFSTEP]
set C := s.powerset.filter fun u ↦ u.toSet.PairwiseDisjoint (· • t)
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
s t : Finset α
ht : Finset.Nonempty t
this : (u : Set α) → Decidable (Set.PairwiseDisjoint u fun x => x • t)
C : Finset (Finset α) := filter (fun u => Set.PairwiseDisjoint ↑u fun x => x • t) (powerset s)
⊢ ∃ u, card u * card t ≤ card (s * t) ∧ s ⊆ u * t / t
[PROOFSTEP]
obtain ⟨u, hu, hCmax⟩ :=
  C.exists_maximal
    (filter_nonempty_iff.2 ⟨∅, empty_mem_powerset _, by rw [coe_empty]; exact Set.pairwiseDisjoint_empty⟩)
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
s t : Finset α
ht : Finset.Nonempty t
this : (u : Set α) → Decidable (Set.PairwiseDisjoint u fun x => x • t)
C : Finset (Finset α) := filter (fun u => Set.PairwiseDisjoint ↑u fun x => x • t) (powerset s)
⊢ Set.PairwiseDisjoint ↑∅ fun x => x • t
[PROOFSTEP]
rw [coe_empty]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
s t : Finset α
ht : Finset.Nonempty t
this : (u : Set α) → Decidable (Set.PairwiseDisjoint u fun x => x • t)
C : Finset (Finset α) := filter (fun u => Set.PairwiseDisjoint ↑u fun x => x • t) (powerset s)
⊢ Set.PairwiseDisjoint ∅ fun x => x • t
[PROOFSTEP]
exact Set.pairwiseDisjoint_empty
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
s t : Finset α
ht : Finset.Nonempty t
this : (u : Set α) → Decidable (Set.PairwiseDisjoint u fun x => x • t)
C : Finset (Finset α) := filter (fun u => Set.PairwiseDisjoint ↑u fun x => x • t) (powerset s)
u : Finset α
hu : u ∈ C
hCmax : ∀ (x : Finset α), x ∈ C → ¬u < x
⊢ ∃ u, card u * card t ≤ card (s * t) ∧ s ⊆ u * t / t
[PROOFSTEP]
rw [mem_filter, mem_powerset] at hu 
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
s t : Finset α
ht : Finset.Nonempty t
this : (u : Set α) → Decidable (Set.PairwiseDisjoint u fun x => x • t)
C : Finset (Finset α) := filter (fun u => Set.PairwiseDisjoint ↑u fun x => x • t) (powerset s)
u : Finset α
hu : u ⊆ s ∧ Set.PairwiseDisjoint ↑u fun x => x • t
hCmax : ∀ (x : Finset α), x ∈ C → ¬u < x
⊢ ∃ u, card u * card t ≤ card (s * t) ∧ s ⊆ u * t / t
[PROOFSTEP]
refine'
  ⟨u, (card_mul_iff.2 <| pairwiseDisjoint_smul_iff.1 hu.2).ge.trans (card_le_of_subset <| mul_subset_mul_right hu.1),
    fun a ha ↦ _⟩
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
s t : Finset α
ht : Finset.Nonempty t
this : (u : Set α) → Decidable (Set.PairwiseDisjoint u fun x => x • t)
C : Finset (Finset α) := filter (fun u => Set.PairwiseDisjoint ↑u fun x => x • t) (powerset s)
u : Finset α
hu : u ⊆ s ∧ Set.PairwiseDisjoint ↑u fun x => x • t
hCmax : ∀ (x : Finset α), x ∈ C → ¬u < x
a : α
ha : a ∈ s
⊢ a ∈ u * t / t
[PROOFSTEP]
rw [mul_div_assoc]
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
s t : Finset α
ht : Finset.Nonempty t
this : (u : Set α) → Decidable (Set.PairwiseDisjoint u fun x => x • t)
C : Finset (Finset α) := filter (fun u => Set.PairwiseDisjoint ↑u fun x => x • t) (powerset s)
u : Finset α
hu : u ⊆ s ∧ Set.PairwiseDisjoint ↑u fun x => x • t
hCmax : ∀ (x : Finset α), x ∈ C → ¬u < x
a : α
ha : a ∈ s
⊢ a ∈ u * (t / t)
[PROOFSTEP]
by_cases hau : a ∈ u
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
s t : Finset α
ht : Finset.Nonempty t
this : (u : Set α) → Decidable (Set.PairwiseDisjoint u fun x => x • t)
C : Finset (Finset α) := filter (fun u => Set.PairwiseDisjoint ↑u fun x => x • t) (powerset s)
u : Finset α
hu : u ⊆ s ∧ Set.PairwiseDisjoint ↑u fun x => x • t
hCmax : ∀ (x : Finset α), x ∈ C → ¬u < x
a : α
ha : a ∈ s
hau : a ∈ u
⊢ a ∈ u * (t / t)
[PROOFSTEP]
exact subset_mul_left _ ht.one_mem_div hau
[GOAL]
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
s t : Finset α
ht : Finset.Nonempty t
this : (u : Set α) → Decidable (Set.PairwiseDisjoint u fun x => x • t)
C : Finset (Finset α) := filter (fun u => Set.PairwiseDisjoint ↑u fun x => x • t) (powerset s)
u : Finset α
hu : u ⊆ s ∧ Set.PairwiseDisjoint ↑u fun x => x • t
hCmax : ∀ (x : Finset α), x ∈ C → ¬u < x
a : α
ha : a ∈ s
hau : ¬a ∈ u
⊢ a ∈ u * (t / t)
[PROOFSTEP]
by_cases H : ∀ b ∈ u, Disjoint (a • t) (b • t)
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
s t : Finset α
ht : Finset.Nonempty t
this : (u : Set α) → Decidable (Set.PairwiseDisjoint u fun x => x • t)
C : Finset (Finset α) := filter (fun u => Set.PairwiseDisjoint ↑u fun x => x • t) (powerset s)
u : Finset α
hu : u ⊆ s ∧ Set.PairwiseDisjoint ↑u fun x => x • t
hCmax : ∀ (x : Finset α), x ∈ C → ¬u < x
a : α
ha : a ∈ s
hau : ¬a ∈ u
H : ∀ (b : α), b ∈ u → Disjoint (a • t) (b • t)
⊢ a ∈ u * (t / t)
[PROOFSTEP]
refine' (hCmax _ _ <| ssubset_insert hau).elim
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
s t : Finset α
ht : Finset.Nonempty t
this : (u : Set α) → Decidable (Set.PairwiseDisjoint u fun x => x • t)
C : Finset (Finset α) := filter (fun u => Set.PairwiseDisjoint ↑u fun x => x • t) (powerset s)
u : Finset α
hu : u ⊆ s ∧ Set.PairwiseDisjoint ↑u fun x => x • t
hCmax : ∀ (x : Finset α), x ∈ C → ¬u < x
a : α
ha : a ∈ s
hau : ¬a ∈ u
H : ∀ (b : α), b ∈ u → Disjoint (a • t) (b • t)
⊢ insert a u ∈ C
[PROOFSTEP]
rw [mem_filter, mem_powerset, insert_subset_iff, coe_insert]
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
s t : Finset α
ht : Finset.Nonempty t
this : (u : Set α) → Decidable (Set.PairwiseDisjoint u fun x => x • t)
C : Finset (Finset α) := filter (fun u => Set.PairwiseDisjoint ↑u fun x => x • t) (powerset s)
u : Finset α
hu : u ⊆ s ∧ Set.PairwiseDisjoint ↑u fun x => x • t
hCmax : ∀ (x : Finset α), x ∈ C → ¬u < x
a : α
ha : a ∈ s
hau : ¬a ∈ u
H : ∀ (b : α), b ∈ u → Disjoint (a • t) (b • t)
⊢ (a ∈ s ∧ u ⊆ s) ∧ Set.PairwiseDisjoint (insert a ↑u) fun x => x • t
[PROOFSTEP]
exact ⟨⟨ha, hu.1⟩, hu.2.insert fun _ hb _ ↦ H _ hb⟩
[GOAL]
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
s t : Finset α
ht : Finset.Nonempty t
this : (u : Set α) → Decidable (Set.PairwiseDisjoint u fun x => x • t)
C : Finset (Finset α) := filter (fun u => Set.PairwiseDisjoint ↑u fun x => x • t) (powerset s)
u : Finset α
hu : u ⊆ s ∧ Set.PairwiseDisjoint ↑u fun x => x • t
hCmax : ∀ (x : Finset α), x ∈ C → ¬u < x
a : α
ha : a ∈ s
hau : ¬a ∈ u
H : ¬∀ (b : α), b ∈ u → Disjoint (a • t) (b • t)
⊢ a ∈ u * (t / t)
[PROOFSTEP]
push_neg at H 
[GOAL]
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
s t : Finset α
ht : Finset.Nonempty t
this : (u : Set α) → Decidable (Set.PairwiseDisjoint u fun x => x • t)
C : Finset (Finset α) := filter (fun u => Set.PairwiseDisjoint ↑u fun x => x • t) (powerset s)
u : Finset α
hu : u ⊆ s ∧ Set.PairwiseDisjoint ↑u fun x => x • t
hCmax : ∀ (x : Finset α), x ∈ C → ¬u < x
a : α
ha : a ∈ s
hau : ¬a ∈ u
H : ∃ b, b ∈ u ∧ ¬Disjoint (a • t) (b • t)
⊢ a ∈ u * (t / t)
[PROOFSTEP]
simp_rw [not_disjoint_iff, ← inv_smul_mem_iff] at H 
[GOAL]
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
s t : Finset α
ht : Finset.Nonempty t
this : (u : Set α) → Decidable (Set.PairwiseDisjoint u fun x => x • t)
C : Finset (Finset α) := filter (fun u => Set.PairwiseDisjoint ↑u fun x => x • t) (powerset s)
u : Finset α
hu : u ⊆ s ∧ Set.PairwiseDisjoint ↑u fun x => x • t
hCmax : ∀ (x : Finset α), x ∈ C → ¬u < x
a : α
ha : a ∈ s
hau : ¬a ∈ u
H : ∃ b, b ∈ u ∧ ∃ a_1, a⁻¹ • a_1 ∈ t ∧ b⁻¹ • a_1 ∈ t
⊢ a ∈ u * (t / t)
[PROOFSTEP]
obtain ⟨b, hb, c, hc₁, hc₂⟩ := H
[GOAL]
case neg.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
s t : Finset α
ht : Finset.Nonempty t
this : (u : Set α) → Decidable (Set.PairwiseDisjoint u fun x => x • t)
C : Finset (Finset α) := filter (fun u => Set.PairwiseDisjoint ↑u fun x => x • t) (powerset s)
u : Finset α
hu : u ⊆ s ∧ Set.PairwiseDisjoint ↑u fun x => x • t
hCmax : ∀ (x : Finset α), x ∈ C → ¬u < x
a : α
ha : a ∈ s
hau : ¬a ∈ u
b : α
hb : b ∈ u
c : α
hc₁ : a⁻¹ • c ∈ t
hc₂ : b⁻¹ • c ∈ t
⊢ a ∈ u * (t / t)
[PROOFSTEP]
refine' mem_mul.2 ⟨b, a / b, hb, _, by simp⟩
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
s t : Finset α
ht : Finset.Nonempty t
this : (u : Set α) → Decidable (Set.PairwiseDisjoint u fun x => x • t)
C : Finset (Finset α) := filter (fun u => Set.PairwiseDisjoint ↑u fun x => x • t) (powerset s)
u : Finset α
hu : u ⊆ s ∧ Set.PairwiseDisjoint ↑u fun x => x • t
hCmax : ∀ (x : Finset α), x ∈ C → ¬u < x
a : α
ha : a ∈ s
hau : ¬a ∈ u
b : α
hb : b ∈ u
c : α
hc₁ : a⁻¹ • c ∈ t
hc₂ : b⁻¹ • c ∈ t
⊢ b * (a / b) = a
[PROOFSTEP]
simp
[GOAL]
case neg.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
s t : Finset α
ht : Finset.Nonempty t
this : (u : Set α) → Decidable (Set.PairwiseDisjoint u fun x => x • t)
C : Finset (Finset α) := filter (fun u => Set.PairwiseDisjoint ↑u fun x => x • t) (powerset s)
u : Finset α
hu : u ⊆ s ∧ Set.PairwiseDisjoint ↑u fun x => x • t
hCmax : ∀ (x : Finset α), x ∈ C → ¬u < x
a : α
ha : a ∈ s
hau : ¬a ∈ u
b : α
hb : b ∈ u
c : α
hc₁ : a⁻¹ • c ∈ t
hc₂ : b⁻¹ • c ∈ t
⊢ a / b ∈ t / t
[PROOFSTEP]
exact mem_div.2 ⟨_, _, hc₂, hc₁, by simp [div_eq_mul_inv a b, mul_comm]⟩
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
s t : Finset α
ht : Finset.Nonempty t
this : (u : Set α) → Decidable (Set.PairwiseDisjoint u fun x => x • t)
C : Finset (Finset α) := filter (fun u => Set.PairwiseDisjoint ↑u fun x => x • t) (powerset s)
u : Finset α
hu : u ⊆ s ∧ Set.PairwiseDisjoint ↑u fun x => x • t
hCmax : ∀ (x : Finset α), x ∈ C → ¬u < x
a : α
ha : a ∈ s
hau : ¬a ∈ u
b : α
hb : b ∈ u
c : α
hc₁ : a⁻¹ • c ∈ t
hc₂ : b⁻¹ • c ∈ t
⊢ b⁻¹ • c / a⁻¹ • c = a / b
[PROOFSTEP]
simp [div_eq_mul_inv a b, mul_comm]
