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
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}))) : ι)
k : κ
hkfi :
  (H (↑(k.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) : ι)).FiniteIndex
hk : K k = D
hcovers' :
  Eq.{u_1 + 1} (α := Set G) (⋃ (i : κ), ⋃ (_ : Membership.mem (γ := Finset κ) {x : κ | K x = D} i), f i • (↑D : Set G))
    Set.univ
hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
hdensity :
  ∑ i ∈ s, (↑(H i).index : ℚ)⁻¹ = HMul.hMul (α := ℚ) (↑(Finset.card (α := κ) {x : κ | K x = D}) : ℚ) (↑D.index : ℚ)⁻¹
h : Finset.card (α := κ) {x : κ | K x = D} = D.index
i_1 : ι
hi_1 : i_1 ∈ s ∧ (H i_1).FiniteIndex
j : ι
hj : j ∈ s ∧ (H j).FiniteIndex
hij : i_1 ≠ j
c : Set G
hi'_1 : c ≤ (fun (i : ι) ↦ g i • (↑(H i) : Set G)) i_1
hj' : c ≤ (fun (i : ι) ↦ g i • (↑(H i) : Set G)) j
x : G
hx : x ∈ c
hdisjoint : (↑{x : κ | K x = D} : Set κ).PairwiseDisjoint (α := Set G) fun (x : κ) ↦ f x • (↑D : Set G)
i : ι
hi : i ∈ s ∧ (H i).FiniteIndex
hi' : c ≤ g i • (↑(H i) : Set G)
⊢ c ≤ HSMul.hSMul (β := Set G) (g i) (⋃ g ∈ t i ⋯ ⋯, (↑g : G) • (↑D : Set G))

Tactic:
rw [← (ht i hi.1 hi.2).2] at hi'

Premises used: And.right, And.left
-- 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
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}))) : ι)
k : κ
hkfi :
  (H (↑(k.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) : ι)).FiniteIndex
hk : K k = D
hcovers' :
  Eq.{u_1 + 1} (α := Set G) (⋃ (i : κ), ⋃ (_ : Membership.mem (γ := Finset κ) {x : κ | K x = D} i), f i • (↑D : Set G))
    Set.univ
hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
hdensity :
  ∑ i ∈ s, (↑(H i).index : ℚ)⁻¹ = HMul.hMul (α := ℚ) (↑(Finset.card (α := κ) {x : κ | K x = D}) : ℚ) (↑D.index : ℚ)⁻¹
h : Finset.card (α := κ) {x : κ | K x = D} = D.index
i_1 : ι
hi_1 : i_1 ∈ s ∧ (H i_1).FiniteIndex
j : ι
hj : j ∈ s ∧ (H j).FiniteIndex
hij : i_1 ≠ j
c : Set G
hi'_1 : c ≤ (fun (i : ι) ↦ g i • (↑(H i) : Set G)) i_1
hj' : c ≤ (fun (i : ι) ↦ g i • (↑(H i) : Set G)) j
x : G
hx : x ∈ c
hdisjoint : (↑{x : κ | K x = D} : Set κ).PairwiseDisjoint (α := Set G) fun (x : κ) ↦ f x • (↑D : Set G)
i : ι
hi : i ∈ s ∧ (H i).FiniteIndex
hi' : c ≤ HSMul.hSMul (β := Set G) (g i) (⋃ g ∈ t i ⋯ ⋯, (↑g : G) • (↑D : Set G))
this : ∃ r ∈ t i ⋯ ⋯, x ∈ (g i * (↑r : G)) • (↑D : Set G)
have :
  ∀ (r : ↥(H i)) (hr : r ∈ t i ⋯ ⋯) (hxr : x ∈ (g i * (↑r : G)) • (↑D : Set G)),
    ∃ (k : κ),
      (↑(k.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) : ι) = i ∧
        K k = D ∧ x ∈ f k • (↑D : Set G)
⊢ ∃ (k : κ),
    (↑(k.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) : ι) = i ∧
      K k = D ∧ x ∈ f k • (↑D : Set G)

Tactic:
have ⟨r, hr, hxr⟩ := this
-- 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
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}))) : ι)
k : κ
hkfi :
  (H (↑(k.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) : ι)).FiniteIndex
