awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
ι : Type u_2
f : ι → Subgroup α
H : Subgroup α
simp_rw simp_rw₁ :
  ∀ (a₁ a₂ : ↥H),
    (Eq (α := (i : ι) → ↥H ⧸ (f i).subgroupOf H) (fun (i : ι) ↦ quotientSubgroupOfMapOfLE H ⋯ (Quotient.mk'' a₁))
        fun (i : ι) ↦ quotientSubgroupOfMapOfLE H ⋯ (Quotient.mk'' a₂)) →
      Eq (α := ↥H ⧸ subgroupOf (⨅ (i : ι), f i) H) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
simp_rw₂ :
  ∀ (a₁ a₂ : ↥H),
    (∀ (x : ι), quotientSubgroupOfMapOfLE H ⋯ (Quotient.mk'' a₁) = quotientSubgroupOfMapOfLE H ⋯ (Quotient.mk'' a₂)) →
      Eq (α := ↥H ⧸ subgroupOf (⨅ (i : ι), f i) H) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
simp_rw₃ :
  ∀ (a₁ a₂ : ↥H),
    (∀ (x : ι), Eq (α := ↥H ⧸ (f x).subgroupOf H) (↑a₁ : ↥H ⧸ (f x).subgroupOf H) (↑a₂ : ↥H ⧸ (f x).subgroupOf H)) →
      Eq (α := ↥H ⧸ subgroupOf (⨅ (i : ι), f i) H) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
simp_rw₄ : ∀ (a₁ a₂ : ↥H), (∀ (x : ι), a₁⁻¹ * a₂ ∈ (f x).subgroupOf H) → a₁⁻¹ * a₂ ∈ subgroupOf (⨅ (i : ι), f i) H
simp_rw₅ :
  ∀ (a₁ a₂ : ↥H),
    (∀ (x : ι), (↑(a₁⁻¹ * a₂) : α) ∈ f x) → Membership.mem (γ := Subgroup α) (⨅ (i : ι), f i) (↑(a₁⁻¹ * a₂) : α)
simp_rw₆ : ∀ (a₁ a₂ : ↥H), (∀ (x : ι), (↑(a₁⁻¹ * a₂) : α) ∈ f x) → ∀ (x : ι), (↑(a₁⁻¹ * a₂) : α) ∈ f x
⊢ ∀ (a₁ a₂ : ↥H),
    Eq (α := (i : ι) → ↥H ⧸ (f i).subgroupOf H)
        ((fun (q : ↥H ⧸ subgroupOf (⨅ (i : ι), f i) H) (i : ι) ↦ quotientSubgroupOfMapOfLE H ⋯ q) (Quotient.mk'' a₁))
        ((fun (q : ↥H ⧸ subgroupOf (⨅ (i : ι), f i) H) (i : ι) ↦ quotientSubgroupOfMapOfLE H ⋯ q) (Quotient.mk'' a₂)) →
      Eq (α := ↥H ⧸ subgroupOf (⨅ (i : ι), f i) H) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
have simp_rw₇ : ∀ (a₁ a₂ : ↥H), True
Tactic: simp_rw [funext_iff, quotientSubgroupOfMapOfLE_apply_mk, QuotientGroup.eq, mem_subgroupOf,
        mem_iInf, imp_self, forall_const]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
ι : Type u_2
f : ι → Subgroup α
simp_rw simp_rw₁ :
  ∀ (a₁ a₂ : α),
    (Eq (α := (i : ι) → α ⧸ f i) (fun (i : ι) ↦ quotientMapOfLE ⋯ (Quotient.mk'' a₁)) fun (i : ι) ↦
        quotientMapOfLE ⋯ (Quotient.mk'' a₂)) →
      Eq (α := HasQuotient.Quotient α (B := Subgroup α) (⨅ (i : ι), f i)) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
