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
α : 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
obtain ⟨u, hu, hCmax⟩ := C.exists_maximal (filter_nonempty_iff.2
  ⟨∅, empty_mem_powerset _, by rw [coe_empty]; exact Set.pairwiseDisjoint_empty⟩)
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
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
rw [mem_filter, mem_powerset] at hu
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
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
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 ↦ _⟩
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)
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
rw [mul_div_assoc]
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)

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)
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)
by_cases hau : a ∈ u
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)

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)
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)
by_cases H : ∀ b ∈ u, Disjoint (a • t) (b • t)
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)
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)
push_neg at H
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)
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)
simp_rw [not_disjoint_iff, ← inv_smul_mem_iff] at H
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)
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)
obtain ⟨b, hb, c, hc₁, hc₂⟩ := H
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
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)
refine' mem_mul.2 ⟨b, a / b, hb, _, by simp⟩
no goals
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
exact mem_div.2 ⟨_, _, hc₂, hc₁, by simp [div_eq_mul_inv a b, mul_comm]⟩
α : 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
α : 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
rw [coe_empty]
no goals
α : 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
exact Set.pairwiseDisjoint_empty
no goals
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)
exact subset_mul_left _ ht.one_mem_div hau
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
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)
refine' (hCmax _ _ <| ssubset_insert hau).elim
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
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
rw [mem_filter, mem_powerset, insert_subset, coe_insert]
no goals
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
exact ⟨⟨ha, hu.1⟩, hu.2.insert fun _ hb _ ↦ H _ hb⟩
no goals
α : 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
simp
no goals
α : 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
simp [div_eq_mul_inv a b, mul_comm]