awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.CosetCover
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
h : s = ∅
hcovers₁ : Eq.{u_1 + 1} (α := Set G) ∅ Set.univ
⊢ H.index = s.card

Tactic:
rw [h, ← Finset.set_biUnion_coe, Finset.coe_empty, Set.biUnion_empty] at hcovers

Premises used: Finset.coe_empty, Finset.set_biUnion_coe, Set.biUnion_empty
-- Module: Mathlib.GroupTheory.CosetCover
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
h : s = ∅
hcovers₁ : Eq.{u_1 + 1} (α := Set G) ∅ Set.univ
hind₁ : H.index = s.card
⊢ s = ∅

Tactic:
rw [h, ← Finset.set_biUnion_coe, Finset.coe_empty, Set.biUnion_empty] at hcovers

Premises used: Finset.coe_empty, Finset.set_biUnion_coe, Set.biUnion_empty
-- Module: Mathlib.GroupTheory.CosetCover
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) ∅ Set.univ
hind : H.index = s.card
h : s = ∅
⊢ False

Tactic:
Set.empty_ne_univ hcovers

Premises used: Set.empty_ne_univ
-- Module: Mathlib.GroupTheory.CosetCover
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) ∅ Set.univ
hind : H.index = s.card
h : s = ∅
⊢ False

Tactic:
exact Set.empty_ne_univ hcovers

Premises used: Set.empty_ne_univ
-- Module: Mathlib.GroupTheory.CosetCover
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
have :
  ∀ (this : Fintype (G ⧸ H)), Set.PairwiseDisjoint.{u_1, u_2} (α := Set G) (↑s : Set ι) fun (x : ι) ↦ g x • (↑H : Set G)
⊢ Set.PairwiseDisjoint.{u_1, u_2} (α := Set G) (↑s : Set ι) fun (x : ι) ↦ g x • (↑H : Set G)

Tactic:
have : Fintype (G ⧸ H) := fintypeOfIndexNeZero fun h => by
    rw [hind, Finset.card_eq_zero] at h
    rw [h, ← Finset.set_biUnion_coe, Finset.coe_empty, Set.biUnion_empty] at hcovers
    exact Set.empty_ne_univ hcovers
-- Module: Mathlib.GroupTheory.CosetCover
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_1 : Fintype (G ⧸ H)
this : Function.Bijective.{u_2 + 1, u_1 + 1} (β := G ⧸ H) fun (x : ↥s) ↦ (↑(g (↑x : ι)) : G ⧸ H)
i : ι
hi : i ∈ (↑s : Set ι)
j : ι
hj : j ∈ (↑s : Set ι)
h' : i ≠ j
c : Set G
hi' : c ≤ (fun (x : ι) ↦ g x • (↑H : Set G)) i
hj' : c ≤ (fun (x : ι) ↦ g x • (↑H : Set G)) j
x : G
hx : x ∈ c
⊢ Membership.mem (γ := Set G) ((fun (x : ι) ↦ g x • (↑H : Set G)) i) x

Tactic:
specialize hi' hx
-- Module: Mathlib.GroupTheory.CosetCover
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_1 : Fintype (G ⧸ H)
this : Function.Bijective.{u_2 + 1, u_1 + 1} (β := G ⧸ H) fun (x : ↥s) ↦ (↑(g (↑x : ι)) : G ⧸ H)
i : ι
hi : i ∈ (↑s : Set ι)
j : ι
hj : j ∈ (↑s : Set ι)
h' : i ≠ j
c : Set G
hj' : c ≤ (fun (x : ι) ↦ g x • (↑H : Set G)) j
x : G
hx : x ∈ c
hi' : Membership.mem (γ := Set G) ((fun (x : ι) ↦ g x • (↑H : Set G)) i) x
⊢ Membership.mem (γ := Set G) ((fun (x : ι) ↦ g x • (↑H : Set G)) j) x

Tactic:
specialize hj' hx
-- Module: Mathlib.GroupTheory.CosetCover
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_1 : Fintype (G ⧸ H)
this : Function.Bijective.{u_2 + 1, u_1 + 1} (β := G ⧸ H) fun (x : ↥s) ↦ (↑(g (↑x : ι)) : G ⧸ H)
i : ι
hi : i ∈ (↑s : Set ι)
j : ι
hj : j ∈ (↑s : Set ι)
h' : i ≠ j
c : Set G
x : G
hx : x ∈ c
hi' : Membership.mem (γ := Set G) ((fun (x : ι) ↦ g x • (↑H : Set G)) i) x
hj' : Membership.mem (γ := Set G) ((fun (x : ι) ↦ g x • (↑H : Set G)) j) x
⊢ Eq (α := G ⧸ H) (↑(g i) : G ⧸ H) (↑x : G ⧸ H)

Tactic:
rw [mem_leftCoset_iff, SetLike.mem_coe, ← QuotientGroup.eq] at hi' hj'