hk : K k = D
hcovers' :
  Eq.{u_1 + 1} (α := Set G) (⋃ (i : κ), ⋃ (_ : Membership.mem (γ := Finset κ) {x : κ | K x = D} i), f i • (↑D : Set G))
    Set.univ
hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
hdensity :
  ∑ i ∈ s, (↑(H i).index : ℚ)⁻¹ = HMul.hMul (α := ℚ) (↑(Finset.card (α := κ) {x : κ | K x = D}) : ℚ) (↑D.index : ℚ)⁻¹
h : Finset.card (α := κ) {x : κ | K x = D} = D.index
i_1 : ι
hi_1 : i_1 ∈ s ∧ (H i_1).FiniteIndex
j : ι
hj : j ∈ s ∧ (H j).FiniteIndex
hij : i_1 ≠ j
c : Set G
hi'_1 : c ≤ (fun (i : ι) ↦ g i • (↑(H i) : Set G)) i_1
hj' : c ≤ (fun (i : ι) ↦ g i • (↑(H i) : Set G)) j
x : G
hx : x ∈ c
hdisjoint : (↑{x : κ | K x = D} : Set κ).PairwiseDisjoint (α := Set G) fun (x : κ) ↦ f x • (↑D : Set G)
i : ι
hi : i ∈ s ∧ (H i).FiniteIndex
hi' : c ≤ HSMul.hSMul (β := Set G) (g i) (⋃ g ∈ t i ⋯ ⋯, (↑g : G) • (↑D : Set G))
this : ∃ r ∈ t i ⋯ ⋯, x ∈ (g i * (↑r : G)) • (↑D : Set G)
r : ↥(H i)
hr : r ∈ t i ⋯ ⋯
hxr : x ∈ (g i * (↑r : G)) • (↑D : Set G)
⊢ ∃ (k : κ),
    (↑(k.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) : ι) = i ∧
      K k = D ∧ x ∈ f k • (↑D : Set G)

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

Premises used: Eq.rec, dif_pos, Subtype.mk, And.right, And.left, And.intro, Exists.intro, Sigma.mk, Eq.symm, rfl
-- 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
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}))) : ι)
k : κ
hkfi :
  (H (↑(k.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) : ι)).FiniteIndex
hk : K k = D
hcovers' :
  Eq.{u_1 + 1} (α := Set G) (⋃ (i : κ), ⋃ (_ : Membership.mem (γ := Finset κ) {x : κ | K x = D} i), f i • (↑D : Set G))
    Set.univ
hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
hdensity :
  ∑ i ∈ s, (↑(H i).index : ℚ)⁻¹ = HMul.hMul (α := ℚ) (↑(Finset.card (α := κ) {x : κ | K x = D}) : ℚ) (↑D.index : ℚ)⁻¹
h : Finset.card (α := κ) {x : κ | K x = D} = D.index
i_1 : ι
hi_1 : i_1 ∈ s ∧ (H i_1).FiniteIndex
j : ι
hj : j ∈ s ∧ (H j).FiniteIndex
hij : i_1 ≠ j
c : Set G
hi'_1 : c ≤ (fun (i : ι) ↦ g i • (↑(H i) : Set G)) i_1
hj' : c ≤ (fun (i : ι) ↦ g i • (↑(H i) : Set G)) j
x : G
hx : x ∈ c
hdisjoint : (↑{x : κ | K x = D} : Set κ).PairwiseDisjoint (α := Set G) fun (x : κ) ↦ f x • (↑D : Set G)
i : ι
hi : i ∈ s ∧ (H i).FiniteIndex
hi' : c ≤ HSMul.hSMul (β := Set G) (g i) (⋃ g ∈ t i ⋯ ⋯, (↑g : G) • (↑D : Set G))
suffices : ∃ r ∈ t i ⋯ ⋯, x ∈ (g i * (↑r : G)) • (↑D : Set G)
⊢ ∃ (k : κ),
    (↑(k.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) : ι) = i ∧
      K k = D ∧ x ∈ f k • (↑D : Set G)

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
-- 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
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}))) : ι)
k : κ
hkfi :
  (H (↑(k.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) : ι)).FiniteIndex