⊢ ∀ (a₁ a₂ : α),
    Eq (α := (i : ι) → α ⧸ f i)
        ((fun (q : HasQuotient.Quotient α (B := Subgroup α) (⨅ (i : ι), f i)) (i : ι) ↦ quotientMapOfLE ⋯ q)
          (Quotient.mk'' a₁))
        ((fun (q : HasQuotient.Quotient α (B := Subgroup α) (⨅ (i : ι), f i)) (i : ι) ↦ quotientMapOfLE ⋯ q)
          (Quotient.mk'' a₂)) →
      Eq (α := HasQuotient.Quotient α (B := Subgroup α) (⨅ (i : ι), f i)) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
have simp_rw₂ : ∀ (a₁ a₂ : α),
  (∀ (x : ι), quotientMapOfLE sorry (Quotient.mk'' a₁) = quotientMapOfLE sorry (Quotient.mk'' a₂)) →
    Eq (α := HasQuotient.Quotient α (B := Subgroup α) (⨅ (i : ι), f i)) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
Tactic: simp_rw [funext_iff, quotientMapOfLE_apply_mk, QuotientGroup.eq, mem_iInf, imp_self,
        forall_const]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
ι : Type u_2
f : ι → Subgroup α
simp_rw simp_rw₁ :
  ∀ (a₁ a₂ : α),
    (Eq (α := (i : ι) → α ⧸ f i) (fun (i : ι) ↦ quotientMapOfLE ⋯ (Quotient.mk'' a₁)) fun (i : ι) ↦
        quotientMapOfLE ⋯ (Quotient.mk'' a₂)) →
      Eq (α := HasQuotient.Quotient α (B := Subgroup α) (⨅ (i : ι), f i)) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
simp_rw₂ :
  ∀ (a₁ a₂ : α),
    (∀ (x : ι), quotientMapOfLE ⋯ (Quotient.mk'' a₁) = quotientMapOfLE ⋯ (Quotient.mk'' a₂)) →
      Eq (α := HasQuotient.Quotient α (B := Subgroup α) (⨅ (i : ι), f i)) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
⊢ ∀ (a₁ a₂ : α),
    Eq (α := (i : ι) → α ⧸ f i)
        ((fun (q : HasQuotient.Quotient α (B := Subgroup α) (⨅ (i : ι), f i)) (i : ι) ↦ quotientMapOfLE ⋯ q)
          (Quotient.mk'' a₁))
        ((fun (q : HasQuotient.Quotient α (B := Subgroup α) (⨅ (i : ι), f i)) (i : ι) ↦ quotientMapOfLE ⋯ q)
          (Quotient.mk'' a₂)) →
      Eq (α := HasQuotient.Quotient α (B := Subgroup α) (⨅ (i : ι), f i)) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
have simp_rw₃ : ∀ (a₁ a₂ : α),
  (∀ (x : ι), Eq (α := α ⧸ f x) (↑a₁ : α ⧸ f x) (↑a₂ : α ⧸ f x)) →
    Eq (α := HasQuotient.Quotient α (B := Subgroup α) (⨅ (i : ι), f i)) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
Tactic: simp_rw [funext_iff, quotientMapOfLE_apply_mk, QuotientGroup.eq, mem_iInf, imp_self,
        forall_const]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
ι : Type u_2
f : ι → Subgroup α
simp_rw simp_rw₁ :
  ∀ (a₁ a₂ : α),
    (Eq (α := (i : ι) → α ⧸ f i) (fun (i : ι) ↦ quotientMapOfLE ⋯ (Quotient.mk'' a₁)) fun (i : ι) ↦
        quotientMapOfLE ⋯ (Quotient.mk'' a₂)) →
      Eq (α := HasQuotient.Quotient α (B := Subgroup α) (⨅ (i : ι), f i)) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
simp_rw₂ :
  ∀ (a₁ a₂ : α),
    (∀ (x : ι), quotientMapOfLE ⋯ (Quotient.mk'' a₁) = quotientMapOfLE ⋯ (Quotient.mk'' a₂)) →
      Eq (α := HasQuotient.Quotient α (B := Subgroup α) (⨅ (i : ι), f i)) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
