awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
M : Type u
inst : Monoid M
α : Type v
inst_1 : MulAction M α
a : α
mp : (orbit M a).Subsingleton → ∀ (m : M), m • a = a
mpr : (∀ (m : M), m • a = a) → (orbit M a).Subsingleton
⊢ (orbit M a).Subsingleton ↔ ∀ (m : M), m • a = a

Tactic:
constructor
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
M : Type u
inst : Monoid M
α : Type v
inst_1 : MulAction M α
a : α
⊢ (orbit M a).Subsingleton → ∀ (m : M), m • a = a

Tactic:
fun h m ↦ h (mem_orbit a m) (mem_orbit_self a)

Premises used: MulAction.mem_orbit, MulAction.mem_orbit_self
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
M : Type u
inst : Monoid M
α : Type v
inst_1 : MulAction M α
a : α
⊢ (orbit M a).Subsingleton → ∀ (m : M), m • a = a

Tactic:
exact fun h m ↦ h (mem_orbit a m) (mem_orbit_self a)
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
M : Type u
inst : Monoid M
α : Type v
inst_1 : MulAction M α
a : α
h : ∀ (m : M), m • a = a
m p : M
⊢ Eq.{v + 1} (α := α) ((fun (m : M) ↦ m • a) m) ((fun (m : M) ↦ m • a) p)

Tactic:
simp only [h]
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
M : Type u
inst : Monoid M
α : Type v
inst_1 : MulAction M α
a : α
inst_2 : Fintype (↑(orbit M a) : Type v)
⊢ a ∈ fixedPoints M α ↔ Fintype.card.{v} (↑(orbit M a) : Type v) = 1

Tactic:
simp only [← subsingleton_orbit_iff_mem_fixedPoints, le_antisymm_iff,
    Fintype.card_le_one_iff_subsingleton, Nat.add_one_le_iff, Fintype.card_pos_iff,
    Set.subsingleton_coe, iff_self_and, Set.nonempty_coe_sort, nonempty_orbit, implies_true]

Premises used: MulAction.nonempty_orbit, Set.nonempty_coe_sort, iff_self_and, Nat.add_one_le_iff, le_antisymm_iff, Set.subsingleton_coe, implies_true, Fintype.card_pos_iff, MulAction.subsingleton_orbit_iff_mem_fixedPoints, Fintype.card_le_one_iff_subsingleton
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
M : Type u
inst : Monoid M
α : Type v
inst_1 : MulAction M α
β : Type u_1
inst_2 : MulAction M β
m : M
inst_3 : DecidableEq β
b : β
⊢ Decidable (m • b = b)

Tactic:
infer_instance
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
M : Type u_1
G : Type u_2
inst : Monoid M
inst_1 : AddGroup G
inst_2 : DistribMulAction M G
k : M
h : ∀ (x : G), k • x = 0 → x = 0
a b : G
h' : k • a = k • b
rw : a - b = 0
⊢ a = b