hk : K k = D
hcovers' :
  Eq.{u_1 + 1} (α := Set G) (⋃ (i : κ), ⋃ (_ : Membership.mem (γ := Finset κ) {x : κ | K x = D} i), f i • (↑D : Set G))
    Set.univ
hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
hdensity :
  ∑ i ∈ s, (↑(H i).index : ℚ)⁻¹ = HMul.hMul (α := ℚ) (↑(Finset.card (α := κ) {x : κ | K x = D}) : ℚ) (↑D.index : ℚ)⁻¹
h : Finset.card (α := κ) {x : κ | K x = D} = D.index
i_1 : ι
hi_1 : i_1 ∈ s ∧ (H i_1).FiniteIndex
j : ι
hj : j ∈ s ∧ (H j).FiniteIndex
hij : i_1 ≠ j
c : Set G
hi'_1 : c ≤ (fun (i : ι) ↦ g i • (↑(H i) : Set G)) i_1
hj' : c ≤ (fun (i : ι) ↦ g i • (↑(H i) : Set G)) j
x : G
hx : x ∈ c
hdisjoint : (↑{x : κ | K x = D} : Set κ).PairwiseDisjoint (α := Set G) fun (x : κ) ↦ f x • (↑D : Set G)
i : ι
hi : i ∈ s ∧ (H i).FiniteIndex
hi' : c ≤ HSMul.hSMul (β := Set G) (g i) (⋃ g ∈ t i ⋯ ⋯, (↑g : G) • (↑D : Set G))
⊢ ∃ r ∈ t i ⋯ ⋯, x ∈ (g i * (↑r : G)) • (↑D : Set G)

Tactic:
simpa [Set.mem_smul_set_iff_inv_smul_mem, smul_eq_mul, mul_assoc] using hi' hx

Premises used: mul_assoc, Set.mem_smul_set_iff_inv_smul_mem, smul_eq_mul
-- 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
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}))) : ι)
k : κ
hkfi :
  (H (↑(k.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) : ι)).FiniteIndex
hk : K k = D
hcovers' :
  Eq.{u_1 + 1} (α := Set G) (⋃ (i : κ), ⋃ (_ : Membership.mem (γ := Finset κ) {x : κ | K x = D} i), f i • (↑D : Set G))
    Set.univ
hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
hdensity :
  ∑ i ∈ s, (↑(H i).index : ℚ)⁻¹ = HMul.hMul (α := ℚ) (↑(Finset.card (α := κ) {x : κ | K x = D}) : ℚ) (↑D.index : ℚ)⁻¹
h : Finset.card (α := κ) {x : κ | K x = D} = 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) : Set G)) i
hj' : c ≤ (fun (i : ι) ↦ g i • (↑(H i) : Set G)) j
x : G
hx : x ∈ c
hdisjoint : (↑{x : κ | K x = D} : Set κ).PairwiseDisjoint (α := Set G) fun (x : κ) ↦ f x • (↑D : Set G)
⊢ ∀ (i : ι) (hi : i ∈ s ∧ (H i).FiniteIndex) (hi' : c ≤ g i • (↑(H i) : Set G)),
    ∃ (k : κ),
      (↑(k.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) : ι) = i ∧
        K k = D ∧ x ∈ f k • (↑D : Set G)

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
-- 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
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}))) : ι)
k : κ
hkfi :
  (H (↑(k.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) : ι)).FiniteIndex
hk : K k = D
hcovers' :
  Eq.{u_1 + 1} (α := Set G) (⋃ (i : κ), ⋃ (_ : Membership.mem (γ := Finset κ) {x : κ | K x = D} i), f i • (↑D : Set G))
    Set.univ
hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
hdensity :
  ∑ i ∈ s, (↑(H i).index : ℚ)⁻¹ = HMul.hMul (α := ℚ) (↑(Finset.card (α := κ) {x : κ | K x = D}) : ℚ) (↑D.index : ℚ)⁻¹
