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 ι
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 : 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)
⊢ ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
have hK : ∀ (k : κ), K k ≠ H j
Tactic: have hK (k : κ) : K k ≠ H j := ((Finset.mem_erase.mp (hK' k)).left ·)
-- 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 ι
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 : 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
y : G
⊢ ∃ (i : κ) (_ : Membership.mem (γ := Finset κ) Finset.univ i), y ∈ f i • (↑(K i) : Set G)
have rw : ∀
  (hcovers :
    Eq.{u_1 + 1} (α := Set G)
      ((⋃ x ∈ {x ∈ s | H x = H j}, g x • (↑(H x) : Set G)) ∪ ⋃ x ∈ {a ∈ s | ¬H a = H j}, g x • (↑(H x) : Set G))
      Set.univ)
  (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 : 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)),
  let κ := ↥({x ∈ s | H x ≠ H j}) × Option ↥({x ∈ s | H x = H j});
  let f : κ → G := fun (x_1 : κ) ↦
    match (motive := κ → G) x_1 with
    | (k₁, some k₂) => g (↑k₂ : ι) * x⁻¹ * g (↑k₁ : ι)
    | (k₁, none) => g (↑k₁ : ι);
  let 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) (y : G),
    ∃ (i : κ) (_ : Membership.mem (γ := Finset κ) Finset.univ i), y ∈ f i • (↑(K i) : Set G)
Tactic: rw [← s.filter_union_filter_not_eq (H · = H j), Finset.set_biUnion_union] at hcovers
Cleared hypotheses: hcovers, hj, hcovers', hn, x, hx, κ, f, K, hK', hK, y
-- 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 : ι
hcovers :
  Eq.{u_1 + 1} (α := Set G)
    ((⋃ x ∈ {x ∈ s | H x = H j}, g x • (↑(H x) : Set G)) ∪ ⋃ x ∈ {a ∈ s | ¬H a = H j}, g x • (↑(H x) : Set G)) Set.univ
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 : 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
y : G
hy : Membership.mem (γ := Set G) (⋃ x ∈ {x ∈ s | H x = H j}, g x • (↑(H x) : Set G)) y
⊢ ∃ (i : κ) (_ : Membership.mem (γ := Finset κ) Finset.univ i), y ∈ f i • (↑(K i) : Set G)
have inl : ∀ (k : ι) (hk : k ∈ {x ∈ s | H x = H j}) (hy : y ∈ g k • (↑(H k) : Set G)),
  ∃ (i : κ) (_ : Membership.mem (γ := Finset κ) Finset.univ i), y ∈ f i • (↑(K i) : Set G)
Tactic: have ⟨k, hk, hy⟩ := Set.mem_iUnion₂.mp hy
-- 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 : ι
hcovers :
  Eq.{u_1 + 1} (α := Set G)
    ((⋃ x ∈ {x ∈ s | H x = H j}, g x • (↑(H x) : Set G)) ∪ ⋃ x ∈ {a ∈ s | ¬H a = H j}, g x • (↑(H x) : Set G)) Set.univ
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 : 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
y : G
hy_1 : Membership.mem (γ := Set G) (⋃ x ∈ {x ∈ s | H x = H j}, g x • (↑(H x) : Set G)) y
k : ι
hk : k ∈ {x ∈ s | H x = H j}
hy : y ∈ g k • (↑(H k) : Set G)
⊢ ∃ (i : κ) (_ : Membership.mem (γ := Finset κ) Finset.univ i), y ∈ f i • (↑(K i) : Set G)
have hk' : H k = H j
Tactic: have hk' : H k = H j := And.right <| by simpa using hk
-- 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 : ι
hcovers :
  Eq.{u_1 + 1} (α := Set G)
    ((⋃ x ∈ {x ∈ s | H x = H j}, g x • (↑(H x) : Set G)) ∪ ⋃ x ∈ {a ∈ s | ¬H a = H j}, g x • (↑(H x) : Set G)) Set.univ
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 : 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
y : G
hy_1 : Membership.mem (γ := Set G) (⋃ x ∈ {x ∈ s | H x = H j}, g x • (↑(H x) : Set G)) y
k : ι
hk : k ∈ {x ∈ s | H x = H j}
hy : y ∈ g k • (↑(H k) : Set G)
hk' : H k = H j
⊢ ∃ (i : κ) (_ : Membership.mem (γ := Finset κ) Finset.univ i), y ∈ f i • (↑(K i) : Set G)
have inl : ∀ (i : ι) (hi : i ∈ {x ∈ s | H x ≠ H j}) (hy : y ∈ (g k * x⁻¹ * g i) • (↑(H i) : Set G)),
  ∃ (i : κ) (_ : Membership.mem (γ := Finset κ) Finset.univ i), y ∈ f i • (↑(K i) : Set G)
Tactic: have ⟨i, hi, hy⟩ := Set.mem_iUnion₂.mp (hx (g k) (hk' ▸ hy))
-- 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 : ι
hcovers :
  Eq.{u_1 + 1} (α := Set G)
    ((⋃ x ∈ {x ∈ s | H x = H j}, g x • (↑(H x) : Set G)) ∪ ⋃ x ∈ {a ∈ s | ¬H a = H j}, g x • (↑(H x) : Set G)) Set.univ
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 : 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
y : G
hy : Membership.mem (γ := Set G) (⋃ x ∈ {a ∈ s | ¬H a = H j}, g x • (↑(H x) : Set G)) y
⊢ ∃ (i : κ) (_ : Membership.mem (γ := Finset κ) Finset.univ i), y ∈ f i • (↑(K i) : Set G)
have inr : ∀ (i : ι) (hi : i ∈ {a ∈ s | ¬H a = H j}) (hy : y ∈ g i • (↑(H i) : Set G)),
  ∃ (i : κ) (_ : Membership.mem (γ := Finset κ) Finset.univ i), y ∈ f i • (↑(K i) : Set G)
Tactic: have ⟨i, hi, hy⟩ := Set.mem_iUnion₂.mp hy
-- 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 : ι
hcovers :
  Eq.{u_1 + 1} (α := Set G)
    ((⋃ x ∈ {x ∈ s | H x = H j}, g x • (↑(H x) : Set G)) ∪ ⋃ x ∈ {a ∈ s | ¬H a = H j}, g x • (↑(H x) : Set G)) Set.univ
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 : 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
y : G
⊢ ∃ (i : κ) (_ : Membership.mem (γ := Finset κ) Finset.univ i), y ∈ f i • (↑(K i) : Set G)
have x₁ : Membership.mem (γ := Set G) (⋃ x ∈ {x ∈ s | H x = H j}, g x • (↑(H x) : Set G)) y ∨
  Membership.mem (γ := Set G) (⋃ x ∈ {a ∈ s | ¬H a = H j}, g x • (↑(H x) : Set G)) y
Tactic: cases (Set.mem_union _ _ _).mp (hcovers.superset (Set.mem_univ y)) with
      | inl hy =>
        have ⟨k, hk, hy⟩ := Set.mem_iUnion₂.mp hy
        have hk' : H k = H j := And.right <| by simpa using hk
        have ⟨i, hi, hy⟩ := Set.mem_iUnion₂.mp (hx (g k) (hk' ▸ hy))
        exact ⟨⟨⟨i, hi⟩, some ⟨k, hk⟩⟩, Finset.mem_univ _, hy⟩
      | inr hy =>
        have ⟨i, hi, hy⟩ := Set.mem_iUnion₂.mp hy
        exact ⟨⟨⟨i, hi⟩, none⟩, Finset.mem_univ _, hy⟩
-- 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 ι
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 : 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
⊢ ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
have hcovers₁ : Eq.{u_1 + 1} (α := Set G) (⋃ (k : κ), ⋃ (_ : Membership.mem (γ := Finset κ) Finset.univ k), f k • (↑(K k) : Set G))
  Set.univ
Tactic: replace hcovers : ⋃ k ∈ Finset.univ, f k • (K k : Set G) = Set.univ :=
        Set.iUnion₂_eq_univ_iff.mpr fun y => by
      rw [← s.filter_union_filter_not_eq (H · = H j), Finset.set_biUnion_union] at hcovers
      cases (Set.mem_union _ _ _).mp (hcovers.superset (Set.mem_univ y)) with
      | inl hy =>
        have ⟨k, hk, hy⟩ := Set.mem_iUnion₂.mp hy
        have hk' : H k = H j := And.right <| by simpa using hk
        have ⟨i, hi, hy⟩ := Set.mem_iUnion₂.mp (hx (g k) (hk' ▸ hy))
        exact ⟨⟨⟨i, hi⟩, some ⟨k, hk⟩⟩, Finset.mem_univ _, hy⟩
      | inr hy =>
        have ⟨i, hi, hy⟩ := Set.mem_iUnion₂.mp hy
        exact ⟨⟨⟨i, hi⟩, none⟩, Finset.mem_univ _, hy⟩
Cleared hypotheses: hcovers
-- 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' : 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
hempty : IsEmpty κ
⊢ False
have hcovers₁ : Eq.{u_1 + 1} (α := Set G) ∅ Set.univ
Tactic: rw [Set.iUnion_of_empty] at hcovers
Cleared hypotheses: hcovers, hempty
-- 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' : 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
⊢ ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
have ind : ∀ (k : κ), ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
Tactic: have ⟨k⟩ : Nonempty κ := not_isEmpty_iff.mp fun hempty => by
      rw [Set.iUnion_of_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
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' : 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 : κ
⊢ ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
have pos : ∀
  (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
Tactic: by_cases hcovers' : ⋃ i ∈ Finset.filter (K · = K k) Finset.univ, f i • (K i : Set G) = Set.univ
-- 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' : 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 : κ
pos :
  ∀
    (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
⊢ ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
have neg : ∀
  (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
Tactic: by_cases hcovers' : ⋃ i ∈ Finset.filter (K · = K k) Finset.univ, f i • (K i : Set G) = Set.univ
-- 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
i : κ
hi : Membership.mem (γ := Finset κ) {x : κ | K x = K k} i
⊢ f i • (↑(K i) : Set G) = f i • (↑(K k) : Set G)
have rw : f i • (↑(K k) : Set G) = f i • (↑(K k) : Set G)
Tactic: rw [(Finset.mem_filter.mp hi).right]