-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
inst_1 : DecidablePred (α := Subgroup G) FiniteIndex
hcovers :
  Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ {i ∈ s | (H i).FiniteIndex} ∪ {a ∈ s | ¬(H a).FiniteIndex}, g i • (↑(H i) : Set G))
    Set.univ
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)
κ : Type (max u_2 u_1) := (i : ↥s) × ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1})
f : (k : κ) → G :=
  fun (k : κ) ↦
    g (↑(k.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) : ι) *
      (↑(↑(k.snd (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) :
            ↥(H (↑k.fst : ι))) :
        G)
K : (k : κ) → Subgroup G :=
  fun (k : κ) ↦
    if
        (H
            (↑(k.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) :
              ι)).FiniteIndex then
      D
    else H (↑(k.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) : ι)
i : ι
pos :
  ∀ (hfi : (H i).FiniteIndex),
    Eq.{u_1 + 1} (α := Set G)
      (⋃ (hx : i ∈ s),
        ⋃ (a :
          ↥(if h : (H (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hx) : ι)).FiniteIndex then
              t (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hx) : ι) ⋯ h
            else {1})),
          ⋃ (_ :
            Membership.mem (γ := Finset κ)
              {a : κ |
                ¬(H
                      (↑(a.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) :
                        ι)).FiniteIndex}
              (Sigma.mk (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))
                (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hx) a)),
            f
                (Sigma.mk (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))
                  (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hx) a) •
              (↑(K
                    (Sigma.mk (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))
                      (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hx) a)) :
                Set G))
      (⋃ (_ : i ∈ {a ∈ s | ¬(H a).FiniteIndex}), g i • (↑(H i) : Set G))
neg :
  ∀ (hfi : ¬(H i).FiniteIndex),
    Eq.{u_1 + 1} (α := Set G)
      (⋃ (hx : i ∈ s),
        ⋃ (a :
          ↥(if h : (H (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hx) : ι)).FiniteIndex then
              t (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hx) : ι) ⋯ h
            else {1})),
          ⋃ (_ :
            Membership.mem (γ := Finset κ)
              {a : κ |
                ¬(H
                      (↑(a.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) :
                        ι)).FiniteIndex}
              (Sigma.mk (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))
                (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hx) a)),
            f
                (Sigma.mk (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))
                  (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hx) a) •
              (↑(K
                    (Sigma.mk (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))
                      (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hx) a)) :
                Set G))
      (⋃ (_ : i ∈ {a ∈ s | ¬(H a).FiniteIndex}), g i • (↑(H i) : Set G))
⊢ Eq.{u_1 + 1} (α := Set G)
    (⋃ (hx : i ∈ s),
      ⋃ (a :
        ↥(if h : (H (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hx) : ι)).FiniteIndex then
            t (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hx) : ι) ⋯ h
          else {1})),
        ⋃ (_ :
          Membership.mem (γ := Finset κ)
            {a : κ |
              ¬(H
                    (↑(a.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) :
                      ι)).FiniteIndex}
            (Sigma.mk (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))
              (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hx) a)),
          f
              (Sigma.mk (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))
                (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hx) a) •
            (↑(K
                  (Sigma.mk (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))
                    (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hx) a)) :
              Set G))
    (⋃ (_ : i ∈ {a ∈ s | ¬(H a).FiniteIndex}), g i • (↑(H i) : Set G))

Tactic:
by_cases hfi : (H i).FiniteIndex

Premises used: Subgroup.FiniteIndex