simp_rw₃ :
  ∀ (a₁ a₂ : α),
    (∀ (x : ι), Eq (α := α ⧸ f x) (↑a₁ : α ⧸ f x) (↑a₂ : α ⧸ f x)) →
      Eq (α := HasQuotient.Quotient α (B := Subgroup α) (⨅ (i : ι), f i)) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
⊢ ∀ (a₁ a₂ : α),
    Eq (α := (i : ι) → α ⧸ f i)
        ((fun (q : HasQuotient.Quotient α (B := Subgroup α) (⨅ (i : ι), f i)) (i : ι) ↦ quotientMapOfLE ⋯ q)
          (Quotient.mk'' a₁))
        ((fun (q : HasQuotient.Quotient α (B := Subgroup α) (⨅ (i : ι), f i)) (i : ι) ↦ quotientMapOfLE ⋯ q)
          (Quotient.mk'' a₂)) →
      Eq (α := HasQuotient.Quotient α (B := Subgroup α) (⨅ (i : ι), f i)) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
have simp_rw₄ : ∀ (a₁ a₂ : α), (∀ (x : ι), a₁⁻¹ * a₂ ∈ f x) → Membership.mem (γ := Subgroup α) (⨅ (i : ι), f i) (a₁⁻¹ * a₂)
Tactic: simp_rw [funext_iff, quotientMapOfLE_apply_mk, QuotientGroup.eq, mem_iInf, imp_self,
        forall_const]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
ι : Type u_2
f : ι → Subgroup α
simp_rw simp_rw₁ :
  ∀ (a₁ a₂ : α),
    (Eq (α := (i : ι) → α ⧸ f i) (fun (i : ι) ↦ quotientMapOfLE ⋯ (Quotient.mk'' a₁)) fun (i : ι) ↦
        quotientMapOfLE ⋯ (Quotient.mk'' a₂)) →
      Eq (α := HasQuotient.Quotient α (B := Subgroup α) (⨅ (i : ι), f i)) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
simp_rw₂ :
  ∀ (a₁ a₂ : α),
    (∀ (x : ι), quotientMapOfLE ⋯ (Quotient.mk'' a₁) = quotientMapOfLE ⋯ (Quotient.mk'' a₂)) →
      Eq (α := HasQuotient.Quotient α (B := Subgroup α) (⨅ (i : ι), f i)) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
simp_rw₃ :
  ∀ (a₁ a₂ : α),
    (∀ (x : ι), Eq (α := α ⧸ f x) (↑a₁ : α ⧸ f x) (↑a₂ : α ⧸ f x)) →
      Eq (α := HasQuotient.Quotient α (B := Subgroup α) (⨅ (i : ι), f i)) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
simp_rw₄ : ∀ (a₁ a₂ : α), (∀ (x : ι), a₁⁻¹ * a₂ ∈ f x) → Membership.mem (γ := Subgroup α) (⨅ (i : ι), f i) (a₁⁻¹ * a₂)
⊢ ∀ (a₁ a₂ : α),
    Eq (α := (i : ι) → α ⧸ f i)
        ((fun (q : HasQuotient.Quotient α (B := Subgroup α) (⨅ (i : ι), f i)) (i : ι) ↦ quotientMapOfLE ⋯ q)
          (Quotient.mk'' a₁))
        ((fun (q : HasQuotient.Quotient α (B := Subgroup α) (⨅ (i : ι), f i)) (i : ι) ↦ quotientMapOfLE ⋯ q)
          (Quotient.mk'' a₂)) →
      Eq (α := HasQuotient.Quotient α (B := Subgroup α) (⨅ (i : ι), f i)) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
