awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (hypothesis)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
H : Subgroup α
ω : Quotient (orbitRel α β)
q :
  Quotient (α := { x : β // x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω} })
    (Setoid.comap (Subtype.val (p := fun (x : β) ↦ x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω})) (orbitRel.{u, v} (↥H) β))
a b : { x : β // x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω} }
h :
  (Setoid.comap Subtype.val (orbitRel (↥H) β) :
      { x : β // x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω} } → { x : β // x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω} } → Prop)
    a b
⊢ Eq.{v + 1} (α := orbitRel.Quotient.{u, v} ↥H (↑(orbitRel.Quotient.orbit ω) : Type v))
    ((fun (x : { x : β // x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω} }) ↦
        (⟦Subtype.mk (p := fun (x : β) ↦ x ∈ orbitRel.Quotient.orbit ω) (↑x : β) ⋯⟧ :
          Quotient (α := (↑(orbitRel.Quotient.orbit ω) : Type v))
            (orbitRel.{u, v} ↥H (↑(orbitRel.Quotient.orbit ω) : Type v))))
      a)
    ((fun (x : { x : β // x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω} }) ↦
        (⟦Subtype.mk (p := fun (x : β) ↦ x ∈ orbitRel.Quotient.orbit ω) (↑x : β) ⋯⟧ :
          Quotient (α := (↑(orbitRel.Quotient.orbit ω) : Type v))
            (orbitRel.{u, v} ↥H (↑(orbitRel.Quotient.orbit ω) : Type v))))
      b)
have h₁ : ⟦(↑a : β)⟧ = ⟦(↑b : β)⟧
Tactic: rw [Setoid.comap_rel, ← Quotient.eq'', @Quotient.mk''_eq_mk] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
H : Subgroup α
ω : Quotient (orbitRel α β)
q : orbitRel.Quotient.{u, v} ↥H (↑(orbitRel.Quotient.orbit ω) : Type v)
⊢ Quotient.liftOn' (s₁ :=
      Setoid.comap (Subtype.val (p := fun (x : β) ↦ x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω})) (orbitRel.{u, v} (↥H) β))
      (Quotient.liftOn' q
        (fun (x : (↑(orbitRel.Quotient.orbit ω) : Type v)) ↦
          ⟦Subtype.mk (p := fun (x : β) ↦ x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω}) (↑x : β) ⋯⟧)
        ⋯)
      (fun (x : { x : β // x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω} }) ↦
        ⟦Subtype.mk (p := fun (x : β) ↦ x ∈ orbitRel.Quotient.orbit ω) (↑x : β) ⋯⟧)
      ⋯ =
    q
have h : ∀ (a : (↑(orbitRel.Quotient.orbit ω) : Type v)),
  Eq (α := orbitRel.Quotient.{u, v} ↥H (↑(orbitRel.Quotient.orbit ω) : Type v))
    (Quotient.liftOn' (s₁ :=
      Setoid.comap (Subtype.val (p := fun (x : β) ↦ x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω})) (orbitRel.{u, v} (↥H) β))
      (Quotient.liftOn' (s₁ := orbitRel.{u, v} ↥H (↑(orbitRel.Quotient.orbit ω) : Type v)) (Quotient.mk'' a)
        (fun (x : (↑(orbitRel.Quotient.orbit ω) : Type v)) ↦
          ⟦Subtype.mk (p := fun (x : β) ↦ x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω}) (↑x : β) sorry⟧)
        sorry)
      (fun (x : { x : β // x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω} }) ↦
        ⟦Subtype.mk (p := fun (x : β) ↦ x ∈ orbitRel.Quotient.orbit ω) (↑x : β) sorry⟧)
      sorry)
    (Quotient.mk'' a)
Tactic: induction q using Quotient.inductionOn'
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
H : Subgroup α
ω : Quotient (orbitRel α β)
q :
  Quotient (α := { x : β // x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω} })
    (Setoid.comap (Subtype.val (p := fun (x : β) ↦ x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω})) (orbitRel.{u, v} (↥H) β))
⊢ Quotient.liftOn' (s₁ := orbitRel.{u, v} ↥H (↑(orbitRel.Quotient.orbit ω) : Type v))
      (q.liftOn'
        (fun (x : { x : β // x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω} }) ↦
          ⟦Subtype.mk (p := fun (x : β) ↦ x ∈ orbitRel.Quotient.orbit ω) (↑x : β) ⋯⟧)
        ⋯)
      (fun (x : (↑(orbitRel.Quotient.orbit ω) : Type v)) ↦
        ⟦Subtype.mk (p := fun (x : β) ↦ x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω}) (↑x : β) ⋯⟧)
      ⋯ =
    q
have h : ∀ (a : { x : β // x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω} }),
  Eq (α :=
    Quotient (α := { x : β // x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω} })
      (Setoid.comap (Subtype.val (p := fun (x : β) ↦ x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω})) (orbitRel.{u, v} (↥H) β)))
    (Quotient.liftOn' (s₁ := orbitRel.{u, v} ↥H (↑(orbitRel.Quotient.orbit ω) : Type v))
      (Quotient.liftOn' (s₁ :=
        Setoid.comap (Subtype.val (p := fun (x : β) ↦ x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω})) (orbitRel.{u, v} (↥H) β))
        (Quotient.mk'' a)
        (fun (x : { x : β // x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω} }) ↦
          ⟦Subtype.mk (p := fun (x : β) ↦ x ∈ orbitRel.Quotient.orbit ω) (↑x : β) sorry⟧)
        sorry)
      (fun (x : (↑(orbitRel.Quotient.orbit ω) : Type v)) ↦
        ⟦Subtype.mk (p := fun (x : β) ↦ x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω}) (↑x : β) sorry⟧)
      sorry)
    (Quotient.mk'' a)
Tactic: induction q using Quotient.inductionOn'
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
H : Subgroup α
inst_2 : Finite.{v + 1} (orbitRel.Quotient α β)
inst_3 : Finite.{u + 1} (α ⧸ H)
⊢ Finite.{v + 1} (orbitRel.Quotient.{u, v} (↥H) β)
have rw : Finite.{v + 1} ((ω : Quotient (orbitRel α β)) × orbitRel.Quotient.{u, v} ↥H (↑(orbitRel.Quotient.orbit ω) : Type v))
Tactic: rw [(equivSubgroupOrbits β H).finite_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (hypothesis)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
inst_3 : IsCancelSMul α β
H : Subgroup α
q : orbitRel.Quotient.{u, v} (↥H) β
y₁ y₂ : β
h : (orbitRel (↥H) β : β → β → Prop) y₁ y₂
⊢ Eq.{u + 1} (α := α ⧸ H) ((fun (y : β) ↦ ((↑(Exists.choose (p := fun (m : α) ↦ m • y = x) ⋯) : α ⧸ H) : α ⧸ H)) y₁)
    ((fun (y : β) ↦ ((↑(Exists.choose (p := fun (m : α) ↦ m • y = x) ⋯) : α ⧸ H) : α ⧸ H)) y₂)
have h₁ : y₁ ∈ orbit.{u, v} (↥H) y₂
Tactic: rw [orbitRel_apply] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
inst_3 : IsCancelSMul α β
H : Subgroup α
q : orbitRel.Quotient.{u, v} (↥H) β
y₁ y₂ : β
h : y₁ ∈ orbit.{u, v} (↥H) y₂
⊢ Eq.{u + 1} (α := α ⧸ H) ((fun (y : β) ↦ ((↑(Exists.choose (p := fun (m : α) ↦ m • y = x) ⋯) : α ⧸ H) : α ⧸ H)) y₁)
    ((fun (y : β) ↦ ((↑(Exists.choose (p := fun (m : α) ↦ m • y = x) ⋯) : α ⧸ H) : α ⧸ H)) y₂)
have rw : (fun (x y : α) ↦ x⁻¹ * y ∈ H) (Exists.choose (p := fun (m : α) ↦ m • y₁ = x) sorry)
  (Exists.choose (p := fun (m : α) ↦ m • y₂ = x) sorry)
Tactic: rw [Quotient.eq'', leftRel_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
inst_3 : IsCancelSMul α β
H : Subgroup α
q : orbitRel.Quotient.{u, v} (↥H) β
y₁ y₂ : β
h : y₁ ∈ orbit.{u, v} (↥H) y₂
⊢ (Exists.choose (p := fun (m : α) ↦ m • y₁ = x) ⋯)⁻¹ * Exists.choose (p := fun (m : α) ↦ m • y₂ = x) ⋯ ∈ H
have rcases : ∀ (g : ↥H),
  (Exists.choose (p := fun (m : α) ↦ HSMul.hSMul (β := β) m ((fun (m : ↥H) ↦ m • y₂) g) = x) sorry)⁻¹ *
      Exists.choose (p := fun (m : α) ↦ m • y₂ = x) sorry ∈
    H
Tactic: rcases h with ⟨g, rfl⟩
Cleared hypotheses: y₁, h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
inst_3 : IsCancelSMul α β
H : Subgroup α
q : orbitRel.Quotient.{u, v} (↥H) β
y₂ : β
g : ↥H
⊢ (Exists.choose (p := fun (m : α) ↦ m • g • y₂ = x) ⋯)⁻¹ * Exists.choose (p := fun (m : α) ↦ m • y₂ = x) ⋯ ∈ H
have suffices : Exists.choose (p := fun (m : α) ↦ m • g • y₂ = x) sorry = Exists.choose (p := fun (m : α) ↦ m • y₂ = x) sorry * (↑g⁻¹ : α)
Tactic: suffices (exists_smul_eq α (g • y₂) x).choose = (exists_smul_eq α y₂ x).choose * g⁻¹ by
      simp [this]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
inst_3 : IsCancelSMul α β
H : Subgroup α
q : orbitRel.Quotient.{u, v} (↥H) β
y₂ : β
g : ↥H
⊢ Exists.choose (p := fun (m : α) ↦ m • g • y₂ = x) ⋯ = Exists.choose (p := fun (m : α) ↦ m • y₂ = x) ⋯ * (↑g⁻¹ : α)
have refine : Exists.choose (p := fun (m : α) ↦ m • g • y₂ = x) sorry • g • y₂ =
  (Exists.choose (p := fun (m : α) ↦ m • y₂ = x) sorry * (↑g⁻¹ : α)) • g • y₂
Tactic: refine IsCancelSMul.right_cancel _ _ (g • y₂) ?_
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
inst_3 : IsCancelSMul α β
H : Subgroup α
q : orbitRel.Quotient.{u, v} (↥H) β
y₂ : β
g : ↥H
⊢ Exists.choose (p := fun (m : α) ↦ m • g • y₂ = x) ⋯ • g • y₂ =
    (Exists.choose (p := fun (m : α) ↦ m • y₂ = x) ⋯ * (↑g⁻¹ : α)) • g • y₂
have rw : x = (Exists.choose (p := fun (m : α) ↦ m • y₂ = x) sorry * (↑g⁻¹ : α)) • g • y₂
Tactic: rw [(exists_smul_eq α (g • y₂) x).choose_spec, Subgroup.smul_def, Subgroup.coe_inv,
        smul_smul, inv_mul_cancel_right, (exists_smul_eq α y₂ x).choose_spec]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
inst_3 : IsCancelSMul α β
H : Subgroup α
q : orbitRel.Quotient.{u, v} (↥H) β
y₂ : β
g : ↥H
rw : x = (Exists.choose (p := fun (m : α) ↦ m • y₂ = x) ⋯ * (↑g⁻¹ : α)) • g • y₂
⊢ Exists.choose (p := fun (m : α) ↦ m • g • y₂ = x) ⋯ • g • y₂ =
    (Exists.choose (p := fun (m : α) ↦ m • y₂ = x) ⋯ * (↑g⁻¹ : α)) • g • y₂
have rw₁ : x = (Exists.choose (p := fun (m : α) ↦ m • y₂ = x) sorry * (↑g⁻¹ : α)) • (↑g : α) • y₂
Tactic: rw [(exists_smul_eq α (g • y₂) x).choose_spec, Subgroup.smul_def, Subgroup.coe_inv,
        smul_smul, inv_mul_cancel_right, (exists_smul_eq α y₂ x).choose_spec]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
inst_3 : IsCancelSMul α β
H : Subgroup α
q : orbitRel.Quotient.{u, v} (↥H) β
y₂ : β
g : ↥H
rw : x = (Exists.choose (p := fun (m : α) ↦ m • y₂ = x) ⋯ * (↑g⁻¹ : α)) • g • y₂
rw₁ : x = (Exists.choose (p := fun (m : α) ↦ m • y₂ = x) ⋯ * (↑g⁻¹ : α)) • (↑g : α) • y₂
⊢ Exists.choose (p := fun (m : α) ↦ m • g • y₂ = x) ⋯ • g • y₂ =
    (Exists.choose (p := fun (m : α) ↦ m • y₂ = x) ⋯ * (↑g⁻¹ : α)) • g • y₂
have rw₂ : x = (Exists.choose (p := fun (m : α) ↦ m • y₂ = x) sorry * (↑g : α)⁻¹) • (↑g : α) • y₂
Tactic: rw [(exists_smul_eq α (g • y₂) x).choose_spec, Subgroup.smul_def, Subgroup.coe_inv,
        smul_smul, inv_mul_cancel_right, (exists_smul_eq α y₂ x).choose_spec]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
inst_3 : IsCancelSMul α β
H : Subgroup α
q : orbitRel.Quotient.{u, v} (↥H) β
y₂ : β
g : ↥H
rw : x = (Exists.choose (p := fun (m : α) ↦ m • y₂ = x) ⋯ * (↑g⁻¹ : α)) • g • y₂
rw₁ : x = (Exists.choose (p := fun (m : α) ↦ m • y₂ = x) ⋯ * (↑g⁻¹ : α)) • (↑g : α) • y₂
rw₂ : x = (Exists.choose (p := fun (m : α) ↦ m • y₂ = x) ⋯ * (↑g : α)⁻¹) • (↑g : α) • y₂
⊢ Exists.choose (p := fun (m : α) ↦ m • g • y₂ = x) ⋯ • g • y₂ =
    (Exists.choose (p := fun (m : α) ↦ m • y₂ = x) ⋯ * (↑g⁻¹ : α)) • g • y₂
have rw₃ : x = (Exists.choose (p := fun (m : α) ↦ m • y₂ = x) sorry * (↑g : α)⁻¹ * (↑g : α)) • y₂
Tactic: rw [(exists_smul_eq α (g • y₂) x).choose_spec, Subgroup.smul_def, Subgroup.coe_inv,
        smul_smul, inv_mul_cancel_right, (exists_smul_eq α y₂ x).choose_spec]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
inst_3 : IsCancelSMul α β
H : Subgroup α
q : orbitRel.Quotient.{u, v} (↥H) β
y₂ : β
g : ↥H
rw : x = (Exists.choose (p := fun (m : α) ↦ m • y₂ = x) ⋯ * (↑g⁻¹ : α)) • g • y₂
rw₁ : x = (Exists.choose (p := fun (m : α) ↦ m • y₂ = x) ⋯ * (↑g⁻¹ : α)) • (↑g : α) • y₂
rw₂ : x = (Exists.choose (p := fun (m : α) ↦ m • y₂ = x) ⋯ * (↑g : α)⁻¹) • (↑g : α) • y₂
rw₃ : x = (Exists.choose (p := fun (m : α) ↦ m • y₂ = x) ⋯ * (↑g : α)⁻¹ * (↑g : α)) • y₂
⊢ Exists.choose (p := fun (m : α) ↦ m • g • y₂ = x) ⋯ • g • y₂ =
    (Exists.choose (p := fun (m : α) ↦ m • y₂ = x) ⋯ * (↑g⁻¹ : α)) • g • y₂
have rw₄ : x = Exists.choose (p := fun (m : α) ↦ m • y₂ = x) sorry • y₂
Tactic: rw [(exists_smul_eq α (g • y₂) x).choose_spec, Subgroup.smul_def, Subgroup.coe_inv,
        smul_smul, inv_mul_cancel_right, (exists_smul_eq α y₂ x).choose_spec]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
inst_3 : IsCancelSMul α β
H : Subgroup α
q : orbitRel.Quotient.{u, v} (↥H) β
y₂ : β
g : ↥H
rw : x = (Exists.choose (p := fun (m : α) ↦ m • y₂ = x) ⋯ * (↑g⁻¹ : α)) • g • y₂
rw₁ : x = (Exists.choose (p := fun (m : α) ↦ m • y₂ = x) ⋯ * (↑g⁻¹ : α)) • (↑g : α) • y₂
rw₂ : x = (Exists.choose (p := fun (m : α) ↦ m • y₂ = x) ⋯ * (↑g : α)⁻¹) • (↑g : α) • y₂
rw₃ : x = (Exists.choose (p := fun (m : α) ↦ m • y₂ = x) ⋯ * (↑g : α)⁻¹ * (↑g : α)) • y₂
rw₄ : x = Exists.choose (p := fun (m : α) ↦ m • y₂ = x) ⋯ • y₂
⊢ Exists.choose (p := fun (m : α) ↦ m • g • y₂ = x) ⋯ • g • y₂ =
    (Exists.choose (p := fun (m : α) ↦ m • y₂ = x) ⋯ * (↑g⁻¹ : α)) • g • y₂
have rw₅ : x = x
Tactic: rw [(exists_smul_eq α (g • y₂) x).choose_spec, Subgroup.smul_def, Subgroup.coe_inv,
        smul_smul, inv_mul_cancel_right, (exists_smul_eq α y₂ x).choose_spec]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (hypothesis)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
inst_3 : IsCancelSMul α β
H : Subgroup α
q : α ⧸ H
g₁ g₂ : α
h : (leftRel H : α → α → Prop) g₁ g₂
⊢ Eq.{v + 1} (α := orbitRel.Quotient.{u, v} (↥H) β) ((fun (g : α) ↦ ⟦g⁻¹ • x⟧) g₁) ((fun (g : α) ↦ ⟦g⁻¹ • x⟧) g₂)
have h₁ : g₁⁻¹ * g₂ ∈ H
Tactic: rw [leftRel_eq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
inst_3 : IsCancelSMul α β
H : Subgroup α
q : α ⧸ H
g₁ g₂ : α
h : g₁⁻¹ * g₂ ∈ H
⊢ ⟦g₁⁻¹ • x⟧ = ⟦g₂⁻¹ • x⟧
have rw : g₁⁻¹ • x ∈ orbit.{u, v} (↥H) (g₂⁻¹ • x)
Tactic: rw [← @Quotient.mk''_eq_mk, Quotient.eq'', orbitRel_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
inst_3 : IsCancelSMul α β
H : Subgroup α
y : orbitRel.Quotient.{u, v} (↥H) β
⊢ (fun (q : α ⧸ H) ↦ (Quotient.liftOn' q (fun (g : α) ↦ ⟦g⁻¹ • x⟧) ⋯ : orbitRel.Quotient.{u, v} (↥H) β))
      ((fun (q : orbitRel.Quotient.{u, v} (↥H) β) ↦
          Quotient.liftOn' q (fun (y : β) ↦ (↑(Exists.choose (p := fun (m : α) ↦ m • y = x) ⋯) : α ⧸ H)) ⋯)
        y) =
    y
have h : ∀ (a : β),
  Eq (α := orbitRel.Quotient.{u, v} (↥H) β)
    ((fun (q : α ⧸ H) ↦ (Quotient.liftOn' q (fun (g : α) ↦ ⟦g⁻¹ • x⟧) sorry : orbitRel.Quotient.{u, v} (↥H) β))
      ((fun (q : orbitRel.Quotient.{u, v} (↥H) β) ↦
          Quotient.liftOn' q (fun (y : β) ↦ (↑(Exists.choose (p := fun (m : α) ↦ m • y = x) sorry) : α ⧸ H)) sorry)
        (Quotient.mk'' a)))
    (Quotient.mk'' a)
Tactic: cases y using Quotient.inductionOn'
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
inst_3 : IsCancelSMul α β
H : Subgroup α
a : β
⊢ ⟦(Exists.choose (p := fun (m : α) ↦ m • a = x) ⋯)⁻¹ • x⟧ = Quotient.mk'' a
have h : (Exists.choose (p := fun (m : α) ↦ m • a = x) sorry)⁻¹ • x ∈ orbit.{u, v} (↥H) a
Tactic: rw [← @Quotient.mk''_eq_mk, Quotient.eq'', orbitRel_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
inst_3 : IsCancelSMul α β
H : Subgroup α
a : β
⊢ (Exists.choose (p := fun (m : α) ↦ m • a = x) ⋯)⁻¹ • x ∈ orbit.{u, v} (↥H) a
have h : (Exists.choose (p := fun (m : α) ↦ m • a = x) sorry)⁻¹ • x = a
Tactic: convert! mem_orbit_self _
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
inst_3 : IsCancelSMul α β
H : Subgroup α
a : β
⊢ (Exists.choose (p := fun (m : α) ↦ m • a = x) ⋯)⁻¹ • x = a
have h : x = Exists.choose (p := fun (m : α) ↦ m • a = x) sorry • a
Tactic: rw [inv_smul_eq_iff, (exists_smul_eq α _ x).choose_spec]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
inst_3 : IsCancelSMul α β
H : Subgroup α
a : β
h : x = Exists.choose (p := fun (m : α) ↦ m • a = x) ⋯ • a
⊢ (Exists.choose (p := fun (m : α) ↦ m • a = x) ⋯)⁻¹ • x = a
have h₁ : x = x
Tactic: rw [inv_smul_eq_iff, (exists_smul_eq α _ x).choose_spec]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
inst_3 : IsCancelSMul α β
H : Subgroup α
g : α ⧸ H
⊢ (fun (q : orbitRel.Quotient.{u, v} (↥H) β) ↦
        Quotient.liftOn' q (fun (y : β) ↦ (↑(Exists.choose (p := fun (m : α) ↦ m • y = x) ⋯) : α ⧸ H)) ⋯)
      ((fun (q : α ⧸ H) ↦ (Quotient.liftOn' q (fun (g : α) ↦ ⟦g⁻¹ • x⟧) ⋯ : orbitRel.Quotient.{u, v} (↥H) β)) g) =
    g
have h : ∀ (g : α),
  Eq (α := α ⧸ H)
    ((fun (q : orbitRel.Quotient.{u, v} (↥H) β) ↦
        Quotient.liftOn' q (fun (y : β) ↦ (↑(Exists.choose (p := fun (m : α) ↦ m • y = x) sorry) : α ⧸ H)) sorry)
      ((fun (q : α ⧸ H) ↦ (Quotient.liftOn' q (fun (g : α) ↦ ⟦g⁻¹ • x⟧) sorry : orbitRel.Quotient.{u, v} (↥H) β))
        (Quotient.mk'' g)))
    (Quotient.mk'' g)
Tactic: cases g using Quotient.inductionOn' with | _ g
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
inst_3 : IsCancelSMul α β
H : Subgroup α
g : α
⊢ Eq (α := α ⧸ H) (Quotient.mk'' (Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯)) (Quotient.mk'' g)
have h : (fun (x y : α) ↦ x⁻¹ * y ∈ H) (Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) sorry) g
Tactic: rw [Quotient.eq'', leftRel_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
inst_3 : IsCancelSMul α β
H : Subgroup α
g : α
⊢ (Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯)⁻¹ * g ∈ H
have h : (Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) sorry)⁻¹ * g = 1
Tactic: convert! one_mem H
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
inst_3 : IsCancelSMul α β
H : Subgroup α
g : α
⊢ (Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯)⁻¹ * g = 1
have h : Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) sorry = g
Tactic: rw [inv_mul_eq_one, eq_comm, ← inv_mul_eq_one, ← Subgroup.mem_bot,
        ← IsCancelSMul.stabilizer_eq_bot (g⁻¹ • x), mem_stabilizer_iff, mul_smul,
        (exists_smul_eq α (g⁻¹ • x) x).choose_spec]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
inst_3 : IsCancelSMul α β
H : Subgroup α
g : α
h : Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯ = g
⊢ (Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯)⁻¹ * g = 1
have h₁ : g = Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) sorry
Tactic: rw [inv_mul_eq_one, eq_comm, ← inv_mul_eq_one, ← Subgroup.mem_bot,
        ← IsCancelSMul.stabilizer_eq_bot (g⁻¹ • x), mem_stabilizer_iff, mul_smul,
        (exists_smul_eq α (g⁻¹ • x) x).choose_spec]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
inst_3 : IsCancelSMul α β
H : Subgroup α
g : α
h : Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯ = g
h₁ : g = Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯
⊢ (Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯)⁻¹ * g = 1
have h₂ : g⁻¹ * Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) sorry = 1
Tactic: rw [inv_mul_eq_one, eq_comm, ← inv_mul_eq_one, ← Subgroup.mem_bot,
        ← IsCancelSMul.stabilizer_eq_bot (g⁻¹ • x), mem_stabilizer_iff, mul_smul,
        (exists_smul_eq α (g⁻¹ • x) x).choose_spec]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
inst_3 : IsCancelSMul α β
H : Subgroup α
g : α
h : Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯ = g
h₁ : g = Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯
h₂ : g⁻¹ * Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯ = 1
⊢ (Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯)⁻¹ * g = 1
have h₃ : Membership.mem (γ := Subgroup α) ⊥ (g⁻¹ * Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) sorry)
Tactic: rw [inv_mul_eq_one, eq_comm, ← inv_mul_eq_one, ← Subgroup.mem_bot,
        ← IsCancelSMul.stabilizer_eq_bot (g⁻¹ • x), mem_stabilizer_iff, mul_smul,
        (exists_smul_eq α (g⁻¹ • x) x).choose_spec]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
inst_3 : IsCancelSMul α β
H : Subgroup α
g : α
h : Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯ = g
h₁ : g = Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯
h₂ : g⁻¹ * Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯ = 1
h₃ : Membership.mem (γ := Subgroup α) ⊥ (g⁻¹ * Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯)
⊢ (Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯)⁻¹ * g = 1
have h₄ : Membership.mem (γ := Subgroup α) (stabilizer α (g⁻¹ • x)) (g⁻¹ * Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) sorry)
Tactic: rw [inv_mul_eq_one, eq_comm, ← inv_mul_eq_one, ← Subgroup.mem_bot,
        ← IsCancelSMul.stabilizer_eq_bot (g⁻¹ • x), mem_stabilizer_iff, mul_smul,
        (exists_smul_eq α (g⁻¹ • x) x).choose_spec]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
inst_3 : IsCancelSMul α β
H : Subgroup α
g : α
h : Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯ = g
h₁ : g = Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯
h₂ : g⁻¹ * Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯ = 1
h₃ : Membership.mem (γ := Subgroup α) ⊥ (g⁻¹ * Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯)
h₄ :
  Membership.mem (γ := Subgroup α) (stabilizer α (g⁻¹ • x)) (g⁻¹ * Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯)
⊢ (Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯)⁻¹ * g = 1
have h₅ : (g⁻¹ * Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) sorry) • g⁻¹ • x = g⁻¹ • x
Tactic: rw [inv_mul_eq_one, eq_comm, ← inv_mul_eq_one, ← Subgroup.mem_bot,
        ← IsCancelSMul.stabilizer_eq_bot (g⁻¹ • x), mem_stabilizer_iff, mul_smul,
        (exists_smul_eq α (g⁻¹ • x) x).choose_spec]