awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
t : Set (α ⧸ s)
x_1 : ↥s × (↑t : Type u_1)
a : α
ha : a ∈ s
x : α ⧸ s
hx : x ∈ t
fst :
  (↑((fun (a : (↑(mk ⁻¹' t) : Type u_1)) ↦
              (Subtype.mk (p := fun (x : α) ↦ x ∈ s) ((Quotient.out (s := leftRel s) (↑(↑a : α) : α ⧸ s))⁻¹ * (↑a : α))
                  ⋯,
                Subtype.mk (p := fun (x : α ⧸ s) ↦ x ∈ t) (↑(↑a : α) : α ⧸ s) ⋯))
            ((fun (a : ↥s × (↑t : Type u_1)) ↦
                (Subtype.mk (p := fun (x : α) ↦ x ∈ mk ⁻¹' t) (Quotient.out (↑a.2 : α ⧸ s) * (↑a.1 : α)) ⋯ :
                  { x : α // x ∈ mk ⁻¹' t }))
              (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha, Subtype.mk (p := fun (x : α ⧸ s) ↦ x ∈ t) x hx))).1 :
      α) =
    (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha, Subtype.mk (p := fun (x : α ⧸ s) ↦ x ∈ t) x hx).1 : α)
⊢ (fun (a : (↑(mk ⁻¹' t) : Type u_1)) ↦
        (Subtype.mk (p := fun (x : α) ↦ x ∈ s) ((Quotient.out (s := leftRel s) (↑(↑a : α) : α ⧸ s))⁻¹ * (↑a : α)) ⋯,
          Subtype.mk (p := fun (x : α ⧸ s) ↦ x ∈ t) (↑(↑a : α) : α ⧸ s) ⋯))
      ((fun (a : ↥s × (↑t : Type u_1)) ↦
          (Subtype.mk (p := fun (x : α) ↦ x ∈ mk ⁻¹' t) (Quotient.out (↑a.2 : α ⧸ s) * (↑a.1 : α)) ⋯ :
            { x : α // x ∈ mk ⁻¹' t }))
        (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha, Subtype.mk (p := fun (x : α ⧸ s) ↦ x ∈ t) x hx)) =
    (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha, Subtype.mk (p := fun (x : α ⧸ s) ↦ x ∈ t) x hx)
have snd : (↑((fun (a : (↑(mk ⁻¹' t) : Type u_1)) ↦
            (Subtype.mk (p := fun (x : α) ↦ x ∈ s) ((Quotient.out (s := leftRel s) (↑(↑a : α) : α ⧸ s))⁻¹ * (↑a : α)) sorry,
              Subtype.mk (p := fun (x : α ⧸ s) ↦ x ∈ t) (↑(↑a : α) : α ⧸ s) sorry))
          ((fun (a : ↥s × (↑t : Type u_1)) ↦
              (Subtype.mk (p := fun (x : α) ↦ x ∈ mk ⁻¹' t) (Quotient.out (↑a.2 : α ⧸ s) * (↑a.1 : α)) sorry :
                { x : α // x ∈ mk ⁻¹' t }))
            (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha, Subtype.mk (p := fun (x : α ⧸ s) ↦ x ∈ t) x hx))).2 :
    α ⧸ s) =
  (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha, Subtype.mk (p := fun (x : α ⧸ s) ↦ x ∈ t) x hx).2 : α ⧸ s)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
H : Subgroup α
⊢ Eq.{u_1 + 1} (α := Set α) univ (⋃ (x : α ⧸ H), Quotient.out x • (↑H : Set α))
have simp_rw : Eq.{u_1 + 1} (α := Set α) (⋃ (x : orbitRel.Quotient (↥H.op) α), Quotient.out x • (↑H : Set α))
  (⋃ (x : α ⧸ H), Quotient.out x • (↑H : Set α))
Tactic: simp_rw [univ_eq_iUnion_orbit H.op, orbit_eq_out_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
x y : α
h : (leftRel ⊥ : α → α → Prop) x y
⊢ (id x)⁻¹ * id y = 1
have rwa : ∀ (h : Membership.mem (γ := Subgroup α) ⊥ (x⁻¹ * y)), (id x)⁻¹ * id y = 1
Tactic: rwa [leftRel_apply, Subgroup.mem_bot] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
x y : α
h : (leftRel ⊥ : α → α → Prop) x y
rwa : ∀ (h : Membership.mem (γ := Subgroup α) ⊥ (x⁻¹ * y)), (id x)⁻¹ * id y = 1
⊢ (id x)⁻¹ * id y = 1
have rwa₁ : ∀ (h : x⁻¹ * y = 1), (id x)⁻¹ * id y = 1
Tactic: rwa [leftRel_apply, Subgroup.mem_bot] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
x : HasQuotient.Quotient α (B := Subgroup α) ⊥
⊢ (↑(Quotient.lift id ⋯ x) : α ⧸ ⊥) = x
have h : ∀ (a : α), Eq (α := HasQuotient.Quotient α (B := Subgroup α) ⊥) (↑(Quotient.lift (s := leftRel ⊥) id sorry ⟦a⟧) : α ⧸ ⊥) ⟦a⟧
Tactic: induction x using Quotient.inductionOn
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Card (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
⊢ Nat.card α = Nat.card.{u_1} (α ⧸ s) * Nat.card.{u_1} ↥s
have rw : Nat.card α = Nat.card.{u_1} ((α ⧸ s) × ↥s)
Tactic: rw [← Nat.card_prod]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Card (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
t : Set α
⊢ Nat.card.{u_1} (↑(t * (↑s : Set α)) : Type u_1) =
    Nat.card.{u_1} ↥s * Nat.card.{u_1} (↑(QuotientGroup.mk '' t) : Type u_1)
have rw : (↑(t * (↑s : Set α)) : Type u_1) ≃ ↥s × (↑(QuotientGroup.mk '' t) : Type u_1)
Tactic: rw [← Nat.card_prod, Nat.card_congr]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Card (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
t : Set α
⊢ (↑(t * (↑s : Set α)) : Type u_1) ≃ ↥s × (↑(QuotientGroup.mk '' t) : Type u_1)
have apply : (↑(t * (↑s : Set α)) : Type u_1) ≃ (↑(Set.preimage (β := α ⧸ s) QuotientGroup.mk (QuotientGroup.mk '' t)) : Type u_1)
Tactic: apply Equiv.trans _ (QuotientGroup.preimageMkEquivSubgroupProdSet _ _)
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Card (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
t : Set α
⊢ (↑(t * (↑s : Set α)) : Type u_1) ≃ (↑(Set.preimage (β := α ⧸ s) QuotientGroup.mk (QuotientGroup.mk '' t)) : Type u_1)
have rw : (↑(t * (↑s : Set α)) : Type u_1) ≃ (↑(⋃ (x : ↥s), (fun (x_1 : α) ↦ x_1 * (↑x : α)) ⁻¹' t) : Type u_1)
Tactic: rw [QuotientGroup.preimage_image_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Card (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
t : Set α
⊢ (↑(t * (↑s : Set α)) : Type u_1) ≃ (↑(⋃ (x : ↥s), (fun (x_1 : α) ↦ x_1 * (↑x : α)) ⁻¹' t) : Type u_1)
have h : ⋃ (x : ↥s), (fun (x_1 : α) ↦ x_1 * (↑x : α)) ⁻¹' t = t * (↑s : Set α)
Tactic: convert! Equiv.refl ↑(t * s)
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Defs (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
⊢ ∀ (a b : α), (leftRel s : α → α → Prop) a b = (a⁻¹ * b ∈ s)
have simp : ∀ (a b : α), (leftRel s : α → α → Prop) a b ↔ a⁻¹ * b ∈ s
Tactic: simp only [eq_iff_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Defs (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
x y : α
⊢ Decidable ((leftRel s : α → α → Prop) x y)
have rw : Decidable ((fun (x y : α) ↦ x⁻¹ * y ∈ s) x y)
Tactic: rw [leftRel_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Defs (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
⊢ ∀ (a b : α), (rightRel s : α → α → Prop) a b = (b * a⁻¹ ∈ s)
have simp : ∀ (a b : α), (rightRel s : α → α → Prop) a b ↔ b * a⁻¹ ∈ s
Tactic: simp only [eq_iff_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Defs (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
x y : α
⊢ Decidable ((rightRel s : α → α → Prop) x y)
have rw : Decidable ((fun (x y : α) ↦ y * x⁻¹ ∈ s) x y)
Tactic: rw [rightRel_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Defs (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
a b : α
⊢ (rightRel s : α → α → Prop) a b → (leftRel s : α → α → Prop) ((fun (g : α) ↦ g⁻¹) a) ((fun (g : α) ↦ g⁻¹) b)
have rw : b * a⁻¹ ∈ s → HMul.hMul (α := α) ((fun (g : α) ↦ g⁻¹) a)⁻¹ ((fun (g : α) ↦ g⁻¹) b) ∈ s
Tactic: rw [leftRel_apply, rightRel_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Defs (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
a b : α
⊢ (leftRel s : α → α → Prop) a b → (rightRel s : α → α → Prop) ((fun (g : α) ↦ g⁻¹) a) ((fun (g : α) ↦ g⁻¹) b)
have rw : a⁻¹ * b ∈ s → HMul.hMul (α := α) ((fun (g : α) ↦ g⁻¹) b) ((fun (g : α) ↦ g⁻¹) a)⁻¹ ∈ s
Tactic: rw [leftRel_apply, rightRel_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Defs (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
g_1 : Quotient (rightRel s)
g : α
⊢ (rightRel s : α → α → Prop) ((fun (g : α) ↦ g⁻¹) ((fun (g : α) ↦ g⁻¹) g)) g
have simp : (rightRel s : α → α → Prop) g g
Tactic: simp only [inv_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Defs (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
g_1 : α ⧸ s
g : α
⊢ (leftRel s : α → α → Prop) ((fun (g : α) ↦ g⁻¹) ((fun (g : α) ↦ g⁻¹) g)) g
have simp : (leftRel s : α → α → Prop) g g
Tactic: simp only [inv_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Defs (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
a b : α
⊢ (leftRel s : α → α → Prop) a b ↔ a⁻¹ * b ∈ s
have rw : a⁻¹ * b ∈ s ↔ a⁻¹ * b ∈ s
Tactic: rw [leftRel_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Defs (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
g : α
⊢ Quotient.out (s := leftRel s) (↑g : α ⧸ s) =
    g * (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) (g⁻¹ * Quotient.out (s := leftRel s) (↑g : α ⧸ s)) ⋯) : α)
have rw : Quotient.out (s := leftRel s) (↑g : α ⧸ s) = Quotient.out (s := leftRel s) (↑g : α ⧸ s)
Tactic: rw [mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Defs (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
b a : α
hb : b ∈ s
⊢ Eq (α := α ⧸ s) (↑(a * b) : α ⧸ s) (↑a : α ⧸ s)
have rwa : (a * b)⁻¹ * a ∈ s
Tactic: rwa [QuotientGroup.eq, mul_inv_rev, inv_mul_cancel_right, s.inv_mem_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Defs (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
b a : α
hb : b ∈ s
rwa : (a * b)⁻¹ * a ∈ s
⊢ Eq (α := α ⧸ s) (↑(a * b) : α ⧸ s) (↑a : α ⧸ s)
have rwa₁ : b⁻¹ * a⁻¹ * a ∈ s
Tactic: rwa [QuotientGroup.eq, mul_inv_rev, inv_mul_cancel_right, s.inv_mem_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Defs (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
b a : α
hb : b ∈ s
rwa : (a * b)⁻¹ * a ∈ s
rwa₁ : b⁻¹ * a⁻¹ * a ∈ s
⊢ Eq (α := α ⧸ s) (↑(a * b) : α ⧸ s) (↑a : α ⧸ s)
have rwa₂ : b⁻¹ ∈ s
Tactic: rwa [QuotientGroup.eq, mul_inv_rev, inv_mul_cancel_right, s.inv_mem_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Defs (goal)
Goal:
α : Type u_1
inst : Group α
N : Subgroup α
s : Set α
⊢ preimage (β := α ⧸ N) mk (mk '' s) = ⋃ (x : ↥N), (fun (x_1 : α) ↦ x_1 * (↑x : α)) ⁻¹' s
have h : ∀ (x : α),
  x ∈ preimage (β := α ⧸ N) mk (mk '' s) ↔
    Membership.mem (γ := Set α) (⋃ (x : ↥N), (fun (x_1 : α) ↦ x_1 * (↑x : α)) ⁻¹' s) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Defs (goal)
Goal:
α : Type u_1
inst : Group α
N : Subgroup α
s : Set α
x : α
⊢ x ∈ preimage (β := α ⧸ N) mk (mk '' s) ↔
    Membership.mem (γ := Set α) (⋃ (x : ↥N), (fun (x_1 : α) ↦ x_1 * (↑x : α)) ⁻¹' s) x
have h : (∃ x_1 ∈ s, x_1⁻¹ * x ∈ N) ↔ ∃ x_1 ∈ N, x * x_1 ∈ s
Tactic: simp only [QuotientGroup.eq, SetLike.exists, exists_prop, Set.mem_preimage, Set.mem_iUnion,
    Set.mem_image]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Defs (goal)
Goal:
α : Type u_1
inst : Group α
N : Subgroup α
s : Set α
⊢ preimage (β := α ⧸ N) mk (mk '' s) = ⋃ (x : ↥N), (fun (x_1 : α) ↦ x_1 * (↑x : α)) '' s
have rw : ∀ (x : ↥N), Eq (α := Set α) ((fun (x_1 : α) ↦ x_1 * (↑x⁻¹ : α)) '' s) ((fun (x_1 : α) ↦ x_1 * (↑x : α)) ⁻¹' s)
Tactic: rw [preimage_image_mk, iUnion_congr_of_surjective (·⁻¹) inv_surjective]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Defs (goal)
Goal:
α : Type u_1
inst : Group α
N : Subgroup α
s : Set α
⊢ preimage (β := α ⧸ N) mk (mk '' s) = s * (↑N : Set α)
have rw : Eq.{u_1 + 1} (α := Set α)
  (⋃ (x : α), ⋃ (hx : x ∈ N), (fun (x_1 : α) ↦ x_1 * (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ N) x hx) : α)) '' s)
  (⋃ b ∈ (↑N : Set α), (fun (x : α) ↦ x * b) '' s)
Tactic: rw [preimage_image_mk_eq_iUnion_image, iUnion_subtype, ← image2_mul, ← iUnion_image_right]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Defs (goal)
Goal:
α : Type u_1
inst : Group α
N : Subgroup α
⊢ preimage (β := α ⧸ N) mk {(↑1 : α ⧸ N)} = (↑N : Set α)
have rw : {1} * (↑N : Set α) = (↑N : Set α)
Tactic: rw [← image_singleton, preimage_image_mk_eq_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (goal)
Goal:
G : Type u_1
inst : Group G
D H : Subgroup G
inst_1 : D.FiniteIndex
hD_le_H : D ≤ H
⊢ ∃ (t : Finset ↥H),
    IsComplement (↑t : Set ↥H) (↑(D.subgroupOf H) : Set ↥H) ∧ ⋃ g ∈ t, (↑g : G) • (↑D : Set G) = (↑H : Set G)
have have : ∀ (t : Set ↥H) (ht : IsComplement t (↑(D.subgroupOf H) : Set ↥H) ∧ 1 ∈ t),
  ∃ (t : Finset ↥H),
    IsComplement (↑t : Set ↥H) (↑(D.subgroupOf H) : Set ↥H) ∧ ⋃ g ∈ t, (↑g : G) • (↑D : Set G) = (↑H : Set G)
Tactic: have ⟨t, ht⟩ := (D.subgroupOf H).exists_isComplement_left 1
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (hypothesis)
Goal:
G : Type u_1
inst : Group G
D H : Subgroup G
inst_1 : D.FiniteIndex
hD_le_H : D ≤ H
t : Set ↥H
ht : IsComplement t (↑(D.subgroupOf H) : Set ↥H) ∧ 1 ∈ t
⊢ ∃ (t : Finset ↥H),
    IsComplement (↑t : Set ↥H) (↑(D.subgroupOf H) : Set ↥H) ∧ ⋃ g ∈ t, (↑g : G) • (↑D : Set G) = (↑H : Set G)
have hf : t.Finite
Tactic: have hf : t.Finite := ht.1.finite_left_iff.mpr inferInstance
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (goal)
Goal:
G : Type u_1
inst : Group G
D H : Subgroup G
inst_1 : D.FiniteIndex
hD_le_H : D ≤ H
t : Set ↥H
ht : IsComplement t (↑(D.subgroupOf H) : Set ↥H) ∧ 1 ∈ t
hf : t.Finite
⊢ ∃ (t : Finset ↥H),
    IsComplement (↑t : Set ↥H) (↑(D.subgroupOf H) : Set ↥H) ∧ ⋃ g ∈ t, (↑g : G) • (↑D : Set G) = (↑H : Set G)
have refine : ⋃ g ∈ hf.toFinset (s := t), (↑g : G) • (↑D : Set G) = (↑H : Set G)
Tactic: refine ⟨hf.toFinset, hf.coe_toFinset.symm ▸ ht.1, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (goal)
Goal:
G : Type u_1
inst : Group G
D H : Subgroup G
inst_1 : D.FiniteIndex
hD_le_H : D ≤ H
t : Set ↥H
ht : IsComplement t (↑(D.subgroupOf H) : Set ↥H) ∧ 1 ∈ t
hf : t.Finite
⊢ ⋃ g ∈ hf.toFinset (s := t), (↑g : G) • (↑D : Set G) = (↑H : Set G)
have h : ∀ (x : G), Membership.mem (γ := Set G) (⋃ g ∈ hf.toFinset (s := t), (↑g : G) • (↑D : Set G)) x ↔ x ∈ (↑H : Set G)
Tactic: ext x
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (goal)
Goal:
G : Type u_1
inst : Group G
D H : Subgroup G
inst_1 : D.FiniteIndex
hD_le_H : D ≤ H
t : Set ↥H
ht : IsComplement t (↑(D.subgroupOf H) : Set ↥H) ∧ 1 ∈ t
hf : t.Finite
x : G
⊢ Membership.mem (γ := Set G) (⋃ g ∈ hf.toFinset (s := t), (↑g : G) • (↑D : Set G)) x ↔ x ∈ (↑H : Set G)
have h : (∃ y ∈ t, ∃ d ∈ D, (↑y : G) * d = x) ↔ x ∈ H
Tactic: suffices (∃ y ∈ t, ∃ d ∈ D, y * d = x) ↔ x ∈ H by simpa using this
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (goal)
Goal:
G : Type u_1
inst : Group G
D H : Subgroup G
inst_1 : D.FiniteIndex
hD_le_H : D ≤ H
t : Set ↥H
ht : IsComplement t (↑(D.subgroupOf H) : Set ↥H) ∧ 1 ∈ t
hf : t.Finite
x : G
⊢ (∃ y ∈ t, ∃ d ∈ D, (↑y : G) * d = x) ↔ x ∈ H
have h : (∃ y ∈ t, ∃ d ∈ D, (↑y : G) * d = x) → x ∈ H
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (goal)
Goal:
G : Type u_1
inst : Group G
D H : Subgroup G
inst_1 : D.FiniteIndex
hD_le_H : D ≤ H
t : Set ↥H
ht : IsComplement t (↑(D.subgroupOf H) : Set ↥H) ∧ 1 ∈ t
hf : t.Finite
x : G
h : (∃ y ∈ t, ∃ d ∈ D, (↑y : G) * d = x) → x ∈ H
⊢ (∃ y ∈ t, ∃ d ∈ D, (↑y : G) * d = x) ↔ x ∈ H
have h₁ : x ∈ H → ∃ y ∈ t, ∃ d ∈ D, (↑y : G) * d = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (hypothesis)
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
⊢ H.FiniteIndex
have hcovers₁ : Set.SurjOn.{u_2, u_1} (β := G ⧸ H) (fun (x : ι) ↦ (↑(g x) : G ⧸ H)) (↑s : Set ι) Set.univ
Tactic: simp_rw [leftCoset_cover_const_iff_surjOn] at hcovers
Cleared hypotheses: hcovers
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (hypothesis)
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : Set.SurjOn.{u_2, u_1} (β := G ⧸ H) (fun (x : ι) ↦ (↑(g x) : G ⧸ H)) (↑s : Set ι) Set.univ
⊢ H.FiniteIndex
have this : Finite.{u_1 + 1} (G ⧸ H)
Tactic: have := Set.finite_univ_iff.mp <| Set.Finite.of_surjOn _ hcovers s.finite_toSet
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (hypothesis)
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
h : H.index > 0
⊢ H.index ≤ s.card
have 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))
Tactic: rw [leftCoset_cover_const_iff_surjOn, Set.surjOn_iff_surjective] at hcovers
Cleared hypotheses: hcovers, h
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (hypothesis)
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
⊢ H.index ≤ s.card
have x : H.index = 0 ∨ H.index > 0
Tactic: cases H.index.eq_zero_or_pos with
  | inl h => exact h ▸ s.card.zero_le
  | inr h =>
    rw [leftCoset_cover_const_iff_surjOn, Set.surjOn_iff_surjective] at hcovers
    exact (Nat.card_le_card_of_surjective _ hcovers).trans_eq (Nat.card_eq_finsetCard _)
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (hypothesis)
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 : H.index = 0
⊢ False
have h₁ : s = ∅
Tactic: rw [hind, Finset.card_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (hypothesis)
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 = ∅
⊢ False
have hcovers₁ : Eq.{u_1 + 1} (α := Set G) ∅ Set.univ
Tactic: rw [h, ← Finset.set_biUnion_coe, Finset.coe_empty, Set.biUnion_empty] at hcovers
Cleared hypotheses: hcovers, hind, h
-- 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
⊢ Set.PairwiseDisjoint.{u_1, u_2} (α := Set G) (↑s : Set ι) fun (x : ι) ↦ g x • (↑H : Set G)
have have : ∀ (this : Fintype (G ⧸ H)), 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
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (hypothesis)
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) ⊥ x
have hi'₁ : Membership.mem (γ := Set G) ((fun (x : ι) ↦ g x • (↑H : Set G)) i) x
Tactic: specialize hi' hx
Cleared hypotheses: hi'
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (hypothesis)
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) ⊥ x
have hj'₁ : Membership.mem (γ := Set G) ((fun (x : ι) ↦ g x • (↑H : Set G)) j) x
Tactic: specialize hj' hx
Cleared hypotheses: hj'
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (hypothesis)
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
⊢ Membership.mem (γ := Set G) ⊥ x
have hi'₁ : Eq (α := G ⧸ H) (↑(g i) : G ⧸ H) (↑x : G ⧸ H)
Tactic: rw [mem_leftCoset_iff, SetLike.mem_coe, ← QuotientGroup.eq] at hi' hj'
Cleared hypotheses: hi', hj'
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (hypothesis)
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)
⊢ Membership.mem (γ := Set G) ⊥ x
have hj'₁ : Eq (α := G ⧸ H) (↑(g j) : G ⧸ H) (↑x : G ⧸ H)
Tactic: rw [mem_leftCoset_iff, SetLike.mem_coe, ← QuotientGroup.eq] at hi' hj'
Cleared hypotheses: hi', hj'
-- 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_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)
⊢ Membership.mem (γ := Set G) ⊥ x
have 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
Tactic: rw [ne_eq, ← Subtype.mk.injEq (p := (· ∈ (s : Set ι))) i hi j hj] at h'
Cleared hypotheses: h', c, x, hx, hi', hj'
-- 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)
⊢ Set.PairwiseDisjoint.{u_1, u_2} (α := Set G) (↑s : Set ι) fun (x : ι) ↦ g x • (↑H : Set G)
have suffices : Function.Bijective.{u_2 + 1, u_1 + 1} (β := G ⧸ H) fun (x : ↥s) ↦ (↑(g (↑x : ι)) : G ⧸ H)
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']
-- 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.Bijective.{u_2 + 1, u_1 + 1} (β := G ⧸ H) fun (x : ↥s) ↦ (↑(g (↑x : ι)) : G ⧸ H)
have 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)
Tactic: rw [Fintype.bijective_iff_surjective_and_card]
-- 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)) ∧
    Fintype.card.{u_2} ↥s = Fintype.card.{u_1} (G ⧸ H)
have left : Function.Surjective.{u_2 + 1, u_1 + 1} (β := G ⧸ H) fun (x : ↥s) ↦ (↑(g (↑x : ι)) : G ⧸ H)
Tactic: constructor