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 α
x y : α
h : x⁻¹ * y ∈ s
z : α
⊢ x⁻¹ * y * y⁻¹ * z ∈ s ↔ y⁻¹ * z ∈ s
have mpr : x⁻¹ * y * (y⁻¹ * z) ∈ s ↔ y⁻¹ * z ∈ s
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x y : α
⊢ op x • (↑s : Set α) = op y • (↑s : Set α) ↔ y * x⁻¹ ∈ s
have rw : (∀ (x_1 : α), x_1 ∈ op x • (↑s : Set α) ↔ x_1 ∈ op y • (↑s : Set α)) ↔ y * x⁻¹ ∈ s
Tactic: rw [Set.ext_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x y : α
⊢ (∀ (x_1 : α), x_1 ∈ op x • (↑s : Set α) ↔ x_1 ∈ op y • (↑s : Set α)) ↔ y * x⁻¹ ∈ s
have simp_rw : (∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s) ↔ y * x⁻¹ ∈ s
Tactic: simp_rw [mem_rightCoset_iff, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x y : α
⊢ (∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s) ↔ y * x⁻¹ ∈ s
have mp : (∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s) → y * x⁻¹ ∈ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x y : α
mp : (∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s) → y * x⁻¹ ∈ s
⊢ (∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s) ↔ y * x⁻¹ ∈ s
have mpr : y * x⁻¹ ∈ s → ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x y : α
h : ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s
⊢ y * x⁻¹ ∈ s
have mp : y * y⁻¹ ∈ s
Tactic: apply (h y).mpr
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x y : α
h : ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s
⊢ y * y⁻¹ ∈ s
have mp : 1 ∈ s
Tactic: rw [mul_inv_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x y : α
h : y * x⁻¹ ∈ s
z : α
⊢ z * x⁻¹ ∈ s ↔ z * y⁻¹ ∈ s
have mpr : z * (y⁻¹ * (y * x⁻¹)) ∈ s ↔ z * y⁻¹ ∈ s
Tactic: rw [← inv_mul_cancel_left y x⁻¹]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x y : α
h : y * x⁻¹ ∈ s
z : α
⊢ z * (y⁻¹ * (y * x⁻¹)) ∈ s ↔ z * y⁻¹ ∈ s
have mpr : z * y⁻¹ * (y * x⁻¹) ∈ s ↔ z * y⁻¹ ∈ s
Tactic: rw [← mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
⊢ (⇑(leftRel s) : α → α → Prop) = LeftCosetEquivalence (↑s : Set α)
have h : ∀ (x x_1 : α), (leftRel s : α → α → Prop) x x_1 ↔ LeftCosetEquivalence (↑s : Set α) x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x x_1 : α
⊢ (leftRel s : α → α → Prop) x x_1 ↔ LeftCosetEquivalence (↑s : Set α) x x_1
have h : (fun (x y : α) ↦ x⁻¹ * y ∈ s) x x_1 ↔ LeftCosetEquivalence (↑s : Set α) x x_1
Tactic: rw [leftRel_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
β : Type u_2
inst_1 : Group β
s' : Subgroup β
⊢ leftRel (s.prod s') = (leftRel s).prod (leftRel s')
have refine : ∀ (x y : α × β),
  (leftRel (s.prod s') : α × β → α × β → Prop) x y ↔ ((leftRel s).prod (leftRel s') : α × β → α × β → Prop) x y
Tactic: refine Setoid.ext fun x y ↦ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
β : Type u_2
inst_1 : Group β
s' : Subgroup β
x y : α × β
⊢ (leftRel (s.prod s') : α × β → α × β → Prop) x y ↔
    (leftRel s : α → α → Prop) x.1 y.1 ∧ (leftRel s' : β → β → Prop) x.2 y.2
have simp_rw : x⁻¹ * y ∈ s.prod s' ↔ x.1⁻¹ * y.1 ∈ s ∧ x.2⁻¹ * y.2 ∈ s'
Tactic: simp_rw [leftRel_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
ι : Type u_2
β : ι → Type u_3
inst : (i : ι) → Group (β i)
s' : (i : ι) → Subgroup (β i)
⊢ leftRel (Subgroup.pi (f := β) univ s') = piSetoid (α := β)
have refine : ∀ (x y : (i : ι) → β i),
  (leftRel (Subgroup.pi univ s') : ((i : ι) → β i) → ((i : ι) → β i) → Prop) x y ↔
    (piSetoid : ((i : ι) → β i) → ((i : ι) → β i) → Prop) x y
Tactic: refine Setoid.ext fun x y ↦ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
⊢ (⇑(rightRel s) : α → α → Prop) = RightCosetEquivalence (↑s : Set α)
have h : ∀ (x x_1 : α), (rightRel s : α → α → Prop) x x_1 ↔ RightCosetEquivalence (↑s : Set α) x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x x_1 : α
⊢ (rightRel s : α → α → Prop) x x_1 ↔ RightCosetEquivalence (↑s : Set α) x x_1
have h : (fun (x y : α) ↦ y * x⁻¹ ∈ s) x x_1 ↔ RightCosetEquivalence (↑s : Set α) x x_1
Tactic: rw [rightRel_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
β : Type u_2
inst_1 : Group β
s' : Subgroup β
⊢ rightRel (s.prod s') = (rightRel s).prod (rightRel s')
have refine : ∀ (x y : α × β),
  (rightRel (s.prod s') : α × β → α × β → Prop) x y ↔ ((rightRel s).prod (rightRel s') : α × β → α × β → Prop) x y
Tactic: refine Setoid.ext fun x y ↦ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
β : Type u_2
inst_1 : Group β
s' : Subgroup β
x y : α × β
⊢ (rightRel (s.prod s') : α × β → α × β → Prop) x y ↔
    (rightRel s : α → α → Prop) x.1 y.1 ∧ (rightRel s' : β → β → Prop) x.2 y.2
have simp_rw : y * x⁻¹ ∈ s.prod s' ↔ y.1 * x.1⁻¹ ∈ s ∧ y.2 * x.2⁻¹ ∈ s'
Tactic: simp_rw [rightRel_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
ι : Type u_2
β : ι → Type u_3
inst : (i : ι) → Group (β i)
s' : (i : ι) → Subgroup (β i)
⊢ rightRel (Subgroup.pi (f := β) univ s') = piSetoid (α := β)
have refine : ∀ (x y : (i : ι) → β i),
  (rightRel (Subgroup.pi univ s') : ((i : ι) → β i) → ((i : ι) → β i) → Prop) x y ↔
    (piSetoid : ((i : ι) → β i) → ((i : ι) → β i) → Prop) x y
Tactic: refine Setoid.ext fun x y ↦ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
⊢ StrictMono (β := Subgroup ↥s × Set (α ⧸ s)) fun (t : Subgroup α) ↦ (Subgroup.comap s.subtype t, mk '' (↑t : Set α))
have refine : ∀ (t₁ t₂ : Subgroup α) (h : t₁ < t₂),
  LE.le.{u_1} (α := Subgroup ↥s × Set (α ⧸ s))
      ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s))) t₂)
      ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s))) t₁) →
    ∀ (a : α) (ha : a ∈ (↑t₂ : Set α))
      (le1 :
        LE.le.{u_1} (α := Subgroup ↥s)
          ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s))) t₂).1
          ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s)))
              t₁).1)
      (le2 :
        LE.le.{u_1} (α := Set (α ⧸ s))
          ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s))) t₂).2
          ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s)))
              t₁).2),
      a ∈ (↑t₁ : Set α)