have simp_rw₅ : ∀ (a₁ a₂ : α), (∀ (x : ι), a₁⁻¹ * a₂ ∈ f x) → ∀ (x : ι), a₁⁻¹ * a₂ ∈ f x
Tactic: simp_rw [funext_iff, quotientMapOfLE_apply_mk, QuotientGroup.eq, mem_iInf, imp_self,
        forall_const]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
ι : Type u_2
f : ι → Subgroup α
simp_rw simp_rw₁ :
  ∀ (a₁ a₂ : α),
    (Eq (α := (i : ι) → α ⧸ f i) (fun (i : ι) ↦ quotientMapOfLE ⋯ (Quotient.mk'' a₁)) fun (i : ι) ↦
        quotientMapOfLE ⋯ (Quotient.mk'' a₂)) →
      Eq (α := HasQuotient.Quotient α (B := Subgroup α) (⨅ (i : ι), f i)) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
simp_rw₂ :
  ∀ (a₁ a₂ : α),
    (∀ (x : ι), quotientMapOfLE ⋯ (Quotient.mk'' a₁) = quotientMapOfLE ⋯ (Quotient.mk'' a₂)) →
      Eq (α := HasQuotient.Quotient α (B := Subgroup α) (⨅ (i : ι), f i)) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
simp_rw₃ :
  ∀ (a₁ a₂ : α),
    (∀ (x : ι), Eq (α := α ⧸ f x) (↑a₁ : α ⧸ f x) (↑a₂ : α ⧸ f x)) →
      Eq (α := HasQuotient.Quotient α (B := Subgroup α) (⨅ (i : ι), f i)) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
simp_rw₄ : ∀ (a₁ a₂ : α), (∀ (x : ι), a₁⁻¹ * a₂ ∈ f x) → Membership.mem (γ := Subgroup α) (⨅ (i : ι), f i) (a₁⁻¹ * a₂)
simp_rw₅ : ∀ (a₁ a₂ : α), (∀ (x : ι), a₁⁻¹ * a₂ ∈ f x) → ∀ (x : ι), a₁⁻¹ * a₂ ∈ f x
⊢ ∀ (a₁ a₂ : α),
    Eq (α := (i : ι) → α ⧸ f i)
        ((fun (q : HasQuotient.Quotient α (B := Subgroup α) (⨅ (i : ι), f i)) (i : ι) ↦ quotientMapOfLE ⋯ q)
          (Quotient.mk'' a₁))
        ((fun (q : HasQuotient.Quotient α (B := Subgroup α) (⨅ (i : ι), f i)) (i : ι) ↦ quotientMapOfLE ⋯ q)
          (Quotient.mk'' a₂)) →
      Eq (α := HasQuotient.Quotient α (B := Subgroup α) (⨅ (i : ι), f i)) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
have simp_rw₆ : ∀ (a₁ a₂ : α), True
Tactic: simp_rw [funext_iff, quotientMapOfLE_apply_mk, QuotientGroup.eq, mem_iInf, imp_self,
        forall_const]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
H : Type u_2
inst_1 : Group H
f : α →* H
a x : α
⊢ Membership.mem (γ := Set α) (preimage (β := H) (⇑f : (a : α) → H) (singleton (α := H) ((f : (a : α) → H) a : H))) x ↔
    x ∈ a • (↑f.ker : Set α)
have rw : Membership.mem (α := H) (γ := Set H) (singleton (α := H) ((f : (a : α) → H) a : H)) ((f : (a : α) → H) x : H) ↔
  x ∈ a • (↑f.ker : Set α)
