awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (goal)
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}))) : ι)
hcovers' :
  Eq.{u_1 + 1} (α := Set G) (⋃ (k : κ), ⋃ (_ : Membership.mem (γ := Finset κ) Finset.univ k), f k • (↑(K k) : Set G))
    Set.univ
k : κ
hkfi :
  (H (↑(k.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) : ι)).FiniteIndex
hk : K k = D
h :
  Ne.{u_1 + 1} (α := Set G)
    (⋃ (i : κ), ⋃ (_ : Membership.mem (γ := Finset κ) {x : κ | K x = K k} i), f i • (↑(K i) : Set G)) Set.univ
⊢ False
have obtain : ∀ (i : κ) (hi : K i ≠ K k ∧ (K i).FiniteIndex), False
Tactic: obtain ⟨i, -, hi⟩ :=
      exists_finiteIndex_of_leftCoset_cover_aux hcovers' k (Finset.mem_univ k) h
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (goal)
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}))) : ι)
hcovers' :
  Eq.{u_1 + 1} (α := Set G) (⋃ (k : κ), ⋃ (_ : Membership.mem (γ := Finset κ) Finset.univ k), f k • (↑(K k) : Set G))
    Set.univ
k : κ
hkfi :
  (H (↑(k.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) : ι)).FiniteIndex
hk : K k = D
h :
  Ne.{u_1 + 1} (α := Set G)
    (⋃ (i : κ), ⋃ (_ : Membership.mem (γ := Finset κ) {x : κ | K x = K k} i), f i • (↑(K i) : Set G)) Set.univ
i : κ
hi : K i ≠ K k ∧ (K i).FiniteIndex
⊢ False
have pos : ∀
  (hfi :
    (H
        (↑(i.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) sorry h else {1}))) :
          ι)).FiniteIndex),
  False
Tactic: by_cases hfi : (H i.1.1).FiniteIndex
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (goal)
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}))) : ι)
hcovers' :
  Eq.{u_1 + 1} (α := Set G) (⋃ (k : κ), ⋃ (_ : Membership.mem (γ := Finset κ) Finset.univ k), f k • (↑(K k) : Set G))
    Set.univ
k : κ
hkfi :
  (H (↑(k.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) : ι)).FiniteIndex
hk : K k = D
h :
  Ne.{u_1 + 1} (α := Set G)
    (⋃ (i : κ), ⋃ (_ : Membership.mem (γ := Finset κ) {x : κ | K x = K k} i), f i • (↑(K i) : Set G)) Set.univ
i : κ
hi : K i ≠ K k ∧ (K i).FiniteIndex
pos :
  ∀
    (hfi :
      (H
          (↑(i.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) :
            ι)).FiniteIndex),
    False
⊢ False
have neg : ∀
  (hfi :
    ¬(H
          (↑(i.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) sorry h else {1}))) :
            ι)).FiniteIndex),
  False
Tactic: by_cases hfi : (H i.1.1).FiniteIndex
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (hypothesis)
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}))) : ι)
hcovers' :
  Eq.{u_1 + 1} (α := Set G) (⋃ (k : κ), ⋃ (_ : Membership.mem (γ := Finset κ) Finset.univ k), f k • (↑(K k) : Set G))
    Set.univ
k : κ
hkfi :
  (H (↑(k.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) : ι)).FiniteIndex
hk : K k = D
⊢ 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))
have hcovers'₁ : Eq.{u_1 + 1} (α := Set G) (⋃ (i : κ), ⋃ (_ : Membership.mem (γ := Finset κ) {x : κ | K x = D} i), f i • (↑D : Set G))
  Set.univ
Tactic: replace hcovers' : ⋃ i ∈ Finset.univ.filter (K · = D), f i • (D : Set G) = Set.univ := by
    rw [← hk, Set.iUnion₂_congr fun i hi => by rw [← (Finset.mem_filter.mp hi).2]]
    by_contra! h
    obtain ⟨i, -, hi⟩ :=
      exists_finiteIndex_of_leftCoset_cover_aux hcovers' k (Finset.mem_univ k) h
    by_cases hfi : (H i.1.1).FiniteIndex <;> simp [K, hfi, hkfi] at hi
