-- Mathlib/GroupTheory/CosetCover.lean
theorem leftCoset_cover_filter_FiniteIndex_aux
    [DecidablePred (FiniteIndex : Subgroup G → Prop)] :
    (⋃ k ∈ s.filter (fun i => (H i).FiniteIndex), g k • (H k : Set G) = Set.univ) ∧
      (1 ≤ ∑ i ∈ s, ((H i).index : ℚ)⁻¹) ∧
      (∑ i ∈ s, ((H i).index : ℚ)⁻¹ = 1 → Set.PairwiseDisjoint
        (s.filter (fun i => (H i).FiniteIndex)) (fun i ↦ g i • (H i : Set G)))

Proof state:
case refine_3
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
inst✝ : DecidablePred FiniteIndex
D : Subgroup G := ⨅ k ∈ Finset.filter (fun i => (H i).FiniteIndex) s, H k
hD : D.FiniteIndex
hD_le : ∀ {i : ι}, i ∈ s → (H i).FiniteIndex → D ≤ H i
t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i)
ht :
  ∀ (i : ι) (hi : i ∈ s) (hfi : (H i).FiniteIndex),
    IsComplement ↑(t i hi hfi) ↑(D.subgroupOf (H i)) ∧ ⋃ g ∈ t i hi hfi, ↑g • ↑D = ↑(H i)