h : Finset.card (α := κ) {x : κ | K x = D} = 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) : Set G)) i
hj' : c ≤ (fun (i : ι) ↦ g i • (↑(H i) : Set G)) j
x : G
hx : x ∈ c
hdisjoint : (↑{x : κ | K x = D} : Set κ).PairwiseDisjoint (α := Set G) fun (x : κ) ↦ f x • (↑D : Set G)
hk' :
  ∀ (i : ι) (hi : i ∈ s ∧ (H i).FiniteIndex) (hi' : c ≤ g i • (↑(H i) : Set G)),
    ∃ (k : κ),
      (↑(k.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) : ι) = i ∧
        K k = D ∧ x ∈ f k • (↑D : Set G)
refine_3 :
  ∀ (k₁ : κ)
    (hik₁ : (↑(k₁.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) : ι) = i)
    (hk₁ : K k₁ = D) (hxk₁ : x ∈ f k₁ • (↑D : Set G)), Membership.mem (γ := Set G) ⊥ x
⊢ Membership.mem (γ := Set G) ⊥ x

Tactic:
have ⟨k₁, hik₁, hk₁, hxk₁⟩ := hk' i hi hi'
-- 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
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}))) : ι)
k : κ
hkfi :
  (H (↑(k.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) : ι)).FiniteIndex
hk : K k = D
hcovers' :
  Eq.{u_1 + 1} (α := Set G) (⋃ (i : κ), ⋃ (_ : Membership.mem (γ := Finset κ) {x : κ | K x = D} i), f i • (↑D : Set G))
    Set.univ
hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
hdensity :
  ∑ i ∈ s, (↑(H i).index : ℚ)⁻¹ = HMul.hMul (α := ℚ) (↑(Finset.card (α := κ) {x : κ | K x = D}) : ℚ) (↑D.index : ℚ)⁻¹
h : Finset.card (α := κ) {x : κ | K x = D} = 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) : Set G)) i
hj' : c ≤ (fun (i : ι) ↦ g i • (↑(H i) : Set G)) j
x : G
hx : x ∈ c
hdisjoint : (↑{x : κ | K x = D} : Set κ).PairwiseDisjoint (α := Set G) fun (x : κ) ↦ f x • (↑D : Set G)
hk' :
  ∀ (i : ι) (hi : i ∈ s ∧ (H i).FiniteIndex) (hi' : c ≤ g i • (↑(H i) : Set G)),
    ∃ (k : κ),
      (↑(k.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) : ι) = i ∧
        K k = D ∧ x ∈ f k • (↑D : Set G)
k₁ : κ
hik₁ : (↑(k₁.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) : ι) = i
hk₁ : K k₁ = D
hxk₁ : x ∈ f k₁ • (↑D : Set G)
refine_3 :
  ∀ (k₂ : κ)
    (hjk₂ : (↑(k₂.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) : ι) = j)
    (hk₂ : K k₂ = D) (hxk₂ : x ∈ f k₂ • (↑D : Set G)), Membership.mem (γ := Set G) ⊥ x
⊢ Membership.mem (γ := Set G) ⊥ x

Tactic:
have ⟨k₂, hjk₂, hk₂, hxk₂⟩ := hk' j hj hj'
-- 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
⊢ Eq.{u_1 + 1} (α := Set G) (⋃ k ∈ {i ∈ s | (H i).FiniteIndex}, g k • (↑(H k) : Set G)) Set.univ

Tactic:
(leftCoset_cover_filter_FiniteIndex_aux hcovers).1

Premises used: Subgroup.leftCoset_cover_filter_FiniteIndex_aux, And.left
-- 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
⊢ LE.le (α := ℚ) 1 (∑ i ∈ s, (↑(H i).index : ℚ)⁻¹)

Tactic:
have := Classical.decPred (FiniteIndex : Subgroup G → Prop)
  (leftCoset_cover_filter_FiniteIndex_aux hcovers).2.1

Premises used: Subgroup.FiniteIndex, Subgroup.leftCoset_cover_filter_FiniteIndex_aux, Classical.decPred, And.right, And.left
-- 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
⊢ 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:
(leftCoset_cover_filter_FiniteIndex_aux hcovers).2.2

Premises used: Subgroup.leftCoset_cover_filter_FiniteIndex_aux, And.right
-- 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
by_contra! : ∀ (h : ∀ (i : ι) (_ : i ∈ s) (_ : (H i).FiniteIndex), s.card < (H i).index), False
⊢ ∃ i ∈ s, (H i).FiniteIndex ∧ (H i).index ≤ s.card

Tactic:
by_contra! h