Tactic:
rw [← sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
M : Type u_1
G : Type u_2
inst : Monoid M
inst_1 : AddGroup G
inst_2 : DistribMulAction M G
k : M
h : ∀ (x : G), k • x = 0 → x = 0
a b : G
h' : k • a = k • b
⊢ a - b = 0

Tactic:
h _ ?_
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
M : Type u_1
G : Type u_2
inst : Monoid M
inst_1 : AddGroup G
inst_2 : DistribMulAction M G
k : M
h : ∀ (x : G), k • x = 0 → x = 0
a b : G
h' : k • a = k • b
refine : k • (a - b) = 0
⊢ a - b = 0

Tactic:
refine h _ ?_
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
M : Type u_1
G : Type u_2
inst : Monoid M
inst_1 : AddGroup G
inst_2 : DistribMulAction M G
k : M
h : ∀ (x : G), k • x = 0 → x = 0
a b : G
h' : k • a = k • b
rw : k • a - k • b = 0
rw₁ : k • b - k • b = 0
rw₂ rw₃ : Eq.{u_2 + 1} (α := G) 0 0
⊢ k • (a - b) = 0

Tactic:
rw [smul_sub, h', sub_self]

Premises used: sub_self, smul_sub
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : Subsingleton α
a : ∀ (x : α), x ∈ fixedPoints G α
⊢ fixedPoints G α = Set.univ

Tactic:
apply Set.eq_univ_of_forall

Premises used: Set.eq_univ_of_forall
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : Subsingleton α
x : α
hx : G
⊢ hx • x = x

Tactic:
apply Subsingleton.elim ..

Premises used: Subsingleton.elim
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
h : fixedPoints G α ≠ Set.univ
⊢ Nontrivial α

Tactic:
(subsingleton_or_nontrivial α).resolve_left fun _ ↦ h fixedPoints_of_subsingleton

Premises used: MulAction.fixedPoints_of_subsingleton, subsingleton_or_nontrivial, Or.resolve_left
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
g : G
a : α
⊢ g • orbit G a = orbit G a

Tactic:
(smul_orbit_subset g a).antisymm <|
    calc
      orbit G a = g • g⁻¹ • orbit G a := (smul_inv_smul _ _).symm
      _ ⊆ g • orbit G a := Set.image_mono (smul_orbit_subset _ _)

Premises used: Trans.trans, Set.image_mono, MulAction.smul_orbit_subset, smul_inv_smul, HasSubset.Subset.antisymm, Eq.symm
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MulAction G β
a : α
g h : G
h₁ :
  (h * g⁻¹) • Subtype.mk (p := fun (x : α) ↦ x ∈ orbit G a) ((fun (m : G) ↦ m • a) g) ⋯ =
    Subtype.mk (p := fun (x : α) ↦ x ∈ orbit G a) ((fun (m : G) ↦ m • a) h) ⋯
⊢ ∃ (g_1 : G),
    g_1 • Subtype.mk (p := fun (x : α) ↦ x ∈ orbit G a) ((fun (m : G) ↦ m • a) g) ⋯ =
      Subtype.mk (p := fun (x : α) ↦ x ∈ orbit G a) ((fun (m : G) ↦ m • a) h) ⋯

Tactic:
use h * g⁻¹
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MulAction G β
a : α
g h : G
h₁ :
  (↑((h * g⁻¹) • Subtype.mk (p := fun (x : α) ↦ x ∈ orbit G a) ((fun (m : G) ↦ m • a) g) ⋯) : α) =
    (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ orbit G a) ((fun (m : G) ↦ m • a) h) ⋯) : α)
⊢ (h * g⁻¹) • Subtype.mk (p := fun (x : α) ↦ x ∈ orbit G a) ((fun (m : G) ↦ m • a) g) ⋯ =
    Subtype.mk (p := fun (x : α) ↦ x ∈ orbit G a) ((fun (m : G) ↦ m • a) h) ⋯

Tactic:
ext1
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MulAction G β
a : α
g h : G
⊢ (↑((h * g⁻¹) • Subtype.mk (p := fun (x : α) ↦ x ∈ orbit G a) ((fun (m : G) ↦ m • a) g) ⋯) : α) =
    (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ orbit G a) ((fun (m : G) ↦ m • a) h) ⋯) : α)

Tactic:
simp [mul_smul]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Subgroup G
⊢ orbitRel.{u_1, u_2} (↥H) α ≤ orbitRel G α

Tactic:
Setoid.le_def.2 mem_orbit_of_mem_orbit_subgroup

Premises used: Iff.mpr, MulAction.mem_orbit_of_mem_orbit_subgroup, Setoid.le_def
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H K : Subgroup G
rw : orbitRel.{u_1, u_2} (↥(H.subgroupOf K)) α = orbitRel.{u_1, u_2} (↥(Subgroup.map K.subtype (H.subgroupOf K))) α
⊢ orbitRel.{u_1, u_2} (↥(H.subgroupOf K)) α = orbitRel.{u_1, u_2} (↥(H ⊓ K)) α

Tactic:
rw [← Subgroup.subgroupOf_map_subtype]

