awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
H : Subgroup α
inst_3 : Finite.{u + 1} (α ⧸ H)
b : β
h' : Finite.{u + 1} (Quotient (rightRel H))
a : Quotient (rightRel H)
g₁ g₂ : α
r : g₁ * g₂⁻¹ ∈ H
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ H) (g₁ * g₂⁻¹) r • g₂ • b = g₁ • b

Tactic:
simp [mul_smul]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
H : Subgroup α
inst_3 : Finite.{u + 1} (α ⧸ H)
b : β
h' : Finite.{u + 1} (Quotient (rightRel H))
a : Quotient (rightRel H)
g₁ g₂ : α
r : g₁ * g₂⁻¹ ∈ H
⊢ ∃ (x : ↥H), x • g₂ • b = g₁ • b

Tactic:
exact ⟨⟨g₁ * g₂⁻¹, r⟩, by simp [mul_smul]⟩
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
H : Subgroup α
inst_3 : Finite.{u + 1} (α ⧸ H)
b : β
h' : Finite.{u + 1} (Quotient (rightRel H))
f : Quotient (rightRel H) → orbitRel.Quotient.{u, v} (↥H) β :=
  fun (a : Quotient (rightRel H)) ↦ a.liftOn' (fun (g : α) ↦ ⟦g • b⟧) ⋯
⊢ Finite.{v + 1} (orbitRel.Quotient.{u, v} (↥H) β)