Premises used: mem_leftCoset_iff, QuotientGroup.eq, SetLike.mem_coe
-- Module: Mathlib.GroupTheory.CosetCover
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_1 : Fintype (G ⧸ H)
this : Function.Bijective.{u_2 + 1, u_1 + 1} (β := G ⧸ H) fun (x : ↥s) ↦ (↑(g (↑x : ι)) : G ⧸ H)
i : ι
hi : i ∈ (↑s : Set ι)
j : ι
hj : j ∈ (↑s : Set ι)
h' : i ≠ j
c : Set G
x : G
hx : x ∈ c
hi' : Membership.mem (γ := Set G) ((fun (x : ι) ↦ g x • (↑H : Set G)) i) x
hj' : Membership.mem (γ := Set G) ((fun (x : ι) ↦ g x • (↑H : Set G)) j) x
hi'₁ : Eq (α := G ⧸ H) (↑(g i) : G ⧸ H) (↑x : G ⧸ H)
⊢ Eq (α := G ⧸ H) (↑(g j) : G ⧸ H) (↑x : G ⧸ H)

Tactic:
rw [mem_leftCoset_iff, SetLike.mem_coe, ← QuotientGroup.eq] at hi' hj'

Premises used: mem_leftCoset_iff, QuotientGroup.eq, SetLike.mem_coe
-- Module: Mathlib.GroupTheory.CosetCover
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_1 : Fintype (G ⧸ H)
this : Function.Bijective.{u_2 + 1, u_1 + 1} (β := G ⧸ H) fun (x : ↥s) ↦ (↑(g (↑x : ι)) : G ⧸ H)
i : ι
hi : i ∈ (↑s : Set ι)
j : ι
hj : j ∈ (↑s : Set ι)
h' : i ≠ j
c : Set G
x : G
hx : x ∈ c
hi' : Eq (α := G ⧸ H) (↑(g i) : G ⧸ H) (↑x : G ⧸ H)
hj' : Eq (α := G ⧸ H) (↑(g j) : G ⧸ H) (↑x : G ⧸ H)
rw :
  ∀
    (h' :
      ¬Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i hi = Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) j hj)
    ⦃c : Set G⦄ ⦃x : G⦄ (hx : x ∈ c) (hi' : Eq (α := G ⧸ H) (↑(g i) : G ⧸ H) (↑x : G ⧸ H))
    (hj' : Eq (α := G ⧸ H) (↑(g j) : G ⧸ H) (↑x : G ⧸ H)), Membership.mem (γ := Set G) ⊥ x
⊢ Membership.mem (γ := Set G) ⊥ x

Tactic:
rw [ne_eq, ← Subtype.mk.injEq (p := (· ∈ (s : Set ι))) i hi j hj] at h'

Premises used: ne_eq, Subtype.mk.injEq
-- Module: Mathlib.GroupTheory.CosetCover
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_1 : Fintype (G ⧸ H)
this : Function.Bijective.{u_2 + 1, u_1 + 1} (β := G ⧸ H) fun (x : ↥s) ↦ (↑(g (↑x : ι)) : G ⧸ H)
i : ι
hi : i ∈ (↑s : Set ι)
j : ι
hj : j ∈ (↑s : Set ι)
h' : ¬Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i hi = Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) j hj
c : Set G
x : G
hx : x ∈ c
hi' : Eq (α := G ⧸ H) (↑(g i) : G ⧸ H) (↑x : G ⧸ H)
hj' : Eq (α := G ⧸ H) (↑(g j) : G ⧸ H) (↑x : G ⧸ H)
⊢ Eq (α := G ⧸ H) (↑(g (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i hi) : ι)) : G ⧸ H)
    (↑(g (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) j hj) : ι)) : G ⧸ H)

Tactic:
simp only [hi', hj']
-- Module: Mathlib.GroupTheory.CosetCover
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_1 : Fintype (G ⧸ H)
this : Function.Bijective.{u_2 + 1, u_1 + 1} (β := G ⧸ H) fun (x : ↥s) ↦ (↑(g (↑x : ι)) : G ⧸ H)
i : ι
hi : i ∈ (↑s : Set ι)
j : ι
hj : j ∈ (↑s : Set ι)
h' : ¬Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i hi = Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) j hj
c : Set G
x : G
hx : x ∈ c
hi' : Eq (α := G ⧸ H) (↑(g i) : G ⧸ H) (↑x : G ⧸ H)
hj' : Eq (α := G ⧸ H) (↑(g j) : G ⧸ H) (↑x : G ⧸ H)
⊢ Membership.mem (γ := Set G) ⊥ x

Tactic:
exact h' <| this.injective <| by simp only [hi', hj']

Premises used: Function.Bijective.injective
-- Module: Mathlib.GroupTheory.CosetCover
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)
suffices : Function.Bijective.{u_2 + 1, u_1 + 1} (β := G ⧸ H) fun (x : ↥s) ↦ (↑(g (↑x : ι)) : G ⧸ H)
⊢ Set.PairwiseDisjoint.{u_1, u_2} (α := Set G) (↑s : Set ι) fun (x : ι) ↦ g x • (↑H : Set G)