κ : Type (max u_2 u_1) := (i : { x // x ∈ s }) × { x // x ∈ if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {1} }
f : κ → G := fun k => g ↑k.fst * ↑↑k.snd
K : κ → Subgroup G := fun k => if (H ↑k.fst).FiniteIndex then D else H ↑k.fst
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
hcovers' : ⋃ i ∈ Finset.filter (fun x => K x = D) Finset.univ, f i • ↑D = Set.univ
hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
hdensity : ∑ i ∈ s, (↑(H i).index)⁻¹ = ↑(Finset.filter (fun x => K x = D) Finset.univ).card * (↑D.index)⁻¹
h : (Finset.filter (fun x => K x = D) Finset.univ).card = D.index
i : ι
hi : i ∈ s ∧ (H i).FiniteIndex
j : ι
hj : j ∈ s ∧ (H j).FiniteIndex
hij : i ≠ j
c : Set G
hi' : c ≤ (fun i => g i • ↑(H i)) i
hj' : c ≤ (fun i => g i • ↑(H i)) j
x : G
hx : x ∈ c
hdisjoint : (↑(Finset.filter (fun x => K x = D) Finset.univ)).PairwiseDisjoint fun x => f x • ↑D
⊢ x ∈ ⊥

Tactic:
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

Result:
case refine_3
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
inst✝ : DecidablePred FiniteIndex
D : Subgroup G := ⨅ k ∈ Finset.filter (fun i => (H i).FiniteIndex) s, H k
hD : D.FiniteIndex
hD_le : ∀ {i : ι}, i ∈ s → (H i).FiniteIndex → D ≤ H i
t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i)
ht :
  ∀ (i : ι) (hi : i ∈ s) (hfi : (H i).FiniteIndex),
    IsComplement ↑(t i hi hfi) ↑(D.subgroupOf (H i)) ∧ ⋃ g ∈ t i hi hfi, ↑g • ↑D = ↑(H i)
κ : Type (max u_2 u_1) := (i : { x // x ∈ s }) × { x // x ∈ if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {1} }
f : κ → G := fun k => g ↑k.fst * ↑↑k.snd
K : κ → Subgroup G := fun k => if (H ↑k.fst).FiniteIndex then D else H ↑k.fst
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
hcovers' : ⋃ i ∈ Finset.filter (fun x => K x = D) Finset.univ, f i • ↑D = Set.univ
hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
hdensity : ∑ i ∈ s, (↑(H i).index)⁻¹ = ↑(Finset.filter (fun x => K x = D) Finset.univ).card * (↑D.index)⁻¹
h : (Finset.filter (fun x => K x = D) Finset.univ).card = D.index
i : ι
hi : i ∈ s ∧ (H i).FiniteIndex
j : ι
hj : j ∈ s ∧ (H j).FiniteIndex
hij : i ≠ j
c : Set G
hi' : c ≤ (fun i => g i • ↑(H i)) i
hj' : c ≤ (fun i => g i • ↑(H i)) j
x : G
hx : x ∈ c
hdisjoint : (↑(Finset.filter (fun x => K x = D) Finset.univ)).PairwiseDisjoint fun x => f x • ↑D
hk' : ∀ (i : ι), i ∈ s ∧ (H i).FiniteIndex → c ≤ g i • ↑(H i) → ∃ k, ↑k.fst = i ∧ K k = D ∧ x ∈ f k • ↑D
⊢ x ∈ ⊥

Proof state:
case refine_3
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
inst✝ : DecidablePred FiniteIndex
D : Subgroup G := ⨅ k ∈ Finset.filter (fun i => (H i).FiniteIndex) s, H k
hD : D.FiniteIndex
hD_le : ∀ {i : ι}, i ∈ s → (H i).FiniteIndex → D ≤ H i
t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i)
ht :
  ∀ (i : ι) (hi : i ∈ s) (hfi : (H i).FiniteIndex),
    IsComplement ↑(t i hi hfi) ↑(D.subgroupOf (H i)) ∧ ⋃ g ∈ t i hi hfi, ↑g • ↑D = ↑(H i)
κ : Type (max u_2 u_1) := (i : { x // x ∈ s }) × { x // x ∈ if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {1} }
f : κ → G := fun k => g ↑k.fst * ↑↑k.snd
K : κ → Subgroup G := fun k => if (H ↑k.fst).FiniteIndex then D else H ↑k.fst
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
hcovers' : ⋃ i ∈ Finset.filter (fun x => K x = D) Finset.univ, f i • ↑D = Set.univ
hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
hdensity : ∑ i ∈ s, (↑(H i).index)⁻¹ = ↑(Finset.filter (fun x => K x = D) Finset.univ).card * (↑D.index)⁻¹
⊢ (Finset.filter (fun x => K x = D) Finset.univ).card = D.index →
    {x | x ∈ s ∧ (H x).FiniteIndex}.PairwiseDisjoint fun i => g i • ↑(H i)

Tactic:
intro h i hi j hj hij c hi' hj' x hx

Result:
case refine_3
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
inst✝ : DecidablePred FiniteIndex
D : Subgroup G := ⨅ k ∈ Finset.filter (fun i => (H i).FiniteIndex) s, H k
hD : D.FiniteIndex
hD_le : ∀ {i : ι}, i ∈ s → (H i).FiniteIndex → D ≤ H i
t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i)
ht :
  ∀ (i : ι) (hi : i ∈ s) (hfi : (H i).FiniteIndex),
    IsComplement ↑(t i hi hfi) ↑(D.subgroupOf (H i)) ∧ ⋃ g ∈ t i hi hfi, ↑g • ↑D = ↑(H i)
κ : Type (max u_2 u_1) := (i : { x // x ∈ s }) × { x // x ∈ if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {1} }
f : κ → G := fun k => g ↑k.fst * ↑↑k.snd
K : κ → Subgroup G := fun k => if (H ↑k.fst).FiniteIndex then D else H ↑k.fst
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
hcovers' : ⋃ i ∈ Finset.filter (fun x => K x = D) Finset.univ, f i • ↑D = Set.univ
hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
hdensity : ∑ i ∈ s, (↑(H i).index)⁻¹ = ↑(Finset.filter (fun x => K x = D) Finset.univ).card * (↑D.index)⁻¹
h : (Finset.filter (fun x => K x = D) Finset.univ).card = D.index
i : ι
hi : i ∈ {x | x ∈ s ∧ (H x).FiniteIndex}
j : ι
hj : j ∈ {x | x ∈ s ∧ (H x).FiniteIndex}
hij : i ≠ j
c : Set G
hi' : c ≤ (fun i => g i • ↑(H i)) i
hj' : c ≤ (fun i => g i • ↑(H i)) j
x : G
hx : x ∈ c
⊢ x ∈ ⊥