Premises used: Subgroup.subgroupOf_map_subtype
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H K : Subgroup G
a :
  ∀ (x b : α),
    (orbitRel (↥(H.subgroupOf K)) α : α → α → Prop) x b ↔
      (orbitRel (↥(Subgroup.map K.subtype (H.subgroupOf K))) α : α → α → Prop) x b
⊢ orbitRel.{u_1, u_2} (↥(H.subgroupOf K)) α = orbitRel.{u_1, u_2} (↥(Subgroup.map K.subtype (H.subgroupOf K))) α

Tactic:
ext x
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H K : Subgroup G
x b : α
⊢ x ∈ orbit.{u_1, u_2} (↥(H.subgroupOf K)) b ↔ x ∈ orbit.{u_1, u_2} (↥(Subgroup.map K.subtype (H.subgroupOf K))) b

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H K : Subgroup G
x b : α
a :
  ∀ (h : x ∈ orbit.{u_1, u_2} (↥(H.subgroupOf K)) b),
    x ∈ orbit.{u_1, u_2} (↥(Subgroup.map K.subtype (H.subgroupOf K))) b
a₁ :
  ∀ (h : x ∈ orbit.{u_1, u_2} (↥(Subgroup.map K.subtype (H.subgroupOf K))) b),
    x ∈ orbit.{u_1, u_2} (↥(H.subgroupOf K)) b
⊢ x ∈ orbit.{u_1, u_2} (↥(H.subgroupOf K)) b ↔ x ∈ orbit.{u_1, u_2} (↥(Subgroup.map K.subtype (H.subgroupOf K))) b

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H K : Subgroup G
x b : α
h : x ∈ orbit.{u_1, u_2} (↥(H.subgroupOf K)) b
a :
  ∀ (gv : ↥K) (gp : gv ∈ H.subgroupOf K),
    (fun (m : ↥(H.subgroupOf K)) ↦ m • b) (Subtype.mk (p := fun (x : ↥K) ↦ x ∈ H.subgroupOf K) gv gp) ∈
      orbit.{u_1, u_2} (↥(Subgroup.map K.subtype (H.subgroupOf K))) b
⊢ x ∈ orbit.{u_1, u_2} (↥(Subgroup.map K.subtype (H.subgroupOf K))) b

Tactic:
rcases h with ⟨⟨gv, gp⟩, rfl⟩

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H K : Subgroup G
b : α
gv : ↥K
gp : gv ∈ H.subgroupOf K
⊢ Subtype.mk (p := fun (x : ↥K) ↦ x ∈ H.subgroupOf K) gv gp • b ∈
    orbit.{u_1, u_2} (↥(Subgroup.map K.subtype (H.subgroupOf K))) b

Tactic:
mem_orbit _ (⟨gv, ?_⟩ : Subgroup.map K.subtype (H.subgroupOf K))

Premises used: Set.Mem, Subtype.mk, MulAction.mem_orbit, Subtype.val
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H K : Subgroup G
b : α
gv : ↥K
gp : gv ∈ H.subgroupOf K
a : (↑gv : G) ∈ Subgroup.map K.subtype (H.subgroupOf K)
⊢ Subtype.mk (p := fun (x : ↥K) ↦ x ∈ H.subgroupOf K) gv gp • b ∈
    orbit.{u_1, u_2} (↥(Subgroup.map K.subtype (H.subgroupOf K))) b

Tactic:
refine mem_orbit _ (⟨gv, ?_⟩ : Subgroup.map K.subtype (H.subgroupOf K))

Premises used: Subtype.mk, MulAction.mem_orbit, Subtype.val
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H K : Subgroup G
b : α
gv : ↥K
gp : gv ∈ H.subgroupOf K
⊢ (↑gv : G) ∈ Subgroup.map K.subtype (H.subgroupOf K)

Tactic:
simpa using gp
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H K : Subgroup G
x b : α
h : x ∈ orbit.{u_1, u_2} (↥(Subgroup.map K.subtype (H.subgroupOf K))) b
a :
  ∀ (gv : G) (gp : gv ∈ Subgroup.map K.subtype (H.subgroupOf K)),
    (fun (m : ↥(Subgroup.map K.subtype (H.subgroupOf K))) ↦ m • b)
        (Subtype.mk (p := fun (x : G) ↦ x ∈ Subgroup.map K.subtype (H.subgroupOf K)) gv gp) ∈
      orbit.{u_1, u_2} (↥(H.subgroupOf K)) b
