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
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑H : Set G)) Set.univ
hind : H.index = s.card
this : Fintype (G ⧸ H)
left : Function.Surjective.{u_2 + 1, u_1 + 1} (β := G ⧸ H) fun (x : ↥s) ↦ (↑(g (↑x : ι)) : G ⧸ H)
⊢ (Function.Surjective.{u_2 + 1, u_1 + 1} (β := G ⧸ H) fun (x : ↥s) ↦ (↑(g (↑x : ι)) : G ⧸ H)) ∧
    Fintype.card.{u_2} ↥s = Fintype.card.{u_1} (G ⧸ H)
have right : Fintype.card.{u_2} ↥s = Fintype.card.{u_1} (G ⧸ H)
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (goal)
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑H : Set G)) Set.univ
hind : H.index = s.card
this : Fintype (G ⧸ H)
⊢ Function.Surjective.{u_2 + 1, u_1 + 1} (β := G ⧸ H) fun (x : ↥s) ↦ (↑(g (↑x : ι)) : G ⧸ H)
have left : ∀ (hcovers : Set.SurjOn.{u_2, u_1} (β := G ⧸ H) (fun (x : ι) ↦ (↑(g x) : G ⧸ H)) (↑s : Set ι) Set.univ)
  (hind : H.index = s.card) (this : Fintype (G ⧸ H)),
  Function.Surjective.{u_2 + 1, u_1 + 1} (β := G ⧸ H) fun (x : ↥s) ↦ (↑(g (↑x : ι)) : G ⧸ H)
Tactic: rwa [leftCoset_cover_const_iff_surjOn, Set.surjOn_iff_surjective] at hcovers
Cleared hypotheses: hcovers, hind, this
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (goal)
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑H : Set G)) Set.univ
hind : H.index = s.card
this : Fintype (G ⧸ H)
left :
  ∀ (hcovers : Set.SurjOn.{u_2, u_1} (β := G ⧸ H) (fun (x : ι) ↦ (↑(g x) : G ⧸ H)) (↑s : Set ι) Set.univ)
    (hind : H.index = s.card) (this : Fintype (G ⧸ H)),
    Function.Surjective.{u_2 + 1, u_1 + 1} (β := G ⧸ H) fun (x : ↥s) ↦ (↑(g (↑x : ι)) : G ⧸ H)
⊢ Function.Surjective.{u_2 + 1, u_1 + 1} (β := G ⧸ H) fun (x : ↥s) ↦ (↑(g (↑x : ι)) : G ⧸ H)
have left₁ : ∀
  (hcovers :
    Function.Surjective.{u_2 + 1, u_1 + 1} (α := (↑(↑s : Set ι) : Type u_2)) (β := G ⧸ H)
      ((↑s : Set ι).restrict (π := fun (a : ι) ↦ G ⧸ H) fun (x : ι) ↦ (↑(g x) : G ⧸ H)))
  (hind : H.index = s.card) (this : Fintype (G ⧸ H)),
  Function.Surjective.{u_2 + 1, u_1 + 1} (β := G ⧸ H) fun (x : ↥s) ↦ (↑(g (↑x : ι)) : G ⧸ H)
Tactic: rwa [leftCoset_cover_const_iff_surjOn, Set.surjOn_iff_surjective] at hcovers
Cleared hypotheses: hcovers, hind, this
-- 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 : DecidableEq (Subgroup G)
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
⊢ ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
have have : ∀ (n : ℕ) (hn : n = (Finset.image H s).card), ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
Tactic: have ⟨n, hn⟩ : ∃ n, n = (s.image H).card := exists_eq
-- 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
⊢ ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
have ind : ∀ (x : G) (hx : ∀ i ∈ s, H i = H j → Ne (α := G ⧸ H i) (↑(g i) : G ⧸ H i) (↑x : G ⧸ H i)),
  ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