Tactic: rw [mem_preimage, mem_singleton_iff, mem_smul_set_iff_inv_smul_mem, SetLike.mem_coe, mem_ker,
        smul_eq_mul, map_mul, map_inv, inv_mul_eq_one, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
H : Type u_2
inst_1 : Group H
f : α →* H
a x : α
rw :
  Membership.mem (α := H) (γ := Set H) (singleton (α := H) ((f : (a : α) → H) a : H)) ((f : (a : α) → H) x : H) ↔
    x ∈ a • (↑f.ker : Set α)
⊢ Membership.mem (γ := Set α) (preimage (β := H) (⇑f : (a : α) → H) (singleton (α := H) ((f : (a : α) → H) a : H))) x ↔
    x ∈ a • (↑f.ker : Set α)
have rw₁ : Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔ x ∈ a • (↑f.ker : Set α)
Tactic: rw [mem_preimage, mem_singleton_iff, mem_smul_set_iff_inv_smul_mem, SetLike.mem_coe, mem_ker,
        smul_eq_mul, map_mul, map_inv, inv_mul_eq_one, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
H : Type u_2
inst_1 : Group H
f : α →* H
a x : α
rw :
  Membership.mem (α := H) (γ := Set H) (singleton (α := H) ((f : (a : α) → H) a : H)) ((f : (a : α) → H) x : H) ↔
    x ∈ a • (↑f.ker : Set α)
rw₁ : Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔ x ∈ a • (↑f.ker : Set α)
⊢ Membership.mem (γ := Set α) (preimage (β := H) (⇑f : (a : α) → H) (singleton (α := H) ((f : (a : α) → H) a : H))) x ↔
    x ∈ a • (↑f.ker : Set α)
have rw₂ : Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔ a⁻¹ • x ∈ (↑f.ker : Set α)
Tactic: rw [mem_preimage, mem_singleton_iff, mem_smul_set_iff_inv_smul_mem, SetLike.mem_coe, mem_ker,
        smul_eq_mul, map_mul, map_inv, inv_mul_eq_one, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
H : Type u_2
inst_1 : Group H
f : α →* H
a x : α
rw :
  Membership.mem (α := H) (γ := Set H) (singleton (α := H) ((f : (a : α) → H) a : H)) ((f : (a : α) → H) x : H) ↔
    x ∈ a • (↑f.ker : Set α)
rw₁ : Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔ x ∈ a • (↑f.ker : Set α)
rw₂ : Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔ a⁻¹ • x ∈ (↑f.ker : Set α)
⊢ Membership.mem (γ := Set α) (preimage (β := H) (⇑f : (a : α) → H) (singleton (α := H) ((f : (a : α) → H) a : H))) x ↔
    x ∈ a • (↑f.ker : Set α)
have rw₃ : Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔ a⁻¹ • x ∈ f.ker
Tactic: rw [mem_preimage, mem_singleton_iff, mem_smul_set_iff_inv_smul_mem, SetLike.mem_coe, mem_ker,
        smul_eq_mul, map_mul, map_inv, inv_mul_eq_one, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
H : Type u_2
inst_1 : Group H
f : α →* H
a x : α
rw :
  Membership.mem (α := H) (γ := Set H) (singleton (α := H) ((f : (a : α) → H) a : H)) ((f : (a : α) → H) x : H) ↔
    x ∈ a • (↑f.ker : Set α)
rw₁ : Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔ x ∈ a • (↑f.ker : Set α)
rw₂ : Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔ a⁻¹ • x ∈ (↑f.ker : Set α)
rw₃ : Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔ a⁻¹ • x ∈ f.ker
⊢ Membership.mem (γ := Set α) (preimage (β := H) (⇑f : (a : α) → H) (singleton (α := H) ((f : (a : α) → H) a : H))) x ↔
    x ∈ a • (↑f.ker : Set α)
have rw₄ : Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔
  Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) (a⁻¹ • x) : H) (1 : H)
Tactic: rw [mem_preimage, mem_singleton_iff, mem_smul_set_iff_inv_smul_mem, SetLike.mem_coe, mem_ker,
        smul_eq_mul, map_mul, map_inv, inv_mul_eq_one, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
H : Type u_2
inst_1 : Group H
f : α →* H
a x : α
rw :
  Membership.mem (α := H) (γ := Set H) (singleton (α := H) ((f : (a : α) → H) a : H)) ((f : (a : α) → H) x : H) ↔
    x ∈ a • (↑f.ker : Set α)
rw₁ : Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔ x ∈ a • (↑f.ker : Set α)
rw₂ : Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔ a⁻¹ • x ∈ (↑f.ker : Set α)
rw₃ : Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔ a⁻¹ • x ∈ f.ker
rw₄ :
  Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔
    Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) (a⁻¹ • x) : H) (1 : H)
⊢ Membership.mem (γ := Set α) (preimage (β := H) (⇑f : (a : α) → H) (singleton (α := H) ((f : (a : α) → H) a : H))) x ↔
    x ∈ a • (↑f.ker : Set α)
have rw₅ : Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔
  Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) (a⁻¹ * x) : H) (1 : H)