⊢ x ∈ orbit.{u_1, u_2} (↥(H.subgroupOf K)) b

Tactic:
rcases h with ⟨⟨gv, gp⟩, rfl⟩

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H K : Subgroup G
b : α
gv : G
gp : gv ∈ Subgroup.map K.subtype (H.subgroupOf K)
⊢ gv ∈ H ∧ gv ∈ K

Tactic:
simp only [Subgroup.subgroupOf_map_subtype, Subgroup.mem_inf] at gp

Premises used: Subgroup.subgroupOf_map_subtype, Subgroup.mem_inf
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H K : Subgroup G
b : α
gv : G
gp_1 : gv ∈ Subgroup.map K.subtype (H.subgroupOf K)
gp : gv ∈ H ∧ gv ∈ K
⊢ Subtype.mk (p := fun (x : G) ↦ x ∈ Subgroup.map K.subtype (H.subgroupOf K)) gv gp_1 • b ∈
    orbit.{u_1, u_2} (↥(H.subgroupOf K)) b

Tactic:
mem_orbit _ (⟨⟨gv, ?_⟩, ?_⟩ : H.subgroupOf K)

Premises used: Set.Mem, Subtype.mk, MulAction.mem_orbit
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H K : Subgroup G
b : α
gv : G
gp_1 : gv ∈ Subgroup.map K.subtype (H.subgroupOf K)
gp : gv ∈ H ∧ gv ∈ K
a : gv ∈ K
a₁ : Subtype.mk (p := fun (x : G) ↦ x ∈ K) gv ⋯ ∈ H.subgroupOf K
⊢ Subtype.mk (p := fun (x : G) ↦ x ∈ Subgroup.map K.subtype (H.subgroupOf K)) gv gp_1 • b ∈
    orbit.{u_1, u_2} (↥(H.subgroupOf K)) b

Tactic:
refine mem_orbit _ (⟨⟨gv, ?_⟩, ?_⟩ : H.subgroupOf K)

Premises used: Subtype.mk, MulAction.mem_orbit
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H K : Subgroup G
b : α
gv : G
gp_1 : gv ∈ Subgroup.map K.subtype (H.subgroupOf K)
gp : gv ∈ H ∧ gv ∈ K
⊢ gv ∈ K

Tactic:
gp.2

Premises used: And.right
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H K : Subgroup G
b : α
gv : G
gp_1 : gv ∈ Subgroup.map K.subtype (H.subgroupOf K)
gp : gv ∈ H ∧ gv ∈ K
⊢ gv ∈ K

Tactic:
exact gp.2

Premises used: And.right
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H K : Subgroup G
b : α
gv : G
gp_1 : gv ∈ Subgroup.map K.subtype (H.subgroupOf K)
gp : gv ∈ H ∧ gv ∈ K
a : gv ∈ H
⊢ Subtype.mk (p := fun (x : G) ↦ x ∈ K) gv ⋯ ∈ H.subgroupOf K

Tactic:
simp only [Subgroup.mem_subgroupOf]

Premises used: Subgroup.mem_subgroupOf
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H K : Subgroup G
b : α
gv : G
gp_1 : gv ∈ Subgroup.map K.subtype (H.subgroupOf K)
gp : gv ∈ H ∧ gv ∈ K
⊢ gv ∈ H

Tactic:
gp.1

Premises used: And.left
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H K : Subgroup G
b : α
gv : G
gp_1 : gv ∈ Subgroup.map K.subtype (H.subgroupOf K)
gp : gv ∈ H ∧ gv ∈ K
⊢ gv ∈ H

Tactic:
exact gp.1

Premises used: And.left
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
⊢ IsPretransitive G α ↔ Subsingleton.{u_2 + 1} (orbitRel.Quotient G α)

Tactic:
⟨fun _ ↦ ⟨fun a b ↦ ?_⟩, fun _ ↦ ⟨fun a b ↦ ?_⟩⟩