Tactic:
suffices Function.Bijective (g · : s → G ⧸ H) by
    intro i hi j hj h' c hi' hj' x hx
    specialize hi' hx
    specialize hj' hx
    rw [mem_leftCoset_iff, SetLike.mem_coe, ← QuotientGroup.eq] at hi' hj'
    rw [ne_eq, ← Subtype.mk.injEq (p := (· ∈ (s : Set ι))) i hi j hj] at h'
    exact h' <| this.injective <| by simp only [hi', hj']
-- Module: Mathlib.GroupTheory.CosetCover
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)
rw :
  (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)
⊢ Function.Bijective.{u_2 + 1, u_1 + 1} (β := G ⧸ H) fun (x : ↥s) ↦ (↑(g (↑x : ι)) : G ⧸ H)

Tactic:
rw [Fintype.bijective_iff_surjective_and_card]

Premises used: Fintype.bijective_iff_surjective_and_card
-- Module: Mathlib.GroupTheory.CosetCover
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)
right : Fintype.card.{u_2} ↥s = Fintype.card.{u_1} (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)

Tactic:
constructor
-- Module: Mathlib.GroupTheory.CosetCover
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)
left₁ left₂ left₃ 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)
⊢ 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

Premises used: Set.surjOn_iff_surjective, Subgroup.leftCoset_cover_const_iff_surjOn
-- Module: Mathlib.GroupTheory.CosetCover
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)
⊢ Fintype.card.{u_2} ↥s = Fintype.card.{u_1} (G ⧸ H)

Tactic:
simp only [Fintype.card_coe, ← hind, index_eq_card, Nat.card_eq_fintype_card]

Premises used: Subgroup.index_eq_card, Fintype.card_coe, Nat.card_eq_fintype_card
-- 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 : 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
have : ∀ (n : ℕ) (hn : n = (Finset.image H s).card), ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
⊢ ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex

Tactic:
have ⟨n, hn⟩ : ∃ n, n = (s.image H).card := exists_eq
-- Module: Mathlib.GroupTheory.CosetCover
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), ∀ i ∈ s, H i = H j → Ne (α := G ⧸ H i) (↑(g i) : G ⧸ H i) (↑x : G ⧸ H i)

Tactic:
simpa [Set.eq_univ_iff_forall, mem_leftCoset_iff, ← QuotientGroup.eq] using hcovers'

Premises used: mem_leftCoset_iff, Set.eq_univ_iff_forall, QuotientGroup.eq
-- Module: Mathlib.GroupTheory.CosetCover
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
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
⊢ ∃ 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'
-- Module: Mathlib.GroupTheory.CosetCover
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)
simp_rw : ∃ (i : ι) (_ : i ∈ s ∧ H i ≠ H j), z ∈ (y * x⁻¹ * g i) • (↑(H i) : Set G)
⊢ Membership.mem (γ := Set G) (⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • (↑(H i) : Set G)) z

Tactic:
simp_rw [Finset.mem_filter, Set.mem_iUnion]

Premises used: Set.mem_iUnion, Finset.mem_filter
-- Module: Mathlib.GroupTheory.CosetCover
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 ∈ s, x * (y⁻¹ * z) ∈ g i • (↑(H i) : Set G)

Tactic:
simpa using Set.eq_univ_iff_forall.mp hcovers (x * (y⁻¹ * z))

Premises used: HMul.hMul, Set.eq_univ_iff_forall, Inv.inv, Iff.mp
-- Module: Mathlib.GroupTheory.CosetCover
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)
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)
⊢ ∃ (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))
-- Module: Mathlib.GroupTheory.CosetCover
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)
⊢ 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

Premises used: mem_leftCoset_iff, QuotientGroup.eq, SetLike.mem_coe
-- Module: Mathlib.GroupTheory.CosetCover
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)

Tactic:
⟨i, ⟨hi, fun hij => hx i hi hij ?_⟩, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.GroupTheory.CosetCover
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)
refine_2 : z ∈ (y * x⁻¹ * g i) • (↑(H i) : Set G)
⊢ ∃ (i : ι) (_ : i ∈ s ∧ H i ≠ H j), z ∈ (y * x⁻¹ * g i) • (↑(H i) : Set G)

Tactic:
refine ⟨i, ⟨hi, fun hij => hx i hi hij ?_⟩, ?_⟩
-- Module: Mathlib.GroupTheory.CosetCover
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
refine_1₅ : y⁻¹ * z ∈ (↑(H j) : Set G)
refine_1₆ refine_1₇ refine_1₈ refine_1₉ : z ∈ y • (↑(H j) : Set G)
⊢ Eq (α := G ⧸ H i) (↑(g i) : 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]

Premises used: mem_leftCoset_iff, inv_mul_cancel_left, QuotientGroup.eq, eq_comm, SetLike.mem_coe
-- Module: Mathlib.GroupTheory.CosetCover
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)
⊢ z ∈ (y * x⁻¹ * g i) • (↑(H i) : Set G)

Tactic:
simpa [mem_leftCoset_iff, SetLike.mem_coe, QuotientGroup.eq, mul_assoc] using hmem

Premises used: mem_leftCoset_iff, mul_assoc, QuotientGroup.eq, SetLike.mem_coe