Tactic: rw [mem_preimage, mem_singleton_iff, mem_smul_set_iff_inv_smul_mem, SetLike.mem_coe, mem_ker,
        smul_eq_mul, map_mul, map_inv, inv_mul_eq_one, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
H : Type u_2
inst_1 : Group H
f : α →* H
a x : α
rw :
  Membership.mem (α := H) (γ := Set H) (singleton (α := H) ((f : (a : α) → H) a : H)) ((f : (a : α) → H) x : H) ↔
    x ∈ a • (↑f.ker : Set α)
rw₁ : Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔ x ∈ a • (↑f.ker : Set α)
rw₂ : Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔ a⁻¹ • x ∈ (↑f.ker : Set α)
rw₃ : Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔ a⁻¹ • x ∈ f.ker
rw₄ :
  Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔
    Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) (a⁻¹ • x) : H) (1 : H)
rw₅ :
  Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔
    Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) (a⁻¹ * x) : H) (1 : H)
⊢ Membership.mem (γ := Set α) (preimage (β := H) (⇑f : (a : α) → H) (singleton (α := H) ((f : (a : α) → H) a : H))) x ↔
    x ∈ a • (↑f.ker : Set α)
have rw₆ : Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔
  HMul.hMul (α := H) (β := H) ((f : (a : α) → H) a⁻¹ : H) ((f : (a : α) → H) x : H) = 1
Tactic: rw [mem_preimage, mem_singleton_iff, mem_smul_set_iff_inv_smul_mem, SetLike.mem_coe, mem_ker,
        smul_eq_mul, map_mul, map_inv, inv_mul_eq_one, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
H : Type u_2
inst_1 : Group H
f : α →* H
a x : α
rw :
  Membership.mem (α := H) (γ := Set H) (singleton (α := H) ((f : (a : α) → H) a : H)) ((f : (a : α) → H) x : H) ↔
    x ∈ a • (↑f.ker : Set α)
rw₁ : Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔ x ∈ a • (↑f.ker : Set α)
rw₂ : Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔ a⁻¹ • x ∈ (↑f.ker : Set α)
rw₃ : Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔ a⁻¹ • x ∈ f.ker
rw₄ :
  Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔
    Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) (a⁻¹ • x) : H) (1 : H)
rw₅ :
  Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔
    Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) (a⁻¹ * x) : H) (1 : H)
rw₆ :
  Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔
    HMul.hMul (α := H) (β := H) ((f : (a : α) → H) a⁻¹ : H) ((f : (a : α) → H) x : H) = 1
⊢ Membership.mem (γ := Set α) (preimage (β := H) (⇑f : (a : α) → H) (singleton (α := H) ((f : (a : α) → H) a : H))) x ↔
    x ∈ a • (↑f.ker : Set α)
have rw₇ : Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔
  HMul.hMul (α := H) (β := H) (((f : (a : α) → H) a)⁻¹ : H) ((f : (a : α) → H) x : H) = 1
