-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (goal)
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑(H i) : Set G)) Set.univ
inst_1 : DecidablePred (α := Subgroup G) FiniteIndex
let let₁ let₂ :
  Eq.{u_1 + 1} (α := Set G) (⋃ k ∈ {i ∈ s | (H i).FiniteIndex}, g k • (↑(H k) : Set G)) Set.univ ∧
    LE.le (α := ℚ) 1 (∑ i ∈ s, (↑(H i).index : ℚ)⁻¹) ∧
      (Eq (α := ℚ) (∑ i ∈ s, (↑(H i).index : ℚ)⁻¹) 1 →
        Set.PairwiseDisjoint.{u_1, u_2} (α := Set G) (↑({i ∈ s | (H i).FiniteIndex}) : Set ι) fun (i : ι) ↦
          g i • (↑(H i) : Set G))
let₃ :
  let D : Subgroup G := ⨅ k ∈ {i ∈ s | (H i).FiniteIndex}, H k;
  ∀ (hD : D.FiniteIndex),
    Eq.{u_1 + 1} (α := Set G) (⋃ k ∈ {i ∈ s | (H i).FiniteIndex}, g k • (↑(H k) : Set G)) Set.univ ∧
      LE.le (α := ℚ) 1 (∑ i ∈ s, (↑(H i).index : ℚ)⁻¹) ∧
        (Eq (α := ℚ) (∑ i ∈ s, (↑(H i).index : ℚ)⁻¹) 1 →
          Set.PairwiseDisjoint.{u_1, u_2} (α := Set G) (↑({i ∈ s | (H i).FiniteIndex}) : Set ι) fun (i : ι) ↦
            g i • (↑(H i) : Set G))
let₄ :
  let D : Subgroup G := ⨅ k ∈ {i ∈ s | (H i).FiniteIndex}, H k;
  ∀ (hD : D.FiniteIndex) (hD_le : ∀ {i : ι} (hi : i ∈ s) (hfi : (H i).FiniteIndex), D ≤ H i),
    Eq.{u_1 + 1} (α := Set G) (⋃ k ∈ {i ∈ s | (H i).FiniteIndex}, g k • (↑(H k) : Set G)) Set.univ ∧
      LE.le (α := ℚ) 1 (∑ i ∈ s, (↑(H i).index : ℚ)⁻¹) ∧
        (Eq (α := ℚ) (∑ i ∈ s, (↑(H i).index : ℚ)⁻¹) 1 →
          Set.PairwiseDisjoint.{u_1, u_2} (α := Set G) (↑({i ∈ s | (H i).FiniteIndex}) : Set ι) fun (i : ι) ↦
            g i • (↑(H i) : Set G))
⊢ Eq.{u_1 + 1} (α := Set G) (⋃ k ∈ {i ∈ s | (H i).FiniteIndex}, g k • (↑(H k) : Set G)) Set.univ ∧
    LE.le (α := ℚ) 1 (∑ i ∈ s, (↑(H i).index : ℚ)⁻¹) ∧
      (Eq (α := ℚ) (∑ i ∈ s, (↑(H i).index : ℚ)⁻¹) 1 →
        Set.PairwiseDisjoint.{u_1, u_2} (α := Set G) (↑({i ∈ s | (H i).FiniteIndex}) : Set ι) fun (i : ι) ↦
          g i • (↑(H i) : Set G))
have let₅ : let D : Subgroup G := ⨅ k ∈ {i ∈ s | (H i).FiniteIndex}, H k;
∀ (hD : D.FiniteIndex) (hD_le : ∀ {i : ι} (hi : i ∈ s) (hfi : (H i).FiniteIndex), D ≤ H i)
  (t : (i : ι) → (hi : i ∈ s) → (hfi : (H i).FiniteIndex) → Finset ↥(H i))
  (ht :
    ∀ (i : ι) (hi : i ∈ s) (hfi : (H i).FiniteIndex),
      IsComplement (↑(t i hi hfi) : Set ↥(H i)) (↑(D.subgroupOf (H i)) : Set ↥(H i)) ∧
        ⋃ g ∈ t i hi hfi, (↑g : G) • (↑D : Set G) = (↑(H i) : Set G)),
  Eq.{u_1 + 1} (α := Set G) (⋃ k ∈ {i ∈ s | (H i).FiniteIndex}, g k • (↑(H k) : Set G)) Set.univ ∧
    LE.le (α := ℚ) 1 (∑ i ∈ s, (↑(H i).index : ℚ)⁻¹) ∧
      (Eq (α := ℚ) (∑ i ∈ s, (↑(H i).index : ℚ)⁻¹) 1 →
        Set.PairwiseDisjoint.{u_1, u_2} (α := Set G) (↑({i ∈ s | (H i).FiniteIndex}) : Set ι) fun (i : ι) ↦
          g i • (↑(H i) : Set G))