Tactic:
Finite.of_surjective f ((Quotient.surjective_liftOn' _).2
      (Quotient.mk''_surjective.comp (MulAction.surjective_smul _ _)))

Premises used: Iff.mpr, Quotient.surjective_liftOn', MulAction.surjective_smul, Quotient.mk''_surjective, Function.Surjective.comp, Finite.of_surjective
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
H : Subgroup α
inst_3 : Finite.{u + 1} (α ⧸ H)
b : β
h' : Finite.{u + 1} (Quotient (rightRel H))
f : Quotient (rightRel H) → orbitRel.Quotient.{u, v} (↥H) β :=
  fun (a : Quotient (rightRel H)) ↦ a.liftOn' (fun (g : α) ↦ ⟦g • b⟧) ⋯
⊢ Finite.{v + 1} (orbitRel.Quotient.{u, v} (↥H) β)

Tactic:
exact Finite.of_surjective f ((Quotient.surjective_liftOn' _).2
      (Quotient.mk''_surjective.comp (MulAction.surjective_smul _ _)))

Premises used: Iff.mpr, Quotient.surjective_liftOn', MulAction.surjective_smul, Quotient.mk''_surjective, Function.Surjective.comp, Finite.of_surjective
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x_1 : β
H : Subgroup α
ω : Quotient (orbitRel α β)
q : orbitRel.Quotient.{u, v} ↥H (↑(orbitRel.Quotient.orbit ω) : Type v)
x : (↑(orbitRel.Quotient.orbit ω) : Type v)
⊢ (↑x : β) ∈ orbitRel.Quotient.orbit ω

Tactic:
have hx := x.property
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x_1 : β
H : Subgroup α
ω : Quotient (orbitRel α β)
q : orbitRel.Quotient.{u, v} ↥H (↑(orbitRel.Quotient.orbit ω) : Type v)
x : (↑(orbitRel.Quotient.orbit ω) : Type v)
hx : (↑x : β) ∈ orbitRel.Quotient.orbit ω
rwa rwa₁ rwa₂ rwa₃ : ∀ (hx : Quotient.mk'' (↑x : β) = ω), ⟦(↑x : β)⟧ = ω
⊢ ⟦(↑x : β)⟧ = ω

Tactic:
rwa [orbitRel.Quotient.mem_orbit] at hx

Premises used: MulAction.orbitRel.Quotient.mem_orbit
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
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)
a b : (↑(orbitRel.Quotient.orbit ω) : Type v)
h :
  (orbitRel ↥H (↑(orbitRel.Quotient.orbit ω) : Type v) :
      (↑(orbitRel.Quotient.orbit ω) : Type v) → (↑(orbitRel.Quotient.orbit ω) : Type v) → Prop)
    a b
⊢ ⟦(↑a : β)⟧ = ⟦(↑b : β)⟧

Tactic:
simp only [← Quotient.eq, orbitRel.Quotient.subgroup_quotient_eq_iff] at h

Premises used: MulAction.orbitRel.Quotient.subgroup_quotient_eq_iff, Quotient.eq
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
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)
a b : (↑(orbitRel.Quotient.orbit ω) : Type v)
h : ⟦(↑a : β)⟧ = ⟦(↑b : β)⟧
simp :
  ∀ (h : (orbitRel (↥H) β : β → β → Prop) (↑a : β) (↑b : β)),
    (Setoid.comap Subtype.val (orbitRel (↥H) β) :
        { x : β // x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω} } →
          { x : β // x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω} } → Prop)
      (Subtype.mk (p := fun (x : β) ↦ x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω}) (↑a : β) ⋯)
      (Subtype.mk (p := fun (x : β) ↦ x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω}) (↑b : β) ⋯)
⊢ Eq.{v + 1} (α :=
    Quotient (α := { x : β // x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω} })
      (Setoid.comap (Subtype.val (p := fun (x : β) ↦ x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω})) (orbitRel.{u, v} (↥H) β)))
    ((fun (x : (↑(orbitRel.Quotient.orbit ω) : Type v)) ↦
        (⟦Subtype.mk (p := fun (x : β) ↦ x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω}) (↑x : β) ⋯⟧ :
          Quotient (α := { x : β // x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω} })
            (Setoid.comap (Subtype.val (p := fun (x : β) ↦ x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω}))
              (orbitRel.{u, v} (↥H) β))))
      a)
    ((fun (x : (↑(orbitRel.Quotient.orbit ω) : Type v)) ↦
        (⟦Subtype.mk (p := fun (x : β) ↦ x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω}) (↑x : β) ⋯⟧ :
          Quotient (α := { x : β // x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω} })
            (Setoid.comap (Subtype.val (p := fun (x : β) ↦ x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω}))
              (orbitRel.{u, v} (↥H) β))))
      b)

Tactic:
simp only [Quotient.eq] at h ⊢

Premises used: Quotient.eq
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
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)
a b : (↑(orbitRel.Quotient.orbit ω) : Type v)
h : (orbitRel (↥H) β : β → β → Prop) (↑a : β) (↑b : β)
⊢ (Setoid.comap Subtype.val (orbitRel (↥H) β) :
      { x : β // x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω} } → { x : β // x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω} } → Prop)
    (Subtype.mk (p := fun (x : β) ↦ x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω}) (↑a : β) ⋯)
    (Subtype.mk (p := fun (x : β) ↦ x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω}) (↑b : β) ⋯)

Tactic:
h

Premises used: Set.Mem
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
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)
a b : (↑(orbitRel.Quotient.orbit ω) : Type v)
h : (orbitRel (↥H) β : β → β → Prop) (↑a : β) (↑b : β)
⊢ (Setoid.comap Subtype.val (orbitRel (↥H) β) :
      { x : β // x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω} } → { x : β // x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω} } → Prop)
    (Subtype.mk (p := fun (x : β) ↦ x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω}) (↑a : β) ⋯)
    (Subtype.mk (p := fun (x : β) ↦ x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω}) (↑b : β) ⋯)

Tactic:
exact h
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x_1 : β
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) β))
x : { x : β // x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω} }
⊢ (↑x : β) ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω}

Tactic:
have hx := x.property
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x_1 : β
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) β))
x : { x : β // x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω} }
hx : (↑x : β) ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω}
⊢ ⟦(↑x : β)⟧ = ω

Tactic:
simp only [Set.mem_preimage, Set.mem_singleton_iff] at hx