Tactic: refine fun t₁ t₂ h ↦ ⟨⟨Subgroup.comap_mono h.1, Set.image_mono h.1⟩,
    mt (fun ⟨le1, le2⟩ a ha ↦ ?_) h.2⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s t₁ t₂ : Subgroup α
h : t₁ < t₂
h_1 :
  LE.le.{u_1} (α := Subgroup ↥s × Set (α ⧸ s))
    ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s))) t₂)
    ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s))) t₁)
a : α
ha : a ∈ (↑t₂ : Set α)
le1 :
  LE.le.{u_1} (α := Subgroup ↥s)
    ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s))) t₂).1
    ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s))) t₁).1
le2 :
  LE.le.{u_1} (α := Set (α ⧸ s))
    ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s))) t₂).2
    ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s))) t₁).2
⊢ a ∈ (↑t₁ : Set α)
have obtain : ∀ (a' : α) (h' : a' ∈ (↑t₁ : Set α)) (eq : Eq (α := α ⧸ s) (↑a' : α ⧸ s) (↑a : α ⧸ s)), a ∈ (↑t₁ : Set α)
Tactic: obtain ⟨a', h', eq⟩ := le2 ⟨_, ha, rfl⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s t₁ t₂ : Subgroup α
h : t₁ < t₂
h_1 :
  LE.le.{u_1} (α := Subgroup ↥s × Set (α ⧸ s))
    ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s))) t₂)
    ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s))) t₁)
