awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : 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) (j : ι) (hj : j ∈ s)
      (hcovers' : Ne.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ)
      (hn : m = (Finset.image H s).card), ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
j : ι
hj : j ∈ s
hcovers'_1 : Ne.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ
hn : n = (Finset.image H s).card
x : G
hx : ∀ (y : G), y • (↑(H j) : Set G) ⊆ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • (↑(H i) : Set G)
κ : Type u_2 := ↥({x ∈ s | H x ≠ H j}) × Option ↥({x ∈ s | H x = H j})
f : κ → G :=
  fun (x_1 : κ) ↦
    match (motive := κ → G) x_1 with
    | (k₁, some k₂) => g (↑k₂ : ι) * x⁻¹ * g (↑k₁ : ι)
    | (k₁, none) => g (↑k₁ : ι)
K : (k : κ) → Subgroup G := fun (k : κ) ↦ H (↑k.1 : ι)
hK' : ∀ (k : κ), K k ∈ (Finset.image H s).erase (H j)
hK : ∀ (k : κ), K k ≠ H j
hcovers :
  Eq.{u_1 + 1} (α := Set G) (⋃ (k : κ), ⋃ (_ : Membership.mem (γ := Finset κ) Finset.univ k), f k • (↑(K k) : Set G))
    Set.univ
k : κ
hcovers' :
  Eq.{u_1 + 1} (α := Set G)
    (⋃ (i : κ), ⋃ (_ : Membership.mem (γ := Finset κ) {x : κ | K x = K k} i), f i • (↑(K i) : Set G)) Set.univ
⊢ ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
have hcovers'₁ : Eq.{u_1 + 1} (α := Set G)
  (⋃ (i : κ), ⋃ (_ : Membership.mem (γ := Finset κ) {x : κ | K x = K k} i), f i • (↑(K k) : Set G)) Set.univ
Tactic: rw [Set.iUnion₂_congr fun i hi => by rw [(Finset.mem_filter.mp hi).right]] at hcovers'
Cleared hypotheses: hcovers'
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : 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) (j : ι) (hj : j ∈ s)
      (hcovers' : Ne.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ)
      (hn : m = (Finset.image H s).card), ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
j : ι
hj : j ∈ s
hcovers'_1 : Ne.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ
hn : n = (Finset.image H s).card
x : G
hx : ∀ (y : G), y • (↑(H j) : Set G) ⊆ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • (↑(H i) : Set G)
κ : Type u_2 := ↥({x ∈ s | H x ≠ H j}) × Option ↥({x ∈ s | H x = H j})
f : κ → G :=
  fun (x_1 : κ) ↦
    match (motive := κ → G) x_1 with
    | (k₁, some k₂) => g (↑k₂ : ι) * x⁻¹ * g (↑k₁ : ι)
    | (k₁, none) => g (↑k₁ : ι)
K : (k : κ) → Subgroup G := fun (k : κ) ↦ H (↑k.1 : ι)
hK' : ∀ (k : κ), K k ∈ (Finset.image H s).erase (H j)
hK : ∀ (k : κ), K k ≠ H j
hcovers :
  Eq.{u_1 + 1} (α := Set G) (⋃ (k : κ), ⋃ (_ : Membership.mem (γ := Finset κ) Finset.univ k), f k • (↑(K k) : Set G))
    Set.univ
k : κ
hcovers' :
  ¬Eq.{u_1 + 1} (α := Set G)
      (⋃ (i : κ), ⋃ (_ : Membership.mem (γ := Finset κ) {x : κ | K x = K k} i), f i • (↑(K i) : Set G)) Set.univ
⊢ (Finset.image K Finset.univ).card < (Finset.image H s).card
have refine : ∀ x ∈ Finset.image K Finset.univ, x ∈ (Finset.image H s).erase (H j)
Tactic: refine ((Finset.card_le_card fun x => ?_).trans_lt <|
        Finset.card_erase_lt_of_mem (Finset.mem_image_of_mem H hj))
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : 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) (j : ι) (hj : j ∈ s)
      (hcovers' : Ne.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ)
      (hn : m = (Finset.image H s).card), ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
j : ι
hj : j ∈ s
hcovers'_1 : Ne.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ
hn : n = (Finset.image H s).card
x_1 : G
hx : ∀ (y : G), y • (↑(H j) : Set G) ⊆ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x_1⁻¹ * g i) • (↑(H i) : Set G)
κ : Type u_2 := ↥({x ∈ s | H x ≠ H j}) × Option ↥({x ∈ s | H x = H j})
f : κ → G :=
  fun (x : κ) ↦
    match (motive := κ → G) x with
    | (k₁, some k₂) => g (↑k₂ : ι) * x_1⁻¹ * g (↑k₁ : ι)
    | (k₁, none) => g (↑k₁ : ι)