Premises used: Set.mem_singleton_iff, Set.mem_preimage
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x_1 : β
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) β))
x : { x : β // x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω} }
hx : ⟦(↑x : β)⟧ = ω
rwa : Quotient.mk'' (↑x : β) = ω
rwa₁ rwa₂ rwa₃ rwa₄ : ⟦(↑x : β)⟧ = ω
⊢ (↑x : β) ∈ orbitRel.Quotient.orbit ω

Tactic:
rwa [orbitRel.Quotient.mem_orbit, @Quotient.mk''_eq_mk]

Premises used: MulAction.orbitRel.Quotient.mem_orbit, Quotient.mk''_eq_mk
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
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
⊢ ⟦(↑a : β)⟧ = ⟦(↑b : β)⟧

Tactic:
rw [Setoid.comap_rel, ← Quotient.eq'', @Quotient.mk''_eq_mk] at h

Premises used: Quotient.eq'', Setoid.comap_rel, Quotient.mk''_eq_mk
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
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 simp : ⟦(↑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)

Tactic:
simp only [orbitRel.Quotient.subgroup_quotient_eq_iff]

Premises used: MulAction.orbitRel.Quotient.subgroup_quotient_eq_iff
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
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 : ⟦(↑a : β)⟧ = ⟦(↑b : β)⟧
⊢ ⟦(↑a : β)⟧ = ⟦(↑b : β)⟧

Tactic:
h
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
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 : ⟦(↑a : β)⟧ = ⟦(↑b : β)⟧
⊢ ⟦(↑a : β)⟧ = ⟦(↑b : β)⟧

Tactic:
exact h
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
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)
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 : β) ⋯⟧)
          ⋯)
        (fun (x : { x : β // x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω} }) ↦
          ⟦Subtype.mk (p := fun (x : β) ↦ x ∈ orbitRel.Quotient.orbit ω) (↑x : β) ⋯⟧)
        ⋯)
      (Quotient.mk'' a)
⊢ 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

Tactic:
induction q using Quotient.inductionOn'
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
H : Subgroup α
ω : Quotient (orbitRel α β)
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 : β) ⋯⟧)
        ⋯)
      (fun (x : { x : β // x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω} }) ↦
        ⟦Subtype.mk (p := fun (x : β) ↦ x ∈ orbitRel.Quotient.orbit ω) (↑x : β) ⋯⟧)
      ⋯)
    (Quotient.mk'' a)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
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) β))
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 : β) ⋯⟧)
          ⋯)
        (fun (x : (↑(orbitRel.Quotient.orbit ω) : Type v)) ↦
          ⟦Subtype.mk (p := fun (x : β) ↦ x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω}) (↑x : β) ⋯⟧)
        ⋯)
      (Quotient.mk'' a)
⊢ 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

Tactic:
induction q using Quotient.inductionOn'
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
H : Subgroup α
ω : Quotient (orbitRel α β)
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 : β) ⋯⟧)
        ⋯)
      (fun (x : (↑(orbitRel.Quotient.orbit ω) : Type v)) ↦
        ⟦Subtype.mk (p := fun (x : β) ↦ x ∈ Quotient.mk (orbitRel α β) ⁻¹' {ω}) (↑x : β) ⋯⟧)
      ⋯)
    (Quotient.mk'' a)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
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)
rw :
  Finite.{v + 1} ((ω : Quotient (orbitRel α β)) × orbitRel.Quotient.{u, v} ↥H (↑(orbitRel.Quotient.orbit ω) : Type v))
⊢ Finite.{v + 1} (orbitRel.Quotient.{u, v} (↥H) β)

Tactic:
rw [(equivSubgroupOrbits β H).finite_iff]

Premises used: Equiv.finite_iff, MulAction.equivSubgroupOrbits
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
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} ((ω : Quotient (orbitRel α β)) × orbitRel.Quotient.{u, v} ↥H (↑(orbitRel.Quotient.orbit ω) : Type v))

Tactic:
infer_instance
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
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₂
⊢ y₁ ∈ orbit.{u, v} (↥H) y₂

Tactic:
rw [orbitRel_apply] at h

Premises used: MulAction.orbitRel_apply
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
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₂
rw : (Exists.choose (p := fun (m : α) ↦ m • y₁ = x) ⋯)⁻¹ * Exists.choose (p := fun (m : α) ↦ m • y₂ = x) ⋯ ∈ H
⊢ 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₂)