a : α
ha : a ∈ (↑t₂ : Set α)
le1 :
  LE.le.{u_1} (α := Subgroup ↥s)
    ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s))) t₂).1
    ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s))) t₁).1
le2 :
  LE.le.{u_1} (α := Set (α ⧸ s))
    ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s))) t₂).2
    ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s))) t₁).2
a' : α
h' : a' ∈ (↑t₁ : Set α)
eq : Eq (α := α ⧸ s) (↑a' : α ⧸ s) (↑a : α ⧸ s)
⊢ a ∈ (↑t₁ : Set α)
have h₁ : HMul.hMul (β := α) a' ((s.subtype : (a : ↥s) → α) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (a'⁻¹ * a) sorry) : α) = a
Tactic: convert! ← t₁.mul_mem h' (@le1 ⟨_, QuotientGroup.eq.1 eq⟩ <| t₂.mul_mem (t₂.inv_mem <| h.1 h') ha)
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
g z : α
⊢ Membership.mem (γ := Set α) {x : α | Eq (α := α ⧸ s) (↑x : α ⧸ s) (↑g : α ⧸ s)} z ↔ z ∈ g • (↑s : Set α)
have rw : Membership.mem (γ := Set α) {x : α | Eq (α := α ⧸ s) (↑x : α ⧸ s) (↑g : α ⧸ s)} z ↔ g⁻¹ * z ∈ (↑s : Set α)
Tactic: rw [mem_leftCoset_iff, Set.mem_setOf_eq, eq_comm, QuotientGroup.eq, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
g z : α
rw : Membership.mem (γ := Set α) {x : α | Eq (α := α ⧸ s) (↑x : α ⧸ s) (↑g : α ⧸ s)} z ↔ g⁻¹ * z ∈ (↑s : Set α)
⊢ Membership.mem (γ := Set α) {x : α | Eq (α := α ⧸ s) (↑x : α ⧸ s) (↑g : α ⧸ s)} z ↔ z ∈ g • (↑s : Set α)
have rw₁ : Eq (α := α ⧸ s) (↑z : α ⧸ s) (↑g : α ⧸ s) ↔ g⁻¹ * z ∈ (↑s : Set α)
Tactic: rw [mem_leftCoset_iff, Set.mem_setOf_eq, eq_comm, QuotientGroup.eq, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
g z : α
rw : Membership.mem (γ := Set α) {x : α | Eq (α := α ⧸ s) (↑x : α ⧸ s) (↑g : α ⧸ s)} z ↔ g⁻¹ * z ∈ (↑s : Set α)
rw₁ : Eq (α := α ⧸ s) (↑z : α ⧸ s) (↑g : α ⧸ s) ↔ g⁻¹ * z ∈ (↑s : Set α)
⊢ Membership.mem (γ := Set α) {x : α | Eq (α := α ⧸ s) (↑x : α ⧸ s) (↑g : α ⧸ s)} z ↔ z ∈ g • (↑s : Set α)
have rw₂ : Eq (α := α ⧸ s) (↑g : α ⧸ s) (↑z : α ⧸ s) ↔ g⁻¹ * z ∈ (↑s : Set α)
Tactic: rw [mem_leftCoset_iff, Set.mem_setOf_eq, eq_comm, QuotientGroup.eq, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
g z : α
rw : Membership.mem (γ := Set α) {x : α | Eq (α := α ⧸ s) (↑x : α ⧸ s) (↑g : α ⧸ s)} z ↔ g⁻¹ * z ∈ (↑s : Set α)
rw₁ : Eq (α := α ⧸ s) (↑z : α ⧸ s) (↑g : α ⧸ s) ↔ g⁻¹ * z ∈ (↑s : Set α)
rw₂ : Eq (α := α ⧸ s) (↑g : α ⧸ s) (↑z : α ⧸ s) ↔ g⁻¹ * z ∈ (↑s : Set α)
⊢ Membership.mem (γ := Set α) {x : α | Eq (α := α ⧸ s) (↑x : α ⧸ s) (↑g : α ⧸ s)} z ↔ z ∈ g • (↑s : Set α)
have rw₃ : g⁻¹ * z ∈ s ↔ g⁻¹ * z ∈ (↑s : Set α)
Tactic: rw [mem_leftCoset_iff, Set.mem_setOf_eq, eq_comm, QuotientGroup.eq, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
g z : α
rw : Membership.mem (γ := Set α) {x : α | Eq (α := α ⧸ s) (↑x : α ⧸ s) (↑g : α ⧸ s)} z ↔ g⁻¹ * z ∈ (↑s : Set α)
rw₁ : Eq (α := α ⧸ s) (↑z : α ⧸ s) (↑g : α ⧸ s) ↔ g⁻¹ * z ∈ (↑s : Set α)
rw₂ : Eq (α := α ⧸ s) (↑g : α ⧸ s) (↑z : α ⧸ s) ↔ g⁻¹ * z ∈ (↑s : Set α)
rw₃ : g⁻¹ * z ∈ s ↔ g⁻¹ * z ∈ (↑s : Set α)
⊢ Membership.mem (γ := Set α) {x : α | Eq (α := α ⧸ s) (↑x : α ⧸ s) (↑g : α ⧸ s)} z ↔ z ∈ g • (↑s : Set α)
have rw₄ : g⁻¹ * z ∈ s ↔ g⁻¹ * z ∈ s
Tactic: rw [mem_leftCoset_iff, Set.mem_setOf_eq, eq_comm, QuotientGroup.eq, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x : α
⊢ orbitRel.Quotient.orbit (G := ↥s.op) (↑x : α ⧸ s) = x • (↑s : Set α)
have h : ∀ (x_1 : α), x_1 ∈ orbitRel.Quotient.orbit (G := ↥s.op) (↑x : α ⧸ s) ↔ x_1 ∈ x • (↑s : Set α)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x x_1 : α
⊢ x_1 ∈ orbitRel.Quotient.orbit (G := ↥s.op) (↑x : α ⧸ s) ↔ x_1 ∈ x • (↑s : Set α)
have h : Eq (α := Quotient (orbitRel (↥s.op) α)) (Quotient.mk'' x_1) (↑x : α ⧸ s) ↔ x_1 ∈ x • (↑s : Set α)
Tactic: rw [orbitRel.Quotient.mem_orbit]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x : α ⧸ s
⊢ MulAction.orbitRel.Quotient.orbit x = Quotient.out x • (↑s : Set α)
have H : ∀ (z : α),
  MulAction.orbitRel.Quotient.orbit (G := ↥s.op) (↑z : α ⧸ s) =
    Quotient.out (s := leftRel s) (↑z : α ⧸ s) • (↑s : Set α)
Tactic: induction x using QuotientGroup.induction_on
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
L : α ⧸ s
⊢ { x : α // (↑x : α ⧸ s) = L } ≃ (↑(Quotient.out L • (↑s : Set α)) : Type u_1)
have rw : { x : α // (↑x : α ⧸ s) = L } ≃ (↑{x : α | Eq (α := α ⧸ s) (↑x : α ⧸ s) (↑(Quotient.out L) : α ⧸ s)} : Type u_1)
Tactic: rw [← eq_class_eq_leftCoset]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
L : α ⧸ s
⊢ { x : α // Quotient.mk'' x = L } ≃
    { x : α // Eq (α := Quotient (leftRel s)) (Quotient.mk'' x) (Quotient.mk'' (Quotient.out L)) }
have simp : { x : α // Quotient.mk'' x = L } ≃ { x : α // Quotient.mk'' x = L }
Tactic: simp
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α ⧸ s
b c : α
h : (leftRel s : α → α → Prop) b c
⊢ (leftRel (s.subgroupOf t) : ↥t → ↥t → Prop)
    ((fun (g : α) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) ((f (Quotient.mk'' g))⁻¹ * g) ⋯) b)
    ((fun (g : α) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) ((f (Quotient.mk'' g))⁻¹ * g) ⋯) c)
have rw : HMul.hMul (α := ↥t) ((fun (g : α) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) ((f (Quotient.mk'' g))⁻¹ * g) sorry) b)⁻¹
    ((fun (g : α) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) ((f (Quotient.mk'' g))⁻¹ * g) sorry) c) ∈
  s.subgroupOf t
Tactic: rw [leftRel_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α ⧸ s
b c : α
h : (leftRel s : α → α → Prop) b c
⊢ HMul.hMul (α := ↥t) ((fun (g : α) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) ((f (Quotient.mk'' g))⁻¹ * g) ⋯) b)⁻¹
      ((fun (g : α) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) ((f (Quotient.mk'' g))⁻¹ * g) ⋯) c) ∈
    s.subgroupOf t
have change : ((f (↑b : α ⧸ t))⁻¹ * b)⁻¹ * ((f (↑c : α ⧸ t))⁻¹ * c) ∈ s
Tactic: change ((f b)⁻¹ * b)⁻¹ * ((f c)⁻¹ * c) ∈ s
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (hypothesis)
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α ⧸ s
b c : α
h : (leftRel s : α → α → Prop) b c
⊢ ((f (↑b : α ⧸ t))⁻¹ * b)⁻¹ * ((f (↑c : α ⧸ t))⁻¹ * c) ∈ s
have key : f (↑b : α ⧸ t) = f (↑c : α ⧸ t)
Tactic: have key : f b = f c :=
          congr_arg f (Quotient.sound' (leftRel_apply.mpr (h_le (leftRel_apply.mp h))))
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α ⧸ s
b c : α
h : (leftRel s : α → α → Prop) b c
key : f (↑b : α ⧸ t) = f (↑c : α ⧸ t)
⊢ ((f (↑b : α ⧸ t))⁻¹ * b)⁻¹ * ((f (↑c : α ⧸ t))⁻¹ * c) ∈ s
have rwa : ((f (↑c : α ⧸ t))⁻¹ * b)⁻¹ * ((f (↑c : α ⧸ t))⁻¹ * c) ∈ s
Tactic: rwa [key, mul_inv_rev, inv_inv, mul_assoc, mul_inv_cancel_left, ← leftRel_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α ⧸ s
b c : α
h : (leftRel s : α → α → Prop) b c
key : f (↑b : α ⧸ t) = f (↑c : α ⧸ t)
rwa : ((f (↑c : α ⧸ t))⁻¹ * b)⁻¹ * ((f (↑c : α ⧸ t))⁻¹ * c) ∈ s
⊢ ((f (↑b : α ⧸ t))⁻¹ * b)⁻¹ * ((f (↑c : α ⧸ t))⁻¹ * c) ∈ s
have rwa₁ : b⁻¹ * (f (↑c : α ⧸ t))⁻¹⁻¹ * ((f (↑c : α ⧸ t))⁻¹ * c) ∈ s
Tactic: rwa [key, mul_inv_rev, inv_inv, mul_assoc, mul_inv_cancel_left, ← leftRel_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α ⧸ s
b c : α
h : (leftRel s : α → α → Prop) b c
key : f (↑b : α ⧸ t) = f (↑c : α ⧸ t)
rwa : ((f (↑c : α ⧸ t))⁻¹ * b)⁻¹ * ((f (↑c : α ⧸ t))⁻¹ * c) ∈ s
rwa₁ : b⁻¹ * (f (↑c : α ⧸ t))⁻¹⁻¹ * ((f (↑c : α ⧸ t))⁻¹ * c) ∈ s
⊢ ((f (↑b : α ⧸ t))⁻¹ * b)⁻¹ * ((f (↑c : α ⧸ t))⁻¹ * c) ∈ s
have rwa₂ : b⁻¹ * f (↑c : α ⧸ t) * ((f (↑c : α ⧸ t))⁻¹ * c) ∈ s
Tactic: rwa [key, mul_inv_rev, inv_inv, mul_assoc, mul_inv_cancel_left, ← leftRel_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α ⧸ s
b c : α
h : (leftRel s : α → α → Prop) b c
key : f (↑b : α ⧸ t) = f (↑c : α ⧸ t)
rwa : ((f (↑c : α ⧸ t))⁻¹ * b)⁻¹ * ((f (↑c : α ⧸ t))⁻¹ * c) ∈ s
rwa₁ : b⁻¹ * (f (↑c : α ⧸ t))⁻¹⁻¹ * ((f (↑c : α ⧸ t))⁻¹ * c) ∈ s
rwa₂ : b⁻¹ * f (↑c : α ⧸ t) * ((f (↑c : α ⧸ t))⁻¹ * c) ∈ s
⊢ ((f (↑b : α ⧸ t))⁻¹ * b)⁻¹ * ((f (↑c : α ⧸ t))⁻¹ * c) ∈ s
have rwa₃ : b⁻¹ * (f (↑c : α ⧸ t) * ((f (↑c : α ⧸ t))⁻¹ * c)) ∈ s
Tactic: rwa [key, mul_inv_rev, inv_inv, mul_assoc, mul_inv_cancel_left, ← leftRel_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α ⧸ s
b c : α
h : (leftRel s : α → α → Prop) b c
key : f (↑b : α ⧸ t) = f (↑c : α ⧸ t)
rwa : ((f (↑c : α ⧸ t))⁻¹ * b)⁻¹ * ((f (↑c : α ⧸ t))⁻¹ * c) ∈ s
rwa₁ : b⁻¹ * (f (↑c : α ⧸ t))⁻¹⁻¹ * ((f (↑c : α ⧸ t))⁻¹ * c) ∈ s
rwa₂ : b⁻¹ * f (↑c : α ⧸ t) * ((f (↑c : α ⧸ t))⁻¹ * c) ∈ s
rwa₃ : b⁻¹ * (f (↑c : α ⧸ t) * ((f (↑c : α ⧸ t))⁻¹ * c)) ∈ s
⊢ ((f (↑b : α ⧸ t))⁻¹ * b)⁻¹ * ((f (↑c : α ⧸ t))⁻¹ * c) ∈ s
have rwa₄ : b⁻¹ * c ∈ s
Tactic: rwa [key, mul_inv_rev, inv_inv, mul_assoc, mul_inv_cancel_left, ← leftRel_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : (α ⧸ t) × ↥t ⧸ s.subgroupOf t
b c : ↥t
h : (leftRel (s.subgroupOf t) : ↥t → ↥t → Prop) b c
⊢ (leftRel s : α → α → Prop) ((fun (b : ↥t) ↦ f a.1 * (↑b : α)) b) ((fun (b : ↥t) ↦ f a.1 * (↑b : α)) c)
have rw : ∀ (h : b⁻¹ * c ∈ s.subgroupOf t),
  HMul.hMul (α := α) ((fun (b : ↥t) ↦ f a.1 * (↑b : α)) b)⁻¹ ((fun (b : ↥t) ↦ f a.1 * (↑b : α)) c) ∈ s
Tactic: rw [leftRel_apply] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : (α ⧸ t) × ↥t ⧸ s.subgroupOf t
b c : ↥t
h : b⁻¹ * c ∈ s.subgroupOf t
⊢ (f a.1 * (↑b : α))⁻¹ * (f a.1 * (↑c : α)) ∈ s
have rwa : (↑b : α)⁻¹ * (f a.1)⁻¹ * (f a.1 * (↑c : α)) ∈ s
Tactic: rwa [mul_inv_rev, mul_assoc, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : (α ⧸ t) × ↥t ⧸ s.subgroupOf t
b c : ↥t
h : b⁻¹ * c ∈ s.subgroupOf t
rwa : (↑b : α)⁻¹ * (f a.1)⁻¹ * (f a.1 * (↑c : α)) ∈ s
⊢ (f a.1 * (↑b : α))⁻¹ * (f a.1 * (↑c : α)) ∈ s
have rwa₁ : (↑b : α)⁻¹ * ((f a.1)⁻¹ * (f a.1 * (↑c : α))) ∈ s
Tactic: rwa [mul_inv_rev, mul_assoc, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : (α ⧸ t) × ↥t ⧸ s.subgroupOf t
b c : ↥t
h : b⁻¹ * c ∈ s.subgroupOf t
rwa : (↑b : α)⁻¹ * (f a.1)⁻¹ * (f a.1 * (↑c : α)) ∈ s
rwa₁ : (↑b : α)⁻¹ * ((f a.1)⁻¹ * (f a.1 * (↑c : α))) ∈ s
⊢ (f a.1 * (↑b : α))⁻¹ * (f a.1 * (↑c : α)) ∈ s
have rwa₂ : (↑b : α)⁻¹ * (↑c : α) ∈ s
Tactic: rwa [mul_inv_rev, mul_assoc, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
⊢ LeftInverse (fun (a : (α ⧸ t) × ↥t ⧸ s.subgroupOf t) ↦ Quotient.map' (fun (b : ↥t) ↦ f a.1 * (↑b : α)) ⋯ a.2)
    fun (a : α ⧸ s) ↦
    (Quotient.map' id ⋯ a,
      Quotient.map' (fun (g : α) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) ((f (Quotient.mk'' g))⁻¹ * g) ⋯) ⋯ a)
have refine : ∀ (a : α),
  Eq (α := α ⧸ s)
    ((fun (a : (α ⧸ t) × ↥t ⧸ s.subgroupOf t) ↦
        (Quotient.map' (fun (b : ↥t) ↦ f a.1 * (↑b : α)) sorry a.2 : Quotient (leftRel s)))
      ((fun (a : α ⧸ s) ↦
          ((Quotient.map' id sorry a,
              Quotient.map' (fun (g : α) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) ((f (Quotient.mk'' g))⁻¹ * g) sorry) sorry a) :
            (α ⧸ t) × ↥t ⧸ s.subgroupOf t))
        (Quotient.mk'' a)))
    (Quotient.mk'' a)
Tactic: refine Quotient.ind' fun a => ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α
⊢ Eq (α := α ⧸ s)
    ((fun (a : (α ⧸ t) × ↥t ⧸ s.subgroupOf t) ↦
        (Quotient.map' (fun (b : ↥t) ↦ f a.1 * (↑b : α)) ⋯ a.2 : Quotient (leftRel s)))
      ((fun (a : α ⧸ s) ↦
          ((Quotient.map' id ⋯ a,
              Quotient.map' (fun (g : α) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) ((f (Quotient.mk'' g))⁻¹ * g) ⋯) ⋯ a) :
            (α ⧸ t) × ↥t ⧸ s.subgroupOf t))
        (Quotient.mk'' a)))
    (Quotient.mk'' a)
have simp_rw : Eq (α := α ⧸ s)
  (Quotient.map' (s₁ := leftRel (s.subgroupOf t))
    (fun (b : ↥t) ↦ f (Quotient.map' (s₁ := leftRel s) id sorry (Quotient.mk'' a)) * (↑b : α)) sorry
    (Quotient.map' (s₁ := leftRel s)
      (fun (g : α) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) ((f (Quotient.mk'' g))⁻¹ * g) sorry) sorry (Quotient.mk'' a)))
  (Quotient.mk'' a)
Tactic: simp_rw [Quotient.map'_mk'', id, mul_inv_cancel_left]