Lean4
@[to_additive]
theorem exists_finiteIndex_of_leftCoset_cover_aux [DecidableEq (Subgroup G)] (j : ι) (hj : j ∈ s)
(hcovers' : ⋃ i ∈ s.filter (H · = H j), g i • (H i : Set G) ≠ Set.univ) : ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex :=
by
classical
have ⟨n, hn⟩ : ∃ n, n = (s.image H).card := exists_eq
induction n using Nat.strongRec generalizing ι with
| ind n ih =>
-- Every left coset of `H j` is contained in a finite union of
-- left cosets of the other subgroups `H k ≠ H j` of the covering.
have ⟨x, hx⟩ : ∃ (x : G), ∀ i ∈ s, H i = H j → (g i : G ⧸ H i) ≠ ↑x := by
simpa [Set.eq_univ_iff_forall, mem_leftCoset_iff, ← QuotientGroup.eq] using hcovers'
replace hx : ∀ (y : G), y • (H j : Set G) ⊆ ⋃ i ∈ s.filter (H · ≠ H j), (y * x⁻¹ * g i) • (H i : Set G) :=
by
intro y z hz
simp_rw [Finset.mem_filter, Set.mem_iUnion]
have ⟨i, hi, hmem⟩ : ∃ i ∈ s, x * (y⁻¹ * z) ∈ g i • (H i : Set G) := by
simpa using Set.eq_univ_iff_forall.mp hcovers (x * (y⁻¹ * z))
rw [mem_leftCoset_iff, SetLike.mem_coe, ← QuotientGroup.eq] at hmem
refine ⟨i, ⟨hi, fun hij => hx i hi hij ?_⟩, ?_⟩
· rwa [hmem, eq_comm, QuotientGroup.eq, hij, inv_mul_cancel_left, ← SetLike.mem_coe, ← mem_leftCoset_iff]
· simpa [mem_leftCoset_iff, SetLike.mem_coe, QuotientGroup.eq, mul_assoc] using hmem
let κ := ↥(s.filter (H · ≠ H j)) × Option ↥(s.filter (H · = H j))
let f : κ → G
| ⟨k₁, some k₂⟩ => g k₂ * x⁻¹ * g k₁
| ⟨k₁, none⟩ => g k₁
let K (k : κ) : Subgroup G := H k.1.val
have hK' (k : κ) : K k ∈ (s.image H).erase (H j) :=
by
have := Finset.mem_filter.mp k.1.property
exact Finset.mem_erase.mpr ⟨this.2, Finset.mem_image_of_mem H this.1⟩
have hK (k : κ) : K k ≠ H j := ((Finset.mem_erase.mp (hK' k)).left ·)
replace hcovers : ⋃ k ∈ Finset.univ, f k • (K k : Set G) = Set.univ :=
Set.iUnion₂_eq_univ_iff.mpr fun y =>
by
rw [← s.filter_union_filter_neg_eq (H · = H j), Finset.set_biUnion_union] at hcovers
cases (Set.mem_union _ _ _).mp (hcovers.superset (Set.mem_univ y)) with
| inl hy =>
have ⟨k, hk, hy⟩ := Set.mem_iUnion₂.mp hy
have hk' : H k = H j := And.right <| by simpa using hk
have ⟨i, hi, hy⟩ := Set.mem_iUnion₂.mp (hx (g k) (hk' ▸ hy))
exact ⟨⟨⟨i, hi⟩, some ⟨k, hk⟩⟩, Finset.mem_univ _, hy⟩
| inr hy =>
have ⟨i, hi, hy⟩ := Set.mem_iUnion₂.mp hy
exact
⟨⟨⟨i, hi⟩, none⟩, Finset.mem_univ _, hy⟩
-- Let `H k` be one of the subgroups in this covering.
have ⟨k⟩ : Nonempty κ :=
not_isEmpty_iff.mp fun hempty => by
rw [Set.iUnion_of_empty] at hcovers
exact Set.empty_ne_univ hcovers
by_cases hcovers' : ⋃ i ∈ Finset.filter (K · = K k) Finset.univ, f i • (K i : Set G) = Set.univ
· rw [Set.iUnion₂_congr fun i hi => by rw [(Finset.mem_filter.mp hi).right]] at hcovers'
exact
⟨k.1, Finset.mem_of_mem_filter k.1.1 k.1.2, hK k, finiteIndex_of_leftCoset_cover_const hcovers'⟩
-- Otherwise, by the induction hypothesis, one of the subgroups `H k ≠ H j` has finite index.
have hn' : (Finset.univ.image K).card < n :=
hn ▸
by
refine
((Finset.card_le_card fun x => ?_).trans_lt <| Finset.card_erase_lt_of_mem (Finset.mem_image_of_mem H hj))
rw [mem_image_univ_iff_mem_range, Set.mem_range]
exact fun ⟨k, hk⟩ => hk ▸ hK' k
have ⟨k', hk'⟩ := ih _ hn' hcovers k (Finset.mem_univ k) hcovers' rfl
exact ⟨k'.1.1, Finset.mem_of_mem_filter k'.1.1 k'.1.2, hK k', hk'.2.2⟩