Premises used: MulAction.IsPretransitive.mk, Subsingleton.intro, Iff.intro
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
refine_1 : IsPretransitive G α → ∀ (a b : orbitRel.Quotient G α), a = b
refine_2 : Subsingleton.{u_2 + 1} (orbitRel.Quotient G α) → ∀ (a b : α), ∃ (g : G), g • a = b
⊢ IsPretransitive G α ↔ Subsingleton.{u_2 + 1} (orbitRel.Quotient G α)

Tactic:
refine ⟨fun _ ↦ ⟨fun a b ↦ ?_⟩, fun _ ↦ ⟨fun a b ↦ ?_⟩⟩
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
h : IsPretransitive G α
a b : orbitRel.Quotient G α
⊢ a = b

Tactic:
Quot.inductionOn a (fun x ↦ ?_)

Premises used: Quot.inductionOn
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
h : IsPretransitive G α
a b : orbitRel.Quotient G α
refine_1 : ∀ (x : α), Quot.mk (⇑(orbitRel G α) : α → α → Prop) x = b
⊢ a = b

Tactic:
refine Quot.inductionOn a (fun x ↦ ?_)
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
h : IsPretransitive G α
a b : orbitRel.Quotient G α
x : α
⊢ Quot.mk (⇑(orbitRel G α) : α → α → Prop) x = b

Tactic:
Quot.inductionOn b (fun y ↦ Quot.sound <| exists_smul_eq G y x)

Premises used: Quot.inductionOn
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
h : IsPretransitive G α
a b : orbitRel.Quotient G α
x : α
⊢ Quot.mk (⇑(orbitRel G α) : α → α → Prop) x = b

Tactic:
exact Quot.inductionOn b (fun y ↦ Quot.sound <| exists_smul_eq G y x)
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
h : Subsingleton.{u_2 + 1} (orbitRel.Quotient G α)
a b : α
⊢ ⟦b⟧ = ⟦a⟧

Tactic:
have h : Quotient.mk (orbitRel G α) b = ⟦a⟧ := Subsingleton.elim _ _
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
h_1 : Subsingleton.{u_2 + 1} (orbitRel.Quotient G α)
a b : α
h : ⟦b⟧ = ⟦a⟧
⊢ ∃ (g : G), g • a = b

Tactic:
Quotient.eq''.mp h

Premises used: Set.Mem, Quotient.eq'', setOf, MulAction.orbit, Iff.mp, Set.range
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
h_1 : Subsingleton.{u_2 + 1} (orbitRel.Quotient G α)
a b : α
h : ⟦b⟧ = ⟦a⟧
⊢ ∃ (g : G), g • a = b

Tactic:
exact Quotient.eq''.mp h

Premises used: Quotient.eq'', Iff.mp
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : Nonempty α
rw : Subsingleton.{u_2 + 1} (orbitRel.Quotient G α) → Nonempty.{u_2 + 1} (orbitRel.Quotient G α)
⊢ IsPretransitive G α ↔ Nonempty.{max 1 (u_2 + 1)} (Unique (orbitRel.Quotient G α))

Tactic:
rw [unique_iff_subsingleton_and_nonempty, pretransitive_iff_subsingleton_quotient, iff_self_and]

Premises used: iff_self_and, unique_iff_subsingleton_and_nonempty, MulAction.pretransitive_iff_subsingleton_quotient
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : Nonempty α
⊢ Subsingleton.{u_2 + 1} (orbitRel.Quotient G α) → Nonempty.{u_2 + 1} (orbitRel.Quotient G α)

Tactic:
fun _ ↦ (nonempty_quotient_iff _).mpr inferInstance

Premises used: Iff.mpr, inferInstance, MulAction.orbitRel, nonempty_quotient_iff
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : Nonempty α
⊢ Subsingleton.{u_2 + 1} (orbitRel.Quotient G α) → Nonempty.{u_2 + 1} (orbitRel.Quotient G α)

Tactic:
exact fun _ ↦ (nonempty_quotient_iff _).mpr inferInstance