K : (k : κ) → Subgroup G := fun (k : κ) ↦ H (↑k.1 : ι)
hK' : ∀ (k : κ), K k ∈ (Finset.image H s).erase (H j)
hK : ∀ (k : κ), K k ≠ H j
hcovers :
  Eq.{u_1 + 1} (α := Set G) (⋃ (k : κ), ⋃ (_ : Membership.mem (γ := Finset κ) Finset.univ k), f k • (↑(K k) : Set G))
    Set.univ
k : κ
hcovers' :
  ¬Eq.{u_1 + 1} (α := Set G)
      (⋃ (i : κ), ⋃ (_ : Membership.mem (γ := Finset κ) {x : κ | K x = K k} i), f i • (↑(K i) : Set G)) Set.univ
x : Subgroup G
⊢ x ∈ Finset.image K Finset.univ → x ∈ (Finset.image H s).erase (H j)
have rw : (∃ (y : κ), K y = x) → x ∈ (Finset.image H s).erase (H j)
Tactic: rw [mem_image_univ_iff_mem_range, Set.mem_range]
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : 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) (j : ι) (hj : j ∈ s)
      (hcovers' : Ne.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ)
      (hn : m = (Finset.image H s).card), ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
j : ι
hj : j ∈ s
hcovers'_1 : Ne.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ
hn : n = (Finset.image H s).card
x : G
hx : ∀ (y : G), y • (↑(H j) : Set G) ⊆ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • (↑(H i) : Set G)
κ : Type u_2 := ↥({x ∈ s | H x ≠ H j}) × Option ↥({x ∈ s | H x = H j})
f : κ → G :=
  fun (x_1 : κ) ↦
    match (motive := κ → G) x_1 with
    | (k₁, some k₂) => g (↑k₂ : ι) * x⁻¹ * g (↑k₁ : ι)
    | (k₁, none) => g (↑k₁ : ι)
K : (k : κ) → Subgroup G := fun (k : κ) ↦ H (↑k.1 : ι)
hK' : ∀ (k : κ), K k ∈ (Finset.image H s).erase (H j)
hK : ∀ (k : κ), K k ≠ H j
hcovers :
  Eq.{u_1 + 1} (α := Set G) (⋃ (k : κ), ⋃ (_ : Membership.mem (γ := Finset κ) Finset.univ k), f k • (↑(K k) : Set G))
    Set.univ
k : κ
hcovers' :
  ¬Eq.{u_1 + 1} (α := Set G)
      (⋃ (i : κ), ⋃ (_ : Membership.mem (γ := Finset κ) {x : κ | K x = K k} i), f i • (↑(K i) : Set G)) Set.univ
⊢ ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
have hn' : (Finset.image K Finset.univ).card < n
Tactic: have hn' : (Finset.univ.image K).card < n := hn ▸ by
      refine ((Finset.card_le_card fun x => ?_).trans_lt <|
        Finset.card_erase_lt_of_mem (Finset.mem_image_of_mem H hj))
      rw [mem_image_univ_iff_mem_range, Set.mem_range]
      exact fun ⟨k, hk⟩ => hk ▸ hK' k
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : 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) (j : ι) (hj : j ∈ s)
      (hcovers' : Ne.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ)
      (hn : m = (Finset.image H s).card), ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
j : ι
hj : j ∈ s
hcovers'_1 : Ne.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ
hn : n = (Finset.image H s).card
x : G
hx : ∀ (y : G), y • (↑(H j) : Set G) ⊆ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • (↑(H i) : Set G)
κ : Type u_2 := ↥({x ∈ s | H x ≠ H j}) × Option ↥({x ∈ s | H x = H j})
f : κ → G :=
  fun (x_1 : κ) ↦
    match (motive := κ → G) x_1 with
    | (k₁, some k₂) => g (↑k₂ : ι) * x⁻¹ * g (↑k₁ : ι)
    | (k₁, none) => g (↑k₁ : ι)
K : (k : κ) → Subgroup G := fun (k : κ) ↦ H (↑k.1 : ι)
hK' : ∀ (k : κ), K k ∈ (Finset.image H s).erase (H j)
hK : ∀ (k : κ), K k ≠ H j
hcovers :
  Eq.{u_1 + 1} (α := Set G) (⋃ (k : κ), ⋃ (_ : Membership.mem (γ := Finset κ) Finset.univ k), f k • (↑(K k) : Set G))
    Set.univ
k : κ
hcovers' :
  ¬Eq.{u_1 + 1} (α := Set G)
      (⋃ (i : κ), ⋃ (_ : Membership.mem (γ := Finset κ) {x : κ | K x = K k} i), f i • (↑(K i) : Set G)) Set.univ
hn' : (Finset.image K Finset.univ).card < n
⊢ ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
have neg : ∀ (k' : κ) (hk' : Membership.mem (γ := Finset κ) Finset.univ k' ∧ K k' ≠ K k ∧ (K k').FiniteIndex),
  ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
Tactic: have ⟨k', hk'⟩ := ih _ hn' hcovers k (Finset.mem_univ k) hcovers' rfl
-- 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
⊢ s.Nonempty
have by_contra! : ∀
  (hcovers :
    Eq.{u_1 + 1} (α := Set G) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), g i • (↑(H i) : Set G)) Set.univ),
  False
Tactic: by_contra! rfl
Cleared hypotheses: s, 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
hcovers :
  Eq.{u_1 + 1} (α := Set G) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), g i • (↑(H i) : Set G)) Set.univ