Tactic:
rw [Quotient.eq'', leftRel_eq]

Premises used: QuotientGroup.leftRel_eq, Quotient.eq''
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
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₂
rcases :
  ∀ (g : ↥H),
    (Exists.choose (p := fun (m : α) ↦ HSMul.hSMul (β := β) m ((fun (m : ↥H) ↦ m • y₂) g) = x) ⋯)⁻¹ *
        Exists.choose (p := fun (m : α) ↦ m • y₂ = x) ⋯ ∈
      H
⊢ (Exists.choose (p := fun (m : α) ↦ m • y₁ = x) ⋯)⁻¹ * Exists.choose (p := fun (m : α) ↦ m • y₂ = x) ⋯ ∈ H

Tactic:
rcases h with ⟨g, rfl⟩

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
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
dsimp : (Exists.choose (p := fun (m : α) ↦ m • g • y₂ = x) ⋯)⁻¹ * Exists.choose (p := fun (m : α) ↦ m • y₂ = x) ⋯ ∈ H
⊢ (Exists.choose (p := fun (m : α) ↦ HSMul.hSMul (β := β) m ((fun (m : ↥H) ↦ m • y₂) g) = x) ⋯)⁻¹ *
      Exists.choose (p := fun (m : α) ↦ m • y₂ = x) ⋯ ∈
    H

Tactic:
dsimp only
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
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
this :
  Exists.choose (p := fun (m : α) ↦ m • g • y₂ = x) ⋯ = Exists.choose (p := fun (m : α) ↦ m • y₂ = x) ⋯ * (↑g⁻¹ : α)
⊢ (Exists.choose (p := fun (m : α) ↦ m • g • y₂ = x) ⋯)⁻¹ * Exists.choose (p := fun (m : α) ↦ m • y₂ = x) ⋯ ∈ H

Tactic:
simp [this]
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
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
suffices :
  Exists.choose (p := fun (m : α) ↦ m • g • y₂ = x) ⋯ = Exists.choose (p := fun (m : α) ↦ m • y₂ = x) ⋯ * (↑g⁻¹ : α)
⊢ (Exists.choose (p := fun (m : α) ↦ m • g • y₂ = x) ⋯)⁻¹ * Exists.choose (p := fun (m : α) ↦ m • y₂ = x) ⋯ ∈ H

Tactic:
suffices (exists_smul_eq α (g • y₂) x).choose = (exists_smul_eq α y₂ x).choose * g⁻¹ by
      simp [this]
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
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⁻¹ : α)

Tactic:
IsCancelSMul.right_cancel _ _ (g • y₂) ?_

Premises used: IsCancelSMul.right_cancel, HSMul.hSMul
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
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
refine :
  Exists.choose (p := fun (m : α) ↦ m • g • y₂ = x) ⋯ • g • y₂ =
    (Exists.choose (p := fun (m : α) ↦ m • y₂ = x) ⋯ * (↑g⁻¹ : α)) • g • y₂
⊢ Exists.choose (p := fun (m : α) ↦ m • g • y₂ = x) ⋯ = Exists.choose (p := fun (m : α) ↦ m • y₂ = x) ⋯ * (↑g⁻¹ : α)

Tactic:
refine IsCancelSMul.right_cancel _ _ (g • y₂) ?_

Premises used: IsCancelSMul.right_cancel, HSMul.hSMul
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
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₂
rw₅ rw₆ : x = x
⊢ Exists.choose (p := fun (m : α) ↦ m • g • y₂ = x) ⋯ • g • y₂ =
    (Exists.choose (p := fun (m : α) ↦ m • y₂ = x) ⋯ * (↑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]

Premises used: Exists.choose_spec, Subgroup.coe_inv, smul_smul, Subgroup.smul_def, HSMul.hSMul, MulAction.exists_smul_eq, inv_mul_cancel_right
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
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₂
⊢ g₁⁻¹ * g₂ ∈ H

Tactic:
rw [leftRel_eq] at h

Premises used: QuotientGroup.leftRel_eq