Premises used: Iff.mpr, inferInstance, nonempty_quotient_iff
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MulAction G β
x : orbitRel.Quotient G α
h :
  ∀ (a : α) (x y : (↑(orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)) : Type u_2)), ∃ (g : G), g • x = y
⊢ ∀ (x_1 y : (↑x.orbit : Type u_2)), ∃ (g : G), g • x_1 = y

Tactic:
induction x using Quotient.inductionOn'
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MulAction G β
a y : α
yh : y ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)
z : α
zh : z ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)
h :
  ∀ (yh_1 : (orbitRel G α : α → α → Prop) y a) (z : α)
    (zh : z ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)) (zh_1 : (orbitRel G α : α → α → Prop) z a),
    ∃ (g : G),
      g • Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)) y yh =
        Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)) z zh
⊢ ∃ (g : G),
    g • Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)) y yh =
      Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)) z zh

Tactic:
rw [orbitRel.Quotient.mem_orbit, Quotient.eq''] at yh zh

Premises used: Quotient.eq'', MulAction.orbitRel.Quotient.mem_orbit
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MulAction G β
a y : α
yh_1 : y ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)
yh : (orbitRel G α : α → α → Prop) y a
z : α
zh_1 : z ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)
zh : (orbitRel G α : α → α → Prop) z a
h :
  ∀ (g : G) (yh : (fun (m : G) ↦ m • a) g ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)),
    ∃ (g_1 : G),
      g_1 •
          Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a))
            ((fun (m : G) ↦ m • a) g) yh =
        Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)) z zh_1
⊢ ∃ (g : G),
    g • Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)) y yh_1 =
      Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)) z zh_1

Tactic:
rcases yh with ⟨g, rfl⟩

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MulAction G β
a z : α
zh_1 : z ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)
zh : (orbitRel G α : α → α → Prop) z a
g : G
yh : (fun (m : G) ↦ m • a) g ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)
h :
  ∀ (h : G) (zh : (fun (m : G) ↦ m • a) h ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)),
    ∃ (g_1 : G),
      g_1 •
          Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a))
            ((fun (m : G) ↦ m • a) g) yh =
        Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a))
          ((fun (m : G) ↦ m • a) h) zh
⊢ ∃ (g_1 : G),
    g_1 •
        Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a))
          ((fun (m : G) ↦ m • a) g) yh =
      Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)) z zh_1

Tactic:
rcases zh with ⟨h, rfl⟩

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MulAction G β
a : α
g : G
yh : (fun (m : G) ↦ m • a) g ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)
h : G
zh : (fun (m : G) ↦ m • a) h ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)
⊢ ∃ (g_1 : G),
    g_1 •
        Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a))
          ((fun (m : G) ↦ m • a) g) yh =
      Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a))
        ((fun (m : G) ↦ m • a) h) zh

Tactic:
⟨h * g⁻¹, ?_⟩

Premises used: HMul.hMul, Inv.inv, Exists.intro
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MulAction G β
a : α
g : G
yh : (fun (m : G) ↦ m • a) g ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)
h : G
zh : (fun (m : G) ↦ m • a) h ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)
h₁ :
  (h * g⁻¹) •
      Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a))
        ((fun (m : G) ↦ m • a) g) yh =
    Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a))
      ((fun (m : G) ↦ m • a) h) zh
⊢ ∃ (g_1 : G),
    g_1 •
        Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a))
          ((fun (m : G) ↦ m • a) g) yh =
      Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a))
        ((fun (m : G) ↦ m • a) h) zh

Tactic:
refine ⟨h * g⁻¹, ?_⟩
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MulAction G β
a : α
g : G
yh : (fun (m : G) ↦ m • a) g ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)
h : G
zh : (fun (m : G) ↦ m • a) h ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)
h₁ :
  (↑((h * g⁻¹) •
          Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a))
            ((fun (m : G) ↦ m • a) g) yh) :
      α) =
    (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a))
          ((fun (m : G) ↦ m • a) h) zh) :
      α)
⊢ (h * g⁻¹) •
      Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a))
        ((fun (m : G) ↦ m • a) g) yh =
    Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a))
      ((fun (m : G) ↦ m • a) h) zh

Tactic:
ext