awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.CosetCover
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
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
choose :
  ∀ (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))
⊢ 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:
choose t ht using fun i hi hfi =>
    exists_leftTransversal_of_FiniteIndex (H := H i) (hD_le hi hfi)

Premises used: Subgroup.exists_leftTransversal_of_FiniteIndex
-- 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}))) : ι)
rw :
  Eq.{u_1 + 1} (α := Set G)
    ((⋃ (x : κ),
        ⋃ (_ :
          Membership.mem (γ := Finset κ)
            {k : κ |
              (H
                  (↑(k.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) :
                    ι)).FiniteIndex}
            x),
          f x • (↑(K x) : Set G)) ∪
      ⋃ (x : κ),
        ⋃ (_ :
          Membership.mem (γ := Finset κ)
            {a : κ |
              ¬(H
                    (↑(a.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) :
                      ι)).FiniteIndex}
            x),
          f x • (↑(K x) : Set G))
    ((⋃ x ∈ {i ∈ s | (H i).FiniteIndex}, g x • (↑(H x) : Set G)) ∪
      ⋃ x ∈ {a ∈ s | ¬(H a).FiniteIndex}, g x • (↑(H x) : Set G))
⊢ Eq.{u_1 + 1} (α := Set G) (⋃ (k : κ), ⋃ (_ : Membership.mem (γ := Finset κ) Finset.univ k), f k • (↑(K k) : Set G))
    Set.univ

Tactic:
rw [← hcovers, ← Finset.univ.filter_union_filter_not_eq (fun k => (H k.1).FiniteIndex),
      Finset.set_biUnion_union, Finset.set_biUnion_union]

Premises used: Finset.univ, Subgroup.FiniteIndex, Finset.filter_union_filter_not_eq, Finset.set_biUnion_union
-- 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}))) : ι)
hx :
  Eq.{u_1 + 1} (α := Set G)
    (⋃ (x : κ),
      ⋃ (_ :
        Membership.mem (γ := Finset κ)
          {k : κ |
            (H
                (↑(k.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) :
                  ι)).FiniteIndex}
          x),
        f x • (↑(K x) : Set G))
    (⋃ x ∈ {i ∈ s | (H i).FiniteIndex}, g x • (↑(H x) : Set G))
hy :
  Eq.{u_1 + 1} (α := Set G)
    (⋃ (x : κ),
      ⋃ (_ :
        Membership.mem (γ := Finset κ)
          {a : κ |
            ¬(H
                  (↑(a.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) :
                    ι)).FiniteIndex}
          x),
        f x • (↑(K x) : Set G))
    (⋃ x ∈ {a ∈ s | ¬(H a).FiniteIndex}, g x • (↑(H x) : Set G))
⊢ Eq.{u_1 + 1} (α := Set G)
    ((⋃ (x : κ),
        ⋃ (_ :
          Membership.mem (γ := Finset κ)
            {k : κ |
              (H
                  (↑(k.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) :
                    ι)).FiniteIndex}
            x),
          f x • (↑(K x) : Set G)) ∪
      ⋃ (x : κ),
        ⋃ (_ :
          Membership.mem (γ := Finset κ)
            {a : κ |
              ¬(H
                    (↑(a.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) :
                      ι)).FiniteIndex}
            x),
          f x • (↑(K x) : Set G))
    ((⋃ x ∈ {i ∈ s | (H i).FiniteIndex}, g x • (↑(H x) : Set G)) ∪
      ⋃ x ∈ {a ∈ s | ¬(H a).FiniteIndex}, g x • (↑(H x) : Set G))

Tactic:
apply congrArg₂ (· ∪ ·)