Cleared hypotheses: hcovers'
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (hypothesis)
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
⊢ 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))
have hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
Tactic: have hHD (i) : ¬(H i).FiniteIndex → H i ≠ D := fun hfi hD' => (hD' ▸ hfi) hD
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (goal)
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
⊢ ∑ i ∈ s, (↑(H i).index : ℚ)⁻¹ = HMul.hMul (α := ℚ) (↑(Finset.card (α := κ) {x : κ | K x = D}) : ℚ) (↑D.index : ℚ)⁻¹
have rw : Eq (α := ℚ)
  (∑ i ∈ s.attach,
    ∑ s_1 : ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) sorry h else {1}),
      (↑(if
              K (Sigma.mk (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) sorry h else {1})) i s_1) =
                D then
            1
          else 0) :
        ℚ))
  (∑ x ∈ s.attach, HMul.hMul (α := ℚ) (↑(H (↑x : ι)).index : ℚ)⁻¹ (↑D.index : ℚ))
Tactic: rw [eq_mul_inv_iff_mul_eq₀ (Nat.cast_ne_zero.mpr hD.index_ne_zero), Finset.sum_mul,
      ← Finset.sum_attach, eq_comm, Finset.card_filter, Nat.cast_sum, ← Finset.univ_sigma_univ,
      Finset.sum_sigma, Finset.sum_coe_sort_eq_attach]
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (goal)
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
⊢ Eq (α := ℚ)
    (∑ i ∈ s.attach,
      ∑ s_1 : ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}),
        (↑(if
                K
                    (Sigma.mk (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1})) i
                      s_1) =
                  D then
              1
            else 0) :
          ℚ))
    (∑ x ∈ s.attach, HMul.hMul (α := ℚ) (↑(H (↑x : ι)).index : ℚ)⁻¹ (↑D.index : ℚ))
have refine : ∀ i ∈ s.attach,
  ∑ s_1 : ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) sorry h else {1}),
      (↑(if
              K (Sigma.mk (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) sorry h else {1})) i s_1) =
                D then
            1
          else 0) :
        ℚ) =
    HMul.hMul (α := ℚ) (↑(H (↑i : ι)).index : ℚ)⁻¹ (↑D.index : ℚ)
Tactic: refine Finset.sum_congr rfl fun i _ => ?_
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (goal)
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
i : ↥s
h : i ∈ s.attach
⊢ ∑ s_1 : ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}),
      (↑(if
              K (Sigma.mk (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1})) i s_1) =
                D then
            1
          else 0) :
        ℚ) =
    HMul.hMul (α := ℚ) (↑(H (↑i : ι)).index : ℚ)⁻¹ (↑D.index : ℚ)
have pos : ∀ (hfi : (H (↑i : ι)).FiniteIndex),
  ∑ s_1 : ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) sorry h else {1}),
      (↑(if
              K (Sigma.mk (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) sorry h else {1})) i s_1) =
                D then
            1
          else 0) :
        ℚ) =
    HMul.hMul (α := ℚ) (↑(H (↑i : ι)).index : ℚ)⁻¹ (↑D.index : ℚ)
Tactic: by_cases hfi : (H i).FiniteIndex
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (goal)
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
i : ↥s
h : i ∈ s.attach
pos :
  ∀ (hfi : (H (↑i : ι)).FiniteIndex),
    ∑ s_1 : ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}),
        (↑(if
                K
                    (Sigma.mk (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1})) i
                      s_1) =
                  D then
              1
            else 0) :
          ℚ) =
      HMul.hMul (α := ℚ) (↑(H (↑i : ι)).index : ℚ)⁻¹ (↑D.index : ℚ)
⊢ ∑ s_1 : ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}),
      (↑(if
              K (Sigma.mk (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1})) i s_1) =
                D then
            1
          else 0) :
        ℚ) =
    HMul.hMul (α := ℚ) (↑(H (↑i : ι)).index : ℚ)⁻¹ (↑D.index : ℚ)
have neg : ∀ (hfi : ¬(H (↑i : ι)).FiniteIndex),
  ∑ s_1 : ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) sorry h else {1}),
      (↑(if
              K (Sigma.mk (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) sorry h else {1})) i s_1) =
                D then
            1
          else 0) :
        ℚ) =
    HMul.hMul (α := ℚ) (↑(H (↑i : ι)).index : ℚ)⁻¹ (↑D.index : ℚ)
Tactic: by_cases hfi : (H i).FiniteIndex