Tactic: have ⟨x, hx⟩ : ∃ (x : G), ∀ i ∈ s, H i = H j → (g i : G ⧸ H i) ≠ ↑x := by
      simpa [Set.eq_univ_iff_forall, mem_leftCoset_iff, ← QuotientGroup.eq] using 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 ι
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 : ∀ i ∈ s, H i = H j → Ne (α := G ⧸ H i) (↑(g i) : G ⧸ H i) (↑x : G ⧸ H i)
y z : G
hz : z ∈ y • (↑(H j) : Set G)
⊢ Membership.mem (γ := Set G) (⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • (↑(H i) : Set G)) z
have simp_rw : ∃ (i : ι) (_ : i ∈ s ∧ H i ≠ H j), z ∈ (y * x⁻¹ * g i) • (↑(H i) : Set G)
Tactic: simp_rw [Finset.mem_filter, Set.mem_iUnion]
-- 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 : ∀ i ∈ s, H i = H j → Ne (α := G ⧸ H i) (↑(g i) : G ⧸ H i) (↑x : G ⧸ H i)
y z : G
hz : z ∈ y • (↑(H j) : Set G)
⊢ ∃ (i : ι) (_ : i ∈ s ∧ H i ≠ H j), z ∈ (y * x⁻¹ * g i) • (↑(H i) : Set G)
have have : ∀ (i : ι) (hi : i ∈ s) (hmem : x * (y⁻¹ * z) ∈ g i • (↑(H i) : Set G)),
  ∃ (i : ι) (_ : i ∈ s ∧ H i ≠ H j), z ∈ (y * x⁻¹ * g i) • (↑(H i) : Set G)
Tactic: have ⟨i, hi, hmem⟩ : ∃ i ∈ s, x * (y⁻¹ * z) ∈ g i • (H i : Set G) := by
        simpa using Set.eq_univ_iff_forall.mp hcovers (x * (y⁻¹ * z))
-- 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 : ∀ i ∈ s, H i = H j → Ne (α := G ⧸ H i) (↑(g i) : G ⧸ H i) (↑x : G ⧸ H i)
y z : G
hz : z ∈ y • (↑(H j) : Set G)
i : ι
hi : i ∈ s
hmem : x * (y⁻¹ * z) ∈ g i • (↑(H i) : Set G)
⊢ ∃ (i : ι) (_ : i ∈ s ∧ H i ≠ H j), z ∈ (y * x⁻¹ * g i) • (↑(H i) : Set G)
have hmem₁ : Eq (α := G ⧸ H i) (↑(g i) : G ⧸ H i) (↑(x * (y⁻¹ * z)) : G ⧸ H i)
Tactic: rw [mem_leftCoset_iff, SetLike.mem_coe, ← QuotientGroup.eq] at hmem
Cleared hypotheses: hmem
-- 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 : ∀ i ∈ s, H i = H j → Ne (α := G ⧸ H i) (↑(g i) : G ⧸ H i) (↑x : G ⧸ H i)
y z : G
hz : z ∈ y • (↑(H j) : Set G)
i : ι
hi : i ∈ s
hmem : Eq (α := G ⧸ H i) (↑(g i) : G ⧸ H i) (↑(x * (y⁻¹ * z)) : G ⧸ H i)
⊢ ∃ (i : ι) (_ : i ∈ s ∧ H i ≠ H j), z ∈ (y * x⁻¹ * g i) • (↑(H i) : Set G)
have refine_1 : ∀ (hij : H i = H j), Eq (α := G ⧸ H i) (↑(g i) : G ⧸ H i) (↑x : G ⧸ H i)
Tactic: refine ⟨i, ⟨hi, fun hij => hx i hi hij ?_⟩, ?_⟩
-- 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 : ∀ i ∈ s, H i = H j → Ne (α := G ⧸ H i) (↑(g i) : G ⧸ H i) (↑x : G ⧸ H i)
y z : G
hz : z ∈ y • (↑(H j) : Set G)
i : ι
hi : i ∈ s
hmem : Eq (α := G ⧸ H i) (↑(g i) : G ⧸ H i) (↑(x * (y⁻¹ * z)) : G ⧸ H i)
refine_1 : ∀ (hij : H i = H j), Eq (α := G ⧸ H i) (↑(g i) : G ⧸ H i) (↑x : G ⧸ H i)
⊢ ∃ (i : ι) (_ : i ∈ s ∧ H i ≠ H j), z ∈ (y * x⁻¹ * g i) • (↑(H i) : Set G)
have refine_2 : z ∈ (y * x⁻¹ * g i) • (↑(H i) : Set G)
Tactic: refine ⟨i, ⟨hi, fun hij => hx i hi hij ?_⟩, ?_⟩
-- 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 : ∀ i ∈ s, H i = H j → Ne (α := G ⧸ H i) (↑(g i) : G ⧸ H i) (↑x : G ⧸ H i)
y z : G
hz : z ∈ y • (↑(H j) : Set G)
i : ι
hi : i ∈ s
hmem : Eq (α := G ⧸ H i) (↑(g i) : G ⧸ H i) (↑(x * (y⁻¹ * z)) : G ⧸ H i)
hij : H i = H j
⊢ Eq (α := G ⧸ H i) (↑(g i) : G ⧸ H i) (↑x : G ⧸ H i)
have refine_1 : Eq (α := G ⧸ H i) (↑(x * (y⁻¹ * z)) : G ⧸ H i) (↑x : G ⧸ H i)
Tactic: rwa [hmem, eq_comm, QuotientGroup.eq, hij, inv_mul_cancel_left,
          ← SetLike.mem_coe, ← mem_leftCoset_iff]