Premises used: congrArg₂, Union.union
-- 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}))) : ι)
hx :
  Eq.{u_1 + 1} (α := Set G)
    (⋃ (x : ι),
      ⋃ (hx : x ∈ s),
        ⋃ (a :
          ↥(if h : (H (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) : ι)).FiniteIndex then
              t (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) : ι) ⋯ h
            else {1})),
          ⋃ (_ :
            Membership.mem (γ := Finset κ)
              {k : κ |
                (H
                    (↑(k.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) x 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) x 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) x hx) a)) :
                Set G))
    (⋃ x ∈ {i ∈ s | (H i).FiniteIndex}, g x • (↑(H x) : Set G))
⊢ Eq.{u_1 + 1} (α := Set G)
    (⋃ (x : κ),
      ⋃ (_ :
        Membership.mem (γ := Finset κ)
          {k : κ |
            (H
                (↑(k.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) :
                  ι)).FiniteIndex}
          x),
        f x • (↑(K x) : Set G))
    (⋃ x ∈ {i ∈ s | (H i).FiniteIndex}, g x • (↑(H x) : Set G))

Tactic:
rw [Set.iUnion_sigma, Set.iUnion_subtype]

Premises used: Set.iUnion_sigma, Set.iUnion_subtype
-- 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}))) : ι)
hy :
  Eq.{u_1 + 1} (α := Set G)
    (⋃ (x : ι),
      ⋃ (hx : x ∈ s),
        ⋃ (a :
          ↥(if h : (H (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) : ι)).FiniteIndex then
              t (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x 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) x 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) x 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) x hx) a)) :
                Set G))
    (⋃ x ∈ {a ∈ s | ¬(H a).FiniteIndex}, g x • (↑(H x) : Set G))
⊢ Eq.{u_1 + 1} (α := Set G)
    (⋃ (x : κ),
      ⋃ (_ :
        Membership.mem (γ := Finset κ)
          {a : κ |
            ¬(H
                  (↑(a.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) :
                    ι)).FiniteIndex}
          x),
        f x • (↑(K x) : Set G))
    (⋃ x ∈ {a ∈ s | ¬(H a).FiniteIndex}, g x • (↑(H x) : Set G))

Tactic:
rw [Set.iUnion_sigma, Set.iUnion_subtype]

Premises used: Set.iUnion_sigma, Set.iUnion_subtype
-- 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}))) : ι)
⊢ Eq.{u_1 + 1} (α := Set G)
    (⋃ (x : ι),
      ⋃ (hx : x ∈ s),
        ⋃ (a :
          ↥(if h : (H (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) : ι)).FiniteIndex then
              t (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) : ι) ⋯ h
            else {1})),
          ⋃ (_ :
            Membership.mem (γ := Finset κ)
              {k : κ |
                (H
                    (↑(k.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) x 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) x 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) x hx) a)) :
                Set G))
    (⋃ x ∈ {i ∈ s | (H i).FiniteIndex}, g x • (↑(H x) : Set G))

Tactic:
Set.iUnion_congr fun i => ?_

Premises used: Set.iUnion_congr
-- 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}))) : ι)
⊢ Eq.{u_1 + 1} (α := Set G)
    (⋃ (x : ι),
      ⋃ (hx : x ∈ s),
        ⋃ (a :
          ↥(if h : (H (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) : ι)).FiniteIndex then
              t (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x 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) x 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) x 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) x hx) a)) :
                Set G))
    (⋃ x ∈ {a ∈ s | ¬(H a).FiniteIndex}, g x • (↑(H x) : Set G))

Tactic:
Set.iUnion_congr fun i => ?_

Premises used: Set.iUnion_congr
-- 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 : ι
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 κ)
            {k : κ |
              (H
                  (↑(k.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 ∈ {i ∈ s | (H i).FiniteIndex}), g i • (↑(H i) : Set G))

Tactic:
simp [← Set.smul_set_iUnion₂, Set.iUnion_subtype, ← leftCoset_assoc, f, K, ht, hfi]

Premises used: Set.smul_set_iUnion₂, leftCoset_assoc, Set.iUnion_subtype