-- 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
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
this : ∃ r ∈ t i ⋯ ⋯, x ∈ (g i * ↑r) • ↑D
r : ↥(H i)
hr : r ∈ t i ⋯ ⋯
hxr : x ∈ (g i * ↑r) • ↑D
⊢ ∃ k, ↑k.fst = i ∧ K k = D ∧ x ∈ f k • ↑D

Tactic:
refine ⟨⟨⟨i, hi.1⟩, ⟨r, dif_pos hi.2 ▸ hr⟩⟩, rfl, ?_⟩

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
this : ∃ r ∈ t i ⋯ ⋯, x ∈ (g i * ↑r) • ↑D
r : ↥(H i)
hr : r ∈ t i ⋯ ⋯
hxr : x ∈ (g i * ↑r) • ↑D
⊢ K ⟨⟨i, ⋯⟩, ⟨r, ⋯⟩⟩ = D ∧ x ∈ f ⟨⟨i, ⋯⟩, ⟨r, ⋯⟩⟩ • ↑D

Proof state:
case hx
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
inst✝ : DecidablePred FiniteIndex
hcovers :
  ⋃ i ∈ Finset.filter (fun i => (H i).FiniteIndex) s ∪ Finset.filter (fun a => ¬(H a).FiniteIndex) s, g i • ↑(H i) =
    Set.univ
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
i : ι
⊢ ⋃ (hx : i ∈ s),
      ⋃ a,
        ⋃ (_ : ⟨⟨i, hx⟩, a⟩ ∈ Finset.filter (fun k => (H ↑k.fst).FiniteIndex) Finset.univ),
          f ⟨⟨i, hx⟩, a⟩ • ↑(K ⟨⟨i, hx⟩, a⟩) =
    ⋃ (_ : i ∈ Finset.filter (fun i => (H i).FiniteIndex) s), g i • ↑(H i)

Tactic:
by_cases hfi : (H i).FiniteIndex <;>
  simp [← Set.smul_set_iUnion₂, Set.iUnion_subtype, ← leftCoset_assoc, f, K, ht, hfi]

Result:
no goals

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

Tactic:
by_cases hfi : (H i).FiniteIndex <;>
  simp [Set.smul_set_iUnion, Set.iUnion_subtype, ← leftCoset_assoc,
    f, K, hHD, ← (ht i hi _).2, hi, hfi, hkfi]

Result:
no goals

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
⊢ ∀ i ∈ Finset.filter (fun i => (H i).FiniteIndex) s, (H i).FiniteIndex

Tactic:
simp

Result:
no goals