Tactic: classical
  let D := ⨅ k ∈ s.filter (fun i => (H i).FiniteIndex), H k
  -- `D`, as the finite intersection of subgroups of finite index, also has finite index.
  have hD : D.FiniteIndex := finiteIndex_iInf' _ <| by simp
  have hD_le {i} (hi : i ∈ s) (hfi : (H i).FiniteIndex) : D ≤ H i :=
    iInf₂_le i (Finset.mem_filter.mpr ⟨hi, hfi⟩)
  -- Each subgroup of finite index in the covering is the union of finitely many cosets of `D`.
  choose t ht using fun i hi hfi =>
    exists_leftTransversal_of_FiniteIndex (H := H i) (hD_le hi hfi)
  -- We construct a cover of `G` by the cosets of subgroups of infinite index and of `D`.
  let κ := (i : s) × { x // x ∈ if h : (H i.1).FiniteIndex then t i.1 i.2 h else {1} }
  let f (k : κ) : G := g k.1 * k.2.val
  let K (k : κ) : Subgroup G := if (H k.1).FiniteIndex then D else H k.1
  have hcovers' : ⋃ k ∈ Finset.univ, f k • (K k : Set G) = Set.univ := by
    rw [← s.filter_union_filter_not_eq (fun i => (H i).FiniteIndex)] at hcovers
    rw [← hcovers, ← Finset.univ.filter_union_filter_not_eq (fun k => (H k.1).FiniteIndex),
      Finset.set_biUnion_union, Finset.set_biUnion_union]
    apply congrArg₂ (· ∪ ·) <;> rw [Set.iUnion_sigma, Set.iUnion_subtype] <;>
        refine Set.iUnion_congr fun i => ?_
    · by_cases hfi : (H i).FiniteIndex <;>
        simp [← Set.smul_set_iUnion₂, Set.iUnion_subtype, ← leftCoset_assoc, f, K, ht, hfi]
    · by_cases hfi : (H i).FiniteIndex <;>
        simp [Set.iUnion_subtype, f, K, hfi]
  -- There is at least one coset of a subgroup of finite index in the original covering.
  -- Therefore a coset of `D` occurs in the new covering.
  have ⟨k, hkfi, hk⟩ : ∃ k, (H k.1.1).FiniteIndex ∧ K k = D :=
    have ⟨j, hj, hjfi⟩ := exists_finiteIndex_of_leftCoset_cover hcovers
    have ⟨x, hx⟩ : (t j hj hjfi).Nonempty := Finset.nonempty_coe_sort.mp
      (ht j hj hjfi).1.leftQuotientEquiv.symm.nonempty
    ⟨⟨⟨j, hj⟩, ⟨x, dif_pos hjfi ▸ hx⟩⟩, hjfi, if_pos hjfi⟩
  -- Since `D` is the unique subgroup of finite index whose cosets occur in the new covering,
  -- the cosets of the other subgroups can be omitted.
  replace hcovers' : ⋃ i ∈ Finset.univ.filter (K · = D), f i • (D : Set G) = Set.univ := by
    rw [← hk, Set.iUnion₂_congr fun i hi => by rw [← (Finset.mem_filter.mp hi).2]]
    by_contra! h
    obtain ⟨i, -, hi⟩ :=
      exists_finiteIndex_of_leftCoset_cover_aux hcovers' k (Finset.mem_univ k) h
    by_cases hfi : (H i.1.1).FiniteIndex <;> simp [K, hfi, hkfi] at hi
  -- The result follows by restoring the original cosets of subgroups of finite index
  -- from the cosets of `D` into which they have been decomposed.
  have hHD (i) : ¬(H i).FiniteIndex → H i ≠ D := fun hfi hD' => (hD' ▸ hfi) hD
  have hdensity : ∑ i ∈ s, ((H i).index : ℚ)⁻¹ =
      (Finset.univ.filter (K · = D)).card * (D.index : ℚ)⁻¹ := by
    rw [eq_mul_inv_iff_mul_eq₀ (Nat.cast_ne_zero.mpr hD.index_ne_zero), Finset.sum_mul,
      ← Finset.sum_attach, eq_comm, Finset.card_filter, Nat.cast_sum, ← Finset.univ_sigma_univ,
      Finset.sum_sigma, Finset.sum_coe_sort_eq_attach]
    refine Finset.sum_congr rfl fun i _ => ?_
    by_cases hfi : (H i).FiniteIndex
    · rw [← relIndex_mul_index (hD_le i.2 hfi), Nat.cast_mul, mul_comm,
        mul_inv_cancel_right₀ (Nat.cast_ne_zero.mpr hfi.index_ne_zero)]
      simpa [K, hfi] using (ht i.1 i.2 hfi).1.card_left
    · rw [of_not_not (FiniteIndex.mk.mt hfi), Nat.cast_zero, inv_zero, zero_mul]
      simpa [K, hfi] using hHD i hfi
  refine ⟨?_, ?_, ?_⟩
  · rw [← hcovers', Set.iUnion_sigma, Set.iUnion_subtype]
    refine Set.iUnion_congr fun i => ?_
    rw [Finset.mem_filter, Set.iUnion_and]
    refine Set.iUnion_congr fun hi => ?_
    by_cases hfi : (H i).FiniteIndex <;>
      simp [Set.smul_set_iUnion, Set.iUnion_subtype, ← leftCoset_assoc,
        f, K, hHD, ← (ht i hi _).2, hfi]
  · rw [hdensity]
    refine le_of_mul_le_mul_right ?_ (Nat.cast_pos.mpr (Nat.pos_of_ne_zero hD.index_ne_zero))
    rw [one_mul, mul_assoc, inv_mul_cancel₀ (Nat.cast_ne_zero.mpr hD.index_ne_zero), mul_one,
      Nat.cast_le]
    exact index_le_of_leftCoset_cover_const hcovers'
  · rw [hdensity, mul_inv_eq_one₀ (Nat.cast_ne_zero.mpr hD.index_ne_zero),
      Nat.cast_inj, Finset.coe_filter]
    intro h i hi j hj hij c hi' hj' x hx
    have hdisjoint := pairwiseDisjoint_leftCoset_cover_const_of_index_eq hcovers' h.symm
    -- We know the `f k • K k` are pairwise disjoint and need to prove that the `g i • H i` are.
    rw [Set.mem_setOf_eq] at hi hj
    have hk' (i) (hi : i ∈ s ∧ (H i).FiniteIndex) (hi' : c ≤ g i • (H i : Set G)) :
        ∃ (k : κ), k.1.1 = i ∧ K k = D ∧ x ∈ f k • (D : Set G) := by
      rw [← (ht i hi.1 hi.2).2] at hi'
      suffices ∃ r : H i, r ∈ t i hi.1 hi.2 ∧ x ∈ (g i * r) • (D : Set G) by
        have ⟨r, hr, hxr⟩ := this
        refine ⟨⟨⟨i, hi.1⟩, ⟨r, dif_pos hi.2 ▸ hr⟩⟩, rfl, ?_⟩
        simpa [K, f, if_pos hi.2] using hxr
      simpa [Set.mem_smul_set_iff_inv_smul_mem, smul_eq_mul, mul_assoc] using hi' hx
    have ⟨k₁, hik₁, hk₁, hxk₁⟩ := hk' i hi hi'
    have ⟨k₂, hjk₂, hk₂, hxk₂⟩ := hk' j hj hj'
    rw [← Set.singleton_subset_iff, ← Set.le_iff_subset] at hxk₁ hxk₂ ⊢
    exact hdisjoint
      (Finset.mem_filter.mpr ⟨Finset.mem_univ k₁, hk₁⟩)
      (Finset.mem_filter.mpr ⟨Finset.mem_univ k₂, hk₂⟩)
      (ne_of_apply_ne Sigma.fst (ne_of_apply_ne Subtype.val (hik₁ ▸ hjk₂ ▸ hij)))
      hxk₁ hxk₂