-- 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:
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
⊢ ⋃ k ∈ Finset.filter (fun i => (H i).FiniteIndex) s, g k • ↑(H k) = Set.univ ∧
    1 ≤ ∑ i ∈ s, (↑(H i).index)⁻¹ ∧
      (∑ i ∈ s, (↑(H i).index)⁻¹ = 1 →
        (↑(Finset.filter (fun i => (H i).FiniteIndex) s)).PairwiseDisjoint fun i => g i • ↑(H i))

Tactic:
let D := ⨅ k ∈ s.filter (fun i => (H i).FiniteIndex), H k

Result:
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
⊢ ⋃ k ∈ Finset.filter (fun i => (H i).FiniteIndex) s, g k • ↑(H k) = Set.univ ∧
    1 ≤ ∑ i ∈ s, (↑(H i).index)⁻¹ ∧
      (∑ i ∈ s, (↑(H i).index)⁻¹ = 1 →
        (↑(Finset.filter (fun i => (H i).FiniteIndex) s)).PairwiseDisjoint fun i => g i • ↑(H i))

Proof state:
case refine_1
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)⁻¹
i : ι
⊢ ⋃ (_ : i ∈ Finset.filter (fun i => (H i).FiniteIndex) s), g i • ↑(H i) =
    ⋃ (hx : i ∈ s), ⋃ a, ⋃ (_ : ⟨⟨i, hx⟩, a⟩ ∈ Finset.filter (fun x => K x = D) Finset.univ), f ⟨⟨i, hx⟩, a⟩ • ↑D

Tactic:
rw [Finset.mem_filter, Set.iUnion_and]

Result:
case refine_1
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)⁻¹
i : ι
⊢ ⋃ (_ : i ∈ s), ⋃ (_ : (H i).FiniteIndex), g i • ↑(H i) =
    ⋃ (hx : i ∈ s), ⋃ a, ⋃ (_ : ⟨⟨i, hx⟩, a⟩ ∈ Finset.filter (fun x => K x = D) Finset.univ), f ⟨⟨i, hx⟩, a⟩ • ↑D

Proof state:
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
i : ι
hi : i ∈ s ∧ (H i).FiniteIndex
hi' : c ≤ g i • ⋃ g ∈ t i ⋯ ⋯, ↑g • ↑D
⊢ ∃ k, ↑k.fst = i ∧ K k = D ∧ x ∈ f k • ↑D

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

Result:
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
i : ι
hi : i ∈ s ∧ (H i).FiniteIndex
hi' : c ≤ g i • ⋃ g ∈ t i ⋯ ⋯, ↑g • ↑D
⊢ ∃ r ∈ t i ⋯ ⋯, x ∈ (g i * ↑r) • ↑D