⊢ False
have hcovers₁ : Eq.{u_1 + 1} (α := Set G) ∅ Set.univ
Tactic: rw [← Finset.set_biUnion_coe, Finset.coe_empty, Set.biUnion_empty] at hcovers
Cleared hypotheses: hcovers
-- 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
⊢ ∃ k ∈ s, (H k).FiniteIndex
have have : ∀ (j : ι) (hj : j ∈ s), ∃ k ∈ s, (H k).FiniteIndex
Tactic: have ⟨j, hj⟩ : s.Nonempty := by
    by_contra! rfl
    rw [← Finset.set_biUnion_coe, Finset.coe_empty, Set.biUnion_empty] at hcovers
    exact Set.empty_ne_univ hcovers
-- 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
j : ι
hj : j ∈ s
⊢ ∃ k ∈ s, (H k).FiniteIndex
have pos : ∀ (hcovers' : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ),
  ∃ k ∈ s, (H k).FiniteIndex
Tactic: by_cases hcovers' : ⋃ i ∈ s.filter (H · = H j), g i • (H i : Set G) = Set.univ
-- 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
j : ι
hj : j ∈ s
pos :
  ∀ (hcovers' : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ),
    ∃ k ∈ s, (H k).FiniteIndex
⊢ ∃ k ∈ s, (H k).FiniteIndex
have neg : ∀ (hcovers' : ¬Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ),
  ∃ k ∈ s, (H k).FiniteIndex
Tactic: by_cases hcovers' : ⋃ i ∈ s.filter (H · = H j), g i • (H i : Set G) = Set.univ
-- 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
j : ι
hj : j ∈ s
hcovers' : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ
i : ι
hi : i ∈ {x ∈ s | H x = H j}
⊢ g i • (↑(H i) : Set G) = g i • (↑(H j) : Set G)
have rw : g i • (↑(H j) : Set G) = g i • (↑(H j) : Set G)
Tactic: rw [(Finset.mem_filter.mp hi).right]
-- 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
j : ι
hj : j ∈ s
hcovers' : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ
⊢ ∃ k ∈ s, (H k).FiniteIndex
have hcovers'₁ : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H j) : Set G)) Set.univ
Tactic: rw [Set.iUnion₂_congr fun i hi => by rw [(Finset.mem_filter.mp hi).right]] at hcovers'
Cleared hypotheses: hcovers'
-- 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
j : ι
hj : j ∈ s
hcovers' : ¬Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ
⊢ ∃ k ∈ s, (H k).FiniteIndex
have neg : ∀ (i : ι) (hi : i ∈ s), H i ≠ H j → ∀ (hfi : (H i).FiniteIndex), ∃ k ∈ s, (H k).FiniteIndex
Tactic: have ⟨i, hi, _, hfi⟩ :=
      exists_finiteIndex_of_leftCoset_cover_aux hcovers j hj hcovers'
-- 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
⊢ ∃ k ∈ s, (H k).FiniteIndex
have have : ∀ (j : ι) (hj : j ∈ s), ∃ k ∈ s, (H k).FiniteIndex
Tactic: classical
  have ⟨j, hj⟩ : s.Nonempty := by
    by_contra! rfl
    rw [← Finset.set_biUnion_coe, Finset.coe_empty, Set.biUnion_empty] at hcovers
    exact Set.empty_ne_univ hcovers
  by_cases hcovers' : ⋃ i ∈ s.filter (H · = H j), g i • (H i : Set G) = Set.univ
  · rw [Set.iUnion₂_congr fun i hi => by rw [(Finset.mem_filter.mp hi).right]] at hcovers'
    exact ⟨j, hj, finiteIndex_of_leftCoset_cover_const hcovers'⟩
  · have ⟨i, hi, _, hfi⟩ :=
      exists_finiteIndex_of_leftCoset_cover_aux hcovers j hj hcovers'
    exact ⟨i, hi, hfi⟩
-- 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
have have₁ have₂ : ∀ (j : ι) (hj : j ∈ s), ∃ k ∈ s, (H k).FiniteIndex
⊢ ∃ k ∈ s, (H k).FiniteIndex
have pos : ∀ (j : ι) (hj : j ∈ s)
  (hcovers' : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ),
  ∃ k ∈ s, (H k).FiniteIndex
Tactic: classical
  have ⟨j, hj⟩ : s.Nonempty := by
    by_contra! rfl
    rw [← Finset.set_biUnion_coe, Finset.coe_empty, Set.biUnion_empty] at hcovers
    exact Set.empty_ne_univ hcovers
  by_cases hcovers' : ⋃ i ∈ s.filter (H · = H j), g i • (H i : Set G) = Set.univ
  · rw [Set.iUnion₂_congr fun i hi => by rw [(Finset.mem_filter.mp hi).right]] at hcovers'
    exact ⟨j, hj, finiteIndex_of_leftCoset_cover_const hcovers'⟩
  · have ⟨i, hi, _, hfi⟩ :=
      exists_finiteIndex_of_leftCoset_cover_aux hcovers j hj hcovers'
    exact ⟨i, hi, hfi⟩
-- 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
have have₁ have₂ : ∀ (j : ι) (hj : j ∈ s), ∃ k ∈ s, (H k).FiniteIndex
pos :
  ∀ (j : ι) (hj : j ∈ s)
    (hcovers' : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ),
    ∃ k ∈ s, (H k).FiniteIndex
⊢ ∃ k ∈ s, (H k).FiniteIndex
have neg : ∀ (j : ι) (hj : j ∈ s)
  (hcovers' : ¬Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ),
  ∃ k ∈ s, (H k).FiniteIndex
Tactic: classical
  have ⟨j, hj⟩ : s.Nonempty := by
    by_contra! rfl
    rw [← Finset.set_biUnion_coe, Finset.coe_empty, Set.biUnion_empty] at hcovers
    exact Set.empty_ne_univ hcovers
  by_cases hcovers' : ⋃ i ∈ s.filter (H · = H j), g i • (H i : Set G) = Set.univ
  · rw [Set.iUnion₂_congr fun i hi => by rw [(Finset.mem_filter.mp hi).right]] at hcovers'
    exact ⟨j, hj, finiteIndex_of_leftCoset_cover_const hcovers'⟩
  · have ⟨i, hi, _, hfi⟩ :=
      exists_finiteIndex_of_leftCoset_cover_aux hcovers j hj hcovers'
    exact ⟨i, hi, hfi⟩
-- 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
⊢ 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 hD : D.FiniteIndex
Tactic: have hD : D.FiniteIndex := finiteIndex_iInf' _ <| by simp
-- 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
⊢ 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 hD_le : ∀ {i : ι} (hi : i ∈ s) (hfi : (H i).FiniteIndex), D ≤ H i
Tactic: have hD_le {i} (hi : i ∈ s) (hfi : (H i).FiniteIndex) : D ≤ H i :=
    iInf₂_le i (Finset.mem_filter.mpr ⟨hi, hfi⟩)
-- 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
⊢ 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 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))
Tactic: choose t ht using fun i hi hfi =>
    exists_leftTransversal_of_FiniteIndex (H := H i) (hD_le hi hfi)
-- 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 ι
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) (⋃ (k : κ), ⋃ (_ : Membership.mem (γ := Finset κ) Finset.univ k), f k • (↑(K k) : Set G))
    Set.univ
have 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 : ι) sorry 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 : ι) sorry 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: rw [← hcovers, ← Finset.univ.filter_union_filter_not_eq (fun k => (H k.1).FiniteIndex),
      Finset.set_biUnion_union, Finset.set_biUnion_union]