-- 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 : ∀ i ∈ s, H i = H j → Ne (α := G ⧸ H i) (↑(g i) : G ⧸ H i) (↑x : G ⧸ H i)
y z : G
hz : z ∈ y • (↑(H j) : Set G)
i : ι
hi : i ∈ s
hmem : Eq (α := G ⧸ H i) (↑(g i) : G ⧸ H i) (↑(x * (y⁻¹ * z)) : G ⧸ H i)
hij : H i = H j
refine_1 : Eq (α := G ⧸ H i) (↑(x * (y⁻¹ * z)) : G ⧸ H i) (↑x : G ⧸ H i)
⊢ Eq (α := G ⧸ H i) (↑(g i) : G ⧸ H i) (↑x : G ⧸ H i)
have refine_1₁ : Eq (α := G ⧸ H i) (↑x : G ⧸ H i) (↑(x * (y⁻¹ * z)) : G ⧸ H i)
Tactic: rwa [hmem, eq_comm, QuotientGroup.eq, hij, inv_mul_cancel_left,
          ← SetLike.mem_coe, ← mem_leftCoset_iff]
-- 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 : ∀ i ∈ s, H i = H j → Ne (α := G ⧸ H i) (↑(g i) : G ⧸ H i) (↑x : G ⧸ H i)
y z : G
hz : z ∈ y • (↑(H j) : Set G)
i : ι
hi : i ∈ s
hmem : Eq (α := G ⧸ H i) (↑(g i) : G ⧸ H i) (↑(x * (y⁻¹ * z)) : G ⧸ H i)
hij : H i = H j
refine_1 : Eq (α := G ⧸ H i) (↑(x * (y⁻¹ * z)) : G ⧸ H i) (↑x : G ⧸ H i)
refine_1₁ : Eq (α := G ⧸ H i) (↑x : G ⧸ H i) (↑(x * (y⁻¹ * z)) : G ⧸ H i)
⊢ Eq (α := G ⧸ H i) (↑(g i) : G ⧸ H i) (↑x : G ⧸ H i)
have refine_1₂ : x⁻¹ * (x * (y⁻¹ * z)) ∈ H i
Tactic: rwa [hmem, eq_comm, QuotientGroup.eq, hij, inv_mul_cancel_left,
          ← SetLike.mem_coe, ← mem_leftCoset_iff]
-- 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 : ∀ i ∈ s, H i = H j → Ne (α := G ⧸ H i) (↑(g i) : G ⧸ H i) (↑x : G ⧸ H i)
y z : G
hz : z ∈ y • (↑(H j) : Set G)
i : ι
hi : i ∈ s
hmem : Eq (α := G ⧸ H i) (↑(g i) : G ⧸ H i) (↑(x * (y⁻¹ * z)) : G ⧸ H i)
hij : H i = H j
refine_1 : Eq (α := G ⧸ H i) (↑(x * (y⁻¹ * z)) : G ⧸ H i) (↑x : G ⧸ H i)
refine_1₁ : Eq (α := G ⧸ H i) (↑x : G ⧸ H i) (↑(x * (y⁻¹ * z)) : G ⧸ H i)
refine_1₂ : x⁻¹ * (x * (y⁻¹ * z)) ∈ H i
⊢ Eq (α := G ⧸ H i) (↑(g i) : G ⧸ H i) (↑x : G ⧸ H i)
have refine_1₃ : x⁻¹ * (x * (y⁻¹ * z)) ∈ H j
Tactic: rwa [hmem, eq_comm, QuotientGroup.eq, hij, inv_mul_cancel_left,
          ← SetLike.mem_coe, ← mem_leftCoset_iff]