Tactic: rw [mem_preimage, mem_singleton_iff, mem_smul_set_iff_inv_smul_mem, SetLike.mem_coe, mem_ker,
        smul_eq_mul, map_mul, map_inv, inv_mul_eq_one, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
H : Type u_2
inst_1 : Group H
f : α →* H
a x : α
rw :
  Membership.mem (α := H) (γ := Set H) (singleton (α := H) ((f : (a : α) → H) a : H)) ((f : (a : α) → H) x : H) ↔
    x ∈ a • (↑f.ker : Set α)
rw₁ : Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔ x ∈ a • (↑f.ker : Set α)
rw₂ : Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔ a⁻¹ • x ∈ (↑f.ker : Set α)
rw₃ : Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔ a⁻¹ • x ∈ f.ker
rw₄ :
  Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔
    Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) (a⁻¹ • x) : H) (1 : H)
rw₅ :
  Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔
    Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) (a⁻¹ * x) : H) (1 : H)
rw₆ :
  Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔
    HMul.hMul (α := H) (β := H) ((f : (a : α) → H) a⁻¹ : H) ((f : (a : α) → H) x : H) = 1
rw₇ :
  Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔
    HMul.hMul (α := H) (β := H) (((f : (a : α) → H) a)⁻¹ : H) ((f : (a : α) → H) x : H) = 1
⊢ Membership.mem (γ := Set α) (preimage (β := H) (⇑f : (a : α) → H) (singleton (α := H) ((f : (a : α) → H) a : H))) x ↔
    x ∈ a • (↑f.ker : Set α)
have rw₈ : Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔
  Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) a : H) ((f : (a : α) → H) x : H)
Tactic: rw [mem_preimage, mem_singleton_iff, mem_smul_set_iff_inv_smul_mem, SetLike.mem_coe, mem_ker,
        smul_eq_mul, map_mul, map_inv, inv_mul_eq_one, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
H : Type u_2
inst_1 : Group H
f : α →* H
a x : α
rw :
  Membership.mem (α := H) (γ := Set H) (singleton (α := H) ((f : (a : α) → H) a : H)) ((f : (a : α) → H) x : H) ↔
    x ∈ a • (↑f.ker : Set α)
rw₁ : Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔ x ∈ a • (↑f.ker : Set α)
rw₂ : Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔ a⁻¹ • x ∈ (↑f.ker : Set α)
rw₃ : Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔ a⁻¹ • x ∈ f.ker
rw₄ :
  Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔
    Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) (a⁻¹ • x) : H) (1 : H)
rw₅ :
  Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔
    Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) (a⁻¹ * x) : H) (1 : H)
rw₆ :
  Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔
    HMul.hMul (α := H) (β := H) ((f : (a : α) → H) a⁻¹ : H) ((f : (a : α) → H) x : H) = 1
rw₇ :
  Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔
    HMul.hMul (α := H) (β := H) (((f : (a : α) → H) a)⁻¹ : H) ((f : (a : α) → H) x : H) = 1
rw₈ :
  Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔
    Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) a : H) ((f : (a : α) → H) x : H)
⊢ Membership.mem (γ := Set α) (preimage (β := H) (⇑f : (a : α) → H) (singleton (α := H) ((f : (a : α) → H) a : H))) x ↔
    x ∈ a • (↑f.ker : Set α)
have rw₉ : Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) a : H) ((f : (a : α) → H) x : H) ↔
  Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) a : H) ((f : (a : α) → H) x : H)
Tactic: rw [mem_preimage, mem_singleton_iff, mem_smul_set_iff_inv_smul_mem, SetLike.mem_coe, mem_ker,
        smul_eq_mul, map_mul, map_inv, inv_mul_eq_one, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
t : Set (α ⧸ s)
a : ↥s × (↑t : Type u_1)
⊢ (↑(Quotient.out (↑a.2 : α ⧸ s) * (↑a.1 : α)) : α ⧸ s) ∈ t
have rw : (↑a.2 : α ⧸ s) ∈ t
Tactic: rw [mk_mul_of_mem _ a.1.2, out_eq']
-- 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
⊢ (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 fst : (↑((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))).1 :
    α) =
  (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha, Subtype.mk (p := fun (x : α ⧸ s) ↦ x ∈ t) x hx).1 : α)
Tactic: ext