-- 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 : ∀ i ∈ s, H i = H j → Ne (α := G ⧸ H i) (↑(g i) : G ⧸ H i) (↑x : G ⧸ H i)
y z : G
hz : z ∈ y • (↑(H j) : Set G)
i : ι
hi : i ∈ s
hmem : Eq (α := G ⧸ H i) (↑(g i) : G ⧸ H i) (↑(x * (y⁻¹ * z)) : G ⧸ H i)
hij : H i = H j
refine_1 : Eq (α := G ⧸ H i) (↑(x * (y⁻¹ * z)) : G ⧸ H i) (↑x : G ⧸ H i)
refine_1₁ : Eq (α := G ⧸ H i) (↑x : G ⧸ H i) (↑(x * (y⁻¹ * z)) : G ⧸ H i)
refine_1₂ : x⁻¹ * (x * (y⁻¹ * z)) ∈ H i
refine_1₃ : x⁻¹ * (x * (y⁻¹ * z)) ∈ H j
⊢ Eq (α := G ⧸ H i) (↑(g i) : G ⧸ H i) (↑x : G ⧸ H i)
have refine_1₄ : y⁻¹ * z ∈ H j
Tactic: rwa [hmem, eq_comm, QuotientGroup.eq, hij, inv_mul_cancel_left,
          ← SetLike.mem_coe, ← mem_leftCoset_iff]
-- 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 : ∀ i ∈ s, H i = H j → Ne (α := G ⧸ H i) (↑(g i) : G ⧸ H i) (↑x : G ⧸ H i)
y z : G
hz : z ∈ y • (↑(H j) : Set G)
i : ι
hi : i ∈ s
hmem : Eq (α := G ⧸ H i) (↑(g i) : G ⧸ H i) (↑(x * (y⁻¹ * z)) : G ⧸ H i)
hij : H i = H j
refine_1 : Eq (α := G ⧸ H i) (↑(x * (y⁻¹ * z)) : G ⧸ H i) (↑x : G ⧸ H i)
refine_1₁ : Eq (α := G ⧸ H i) (↑x : G ⧸ H i) (↑(x * (y⁻¹ * z)) : G ⧸ H i)
refine_1₂ : x⁻¹ * (x * (y⁻¹ * z)) ∈ H i
refine_1₃ : x⁻¹ * (x * (y⁻¹ * z)) ∈ H j
refine_1₄ : y⁻¹ * z ∈ H j
⊢ Eq (α := G ⧸ H i) (↑(g i) : G ⧸ H i) (↑x : G ⧸ H i)
have refine_1₅ : y⁻¹ * z ∈ (↑(H j) : Set G)
Tactic: rwa [hmem, eq_comm, QuotientGroup.eq, hij, inv_mul_cancel_left,
          ← SetLike.mem_coe, ← mem_leftCoset_iff]
-- 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 : ∀ i ∈ s, H i = H j → Ne (α := G ⧸ H i) (↑(g i) : G ⧸ H i) (↑x : G ⧸ H i)
⊢ ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
have hx₁ : ∀ (y : G), y • (↑(H j) : Set G) ⊆ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • (↑(H i) : Set G)
Tactic: replace hx : ∀ (y : G), y • (H j : Set G) ⊆
        ⋃ i ∈ s.filter (H · ≠ H j), (y * x⁻¹ * g i) • (H i : Set G) := by
      intro y z hz
      simp_rw [Finset.mem_filter, Set.mem_iUnion]
      have ⟨i, hi, hmem⟩ : ∃ i ∈ s, x * (y⁻¹ * z) ∈ g i • (H i : Set G) := by
        simpa using Set.eq_univ_iff_forall.mp hcovers (x * (y⁻¹ * z))
      rw [mem_leftCoset_iff, SetLike.mem_coe, ← QuotientGroup.eq] at hmem
      refine ⟨i, ⟨hi, fun hij => hx i hi hij ?_⟩, ?_⟩
      · rwa [hmem, eq_comm, QuotientGroup.eq, hij, inv_mul_cancel_left,
          ← SetLike.mem_coe, ← mem_leftCoset_iff]
      · simpa [mem_leftCoset_iff, SetLike.mem_coe, QuotientGroup.eq, mul_assoc] using hmem
Cleared hypotheses: hx
-- 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 : ι)
k : κ
⊢ K k ∈ (Finset.image H s).erase (H j)
have this : (↑k.1 : ι) ∈ s ∧ H (↑k.1 : ι) ≠ H j
Tactic: have := Finset.mem_filter.mp k.1.property
-- 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 : ι)
⊢ ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
have hK' : ∀ (k : κ), K k ∈ (Finset.image H s).erase (H j)
Tactic: have hK' (k : κ) : K k ∈ (s.image H).erase (H j) := by
      have := Finset.mem_filter.mp k.1.property
      exact Finset.mem_erase.mpr ⟨this.2, Finset.mem_image_of_mem H this.1⟩