awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
U V : Set α
this : Setoid α := orbitRel G α
set :
  let f : α → Quotient (orbitRel G α) := Quotient.mk';
  Disjoint (f '' U) (f '' V) ↔ ∀ x ∈ U, ∀ (g : G), g • x ∉ V
⊢ Disjoint (α := Set (Quotient (orbitRel G α))) (Quotient.mk' '' U) (Quotient.mk' '' V) ↔ ∀ x ∈ U, ∀ (g : G), g • x ∉ V

Tactic:
set f : α → Quotient (MulAction.orbitRel G α) := Quotient.mk'

Premises used: Quotient.mk'
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
U V : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
⊢ Disjoint (f '' U) (f '' V) ↔ ∀ x ∈ U, ∀ (g : G), g • x ∉ V

Tactic:
⟨fun h a a_in_U g g_in_V =>
      h.le_bot ⟨⟨a, a_in_U, Quotient.sound ⟨g⁻¹, ?_⟩⟩, ⟨g • a, g_in_V, rfl⟩⟩, ?_⟩

Premises used: Disjoint.le_bot, Inv.inv, And.intro, Iff.intro, Exists.intro, HSMul.hSMul, Quotient.sound, rfl
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
U V : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
refine_1 :
  ∀ (h : Disjoint (f '' U) (f '' V)) (a : α) (a_in_U : a ∈ U) (g : G) (g_in_V : g • a ∈ V),
    (fun (m : G) ↦ m • g • a) g⁻¹ = a
refine_2 : (∀ x ∈ U, ∀ (g : G), g • x ∉ V) → Disjoint (f '' U) (f '' V)
⊢ Disjoint (f '' U) (f '' V) ↔ ∀ x ∈ U, ∀ (g : G), g • x ∉ V

Tactic:
refine
    ⟨fun h a a_in_U g g_in_V =>
      h.le_bot ⟨⟨a, a_in_U, Quotient.sound ⟨g⁻¹, ?_⟩⟩, ⟨g • a, g_in_V, rfl⟩⟩, ?_⟩
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
U V : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
h : Disjoint (f '' U) (f '' V)
a : α
a_in_U : a ∈ U
g : G
g_in_V : g • a ∈ V
⊢ (fun (m : G) ↦ m • g • a) g⁻¹ = a

Tactic:
simp
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
U V : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
h : ∀ x ∈ U, ∀ (g : G), g • x ∉ V
refine_2 : ∀ ⦃a : Quotient (orbitRel G α)⦄, a ∈ f '' U → a ∉ f '' V
⊢ Disjoint (f '' U) (f '' V)

Tactic:
rw [Set.disjoint_left]

Premises used: Set.disjoint_left
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
U V : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
h : ∀ x ∈ U, ∀ (g : G), g • x ∉ V
a : Quotient (orbitRel G α)
b : α
hb₁ : b ∈ U
hb₂ : f b = a
c : α
hc₁ : c ∈ V
hc₂ : f c = a
refine_2 : ∀ (g : G) (hc₁ : (fun (m : G) ↦ m • b) g ∈ V) (hc₂ : f ((fun (m : G) ↦ m • b) g) = a), False
⊢ False

Tactic:
obtain ⟨g, rfl⟩ := Quotient.exact (hc₂.trans hb₂.symm)

Premises used: Quotient.exact, Eq.symm, rfl, Eq.trans
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
U V : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
h : ∀ x ∈ U, ∀ (g : G), g • x ∉ V
a : Quotient (orbitRel G α)
b : α
hb₁ : b ∈ U
hb₂ : f b = a
g : G
hc₁ : (fun (m : G) ↦ m • b) g ∈ V
hc₂ : f ((fun (m : G) ↦ m • b) g) = a
⊢ False

Tactic:
h b hb₁ g hc₁
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
U V : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
h : ∀ x ∈ U, ∀ (g : G), g • x ∉ V
a : Quotient (orbitRel G α)
b : α
hb₁ : b ∈ U
hb₂ : f b = a
g : G
hc₁ : (fun (m : G) ↦ m • b) g ∈ V
hc₂ : f ((fun (m : G) ↦ m • b) g) = a
⊢ False

Tactic:
exact h b hb₁ g hc₁
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
U V : Set α
⊢ Eq (α := Set (Quotient (orbitRel G α))) (Quotient.mk' '' U ∩ Quotient.mk' '' V) ∅ ↔ ∀ x ∈ U, ∀ (g : G), g • x ∉ V

Tactic:
Set.disjoint_iff_inter_eq_empty.symm.trans disjoint_image_image_iff

Premises used: MulAction.disjoint_image_image_iff, Set.disjoint_iff_inter_eq_empty, Iff.trans, Iff.symm
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
a : α
⊢ orbit.{u_1, u_2} (G := G) (Quotient.mk'' a) = MulAction.orbit G a

Tactic:
rfl

Premises used: MulAction.orbitRel.Quotient.orbit, MulAction.orbit, Set.range, rfl
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
a : α
x : Quotient G α
h :
  ∀ (a_1 : α),
    a ∈ orbit.{u_1, u_2} (G := G) (Quotient.mk'' a_1) ↔
      Eq (α := _root_.Quotient (orbitRel G α)) (Quotient.mk'' a) (Quotient.mk'' a_1)
⊢ a ∈ x.orbit ↔ Quotient.mk'' a = x

Tactic:
induction x using Quotient.inductionOn'
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
a a_1 : α
h : a ∈ orbit.{u_1, u_2} (G := G) (Quotient.mk'' a_1) ↔ (orbitRel G α : α → α → Prop) a a_1
⊢ a ∈ orbit.{u_1, u_2} (G := G) (Quotient.mk'' a_1) ↔
    Eq (α := _root_.Quotient (orbitRel G α)) (Quotient.mk'' a) (Quotient.mk'' a_1)

Tactic:
rw [Quotient.eq'']

Premises used: Quotient.eq''
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
a a_1 : α
⊢ a ∈ orbit.{u_1, u_2} (G := G) (Quotient.mk'' a_1) ↔ (orbitRel G α : α → α → Prop) a a_1

Tactic:
rfl
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x : Quotient G α
φ : Quotient G α → α
hφ : RightInverse φ Quotient.mk'
rw : orbit.{u_1, u_2} (G := G) (Quotient.mk' (φ x))
| x.orbit

Tactic:
rw [← hφ x]
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x : Quotient G α
φ : Quotient G α → α
hφ : RightInverse φ Quotient.mk'
conv_lhs : orbit.{u_1, u_2} (G := G) (Quotient.mk' (φ x)) = MulAction.orbit G (φ x)
⊢ x.orbit = MulAction.orbit G (φ x)

Tactic:
conv_lhs => rw [← hφ x]
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x : Quotient G α
φ : Quotient G α → α
hφ : RightInverse φ Quotient.mk'
⊢ orbit.{u_1, u_2} (G := G) (Quotient.mk' (φ x)) = MulAction.orbit G (φ x)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x y : Quotient G α
h : x.orbit = y.orbit
⊢ (orbitRel G α : α → α → Prop) (Quotient.out x) (Quotient.out y)

Tactic:
simp_rw [orbitRel.Quotient.orbit_eq_orbit_out _ Quotient.out_eq', orbit_eq_iff,
    ← orbitRel_apply] at h

Premises used: Quotient.out_eq', MulAction.orbitRel_apply, MulAction.orbit_eq_iff, MulAction.orbitRel.Quotient.orbit_eq_orbit_out
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x y : Quotient G α
h : (orbitRel G α : α → α → Prop) (Quotient.out x) (Quotient.out y)
⊢ x = y

Tactic:
simpa [← Quotient.eq''] using h

Premises used: Quotient.eq''
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x y : Quotient G α
⊢ x.orbit = y.orbit ↔ x = y

Tactic:
orbitRel.Quotient.orbit_injective.eq_iff

Premises used: Function.Injective.eq_iff, MulAction.orbitRel.Quotient.orbit_injective
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Subgroup G
a b : α
h : ⟦a⟧ = ⟦b⟧
rw : ∀ (h : (orbitRel (↥H) α : α → α → Prop) a b), (orbitRel G α : α → α → Prop) a b
⊢ ⟦a⟧ = ⟦b⟧

Tactic:
rw [@Quotient.eq] at h ⊢

Premises used: Quotient.eq
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Subgroup G
a b : α
h : (orbitRel (↥H) α : α → α → Prop) a b
⊢ (orbitRel G α : α → α → Prop) a b

Tactic:
mem_orbit_of_mem_orbit_subgroup h

Premises used: MulAction.mem_orbit_of_mem_orbit_subgroup
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Subgroup G
a b : α
h : (orbitRel (↥H) α : α → α → Prop) a b
⊢ (orbitRel G α : α → α → Prop) a b

Tactic:
exact mem_orbit_of_mem_orbit_subgroup h

Premises used: MulAction.mem_orbit_of_mem_orbit_subgroup
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Subgroup G
a b : α
h : Eq (α := _root_.Quotient (orbitRel.{u_1, u_2} (↥H) α)) (Quotient.mk'' a) (Quotient.mk'' b)
⊢ Eq (α := _root_.Quotient (orbitRel G α)) (Quotient.mk'' a) (Quotient.mk'' b)

Tactic:
orbitRel.quotient_eq_of_quotient_subgroup_eq h

Premises used: MulAction.orbitRel.quotient_eq_of_quotient_subgroup_eq
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x : Quotient G α
rw : (MulAction.orbit G (Quotient.out x)).Nonempty
⊢ x.orbit.Nonempty

Tactic:
rw [orbitRel.Quotient.orbit_eq_orbit_out x Quotient.out_eq']

Premises used: Quotient.out_eq', MulAction.orbitRel.Quotient.orbit_eq_orbit_out
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x : Quotient G α
⊢ (MulAction.orbit G (Quotient.out x)).Nonempty

Tactic:
nonempty_orbit _

Premises used: MulAction.nonempty_orbit
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x : Quotient G α
⊢ (MulAction.orbit G (Quotient.out x)).Nonempty

Tactic:
exact nonempty_orbit _

Premises used: MulAction.orbitRel.Quotient.nonempty_orbit
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
g : G
x : Quotient G α
rw : Set.MapsTo (fun (x : α) ↦ g • x) (MulAction.orbit G (Quotient.out x)) (MulAction.orbit G (Quotient.out x))
⊢ Set.MapsTo (fun (x : α) ↦ g • x) x.orbit x.orbit

Tactic:
rw [orbitRel.Quotient.orbit_eq_orbit_out x Quotient.out_eq']

Premises used: Quotient.out_eq', MulAction.orbitRel.Quotient.orbit_eq_orbit_out
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
g : G
x : Quotient G α
⊢ Set.MapsTo (fun (x : α) ↦ g • x) (MulAction.orbit G (Quotient.out x)) (MulAction.orbit G (Quotient.out x))

Tactic:
mapsTo_smul_orbit g x.out

Premises used: Quotient.out, MulAction.mapsTo_smul_orbit
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
g : G
x : Quotient G α
⊢ Set.MapsTo (fun (x : α) ↦ g • x) (MulAction.orbit G (Quotient.out x)) (MulAction.orbit G (Quotient.out x))

Tactic:
exact mapsTo_smul_orbit g x.out
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
g : G
x : Quotient G α
a : (↑x.orbit : Type u_2)
⊢ (↑(g • a) : α) = g • (↑a : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Subgroup G
x : Quotient G α
a b : (↑x.orbit : Type u_2)
⊢ (↑a : α) ∈ MulAction.orbit.{u_1, u_2} ↥H (↑b : α) ↔ a ∈ MulAction.orbit.{u_1, u_2} (↥H) b

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

Premises used: Iff.intro
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Subgroup G
x : Quotient G α
a b : (↑x.orbit : Type u_2)
refine_1 : ∀ (h : (↑a : α) ∈ MulAction.orbit.{u_1, u_2} ↥H (↑b : α)), a ∈ MulAction.orbit.{u_1, u_2} (↥H) b
refine_2 : ∀ (h : a ∈ MulAction.orbit.{u_1, u_2} (↥H) b), (↑a : α) ∈ MulAction.orbit.{u_1, u_2} ↥H (↑b : α)
⊢ (↑a : α) ∈ MulAction.orbit.{u_1, u_2} ↥H (↑b : α) ↔ a ∈ MulAction.orbit.{u_1, u_2} (↥H) b

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Subgroup G
x : Quotient G α
a b : (↑x.orbit : Type u_2)
h : (↑a : α) ∈ MulAction.orbit.{u_1, u_2} ↥H (↑b : α)
refine_1 : ∀ (g : ↥H) (h : (fun (m : ↥H) ↦ m • (↑b : α)) g = (↑a : α)), a ∈ MulAction.orbit.{u_1, u_2} (↥H) b
⊢ a ∈ MulAction.orbit.{u_1, u_2} (↥H) b

Tactic:
rcases h with ⟨g, h⟩
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Subgroup G
x : Quotient G α
a b : (↑x.orbit : Type u_2)
g : ↥H
h : g • (↑b : α) = (↑a : α)
⊢ (↑g : G) • b = a

Tactic:
rw [subgroup_smul_def, ← orbit.coe_smul, ← Subtype.ext_iff] at h

Premises used: MulAction.orbitRel.Quotient.orbit.coe_smul, Subtype.ext_iff, MulAction.subgroup_smul_def
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Subgroup G
x : Quotient G α
a b : (↑x.orbit : Type u_2)
g : ↥H
h : (↑g : G) • b = a
refine_1 : (↑g : G) • b ∈ MulAction.orbit.{u_1, u_2} (↥H) b
⊢ a ∈ MulAction.orbit.{u_1, u_2} (↥H) b

Tactic:
subst h
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Subgroup G
x : Quotient G α
b : (↑x.orbit : Type u_2)
g : ↥H
⊢ (↑g : G) • b ∈ MulAction.orbit.{u_1, u_2} (↥H) b

Tactic:
MulAction.mem_orbit _ g

Premises used: Set.Mem, MulAction.mem_orbit
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Subgroup G
x : Quotient G α
b : (↑x.orbit : Type u_2)
g : ↥H
⊢ (↑g : G) • b ∈ MulAction.orbit.{u_1, u_2} (↥H) b

Tactic:
exact MulAction.mem_orbit _ g

Premises used: MulAction.mem_orbit
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Subgroup G
x : Quotient G α
a b : (↑x.orbit : Type u_2)
h : a ∈ MulAction.orbit.{u_1, u_2} (↥H) b
refine_2 : ∀ (g : ↥H), (↑((fun (m : ↥H) ↦ m • b) g) : α) ∈ MulAction.orbit.{u_1, u_2} ↥H (↑b : α)
⊢ (↑a : α) ∈ MulAction.orbit.{u_1, u_2} ↥H (↑b : α)

Tactic:
rcases h with ⟨g, rfl⟩

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Subgroup G
x : Quotient G α
b : (↑x.orbit : Type u_2)
g : ↥H
⊢ (↑((fun (m : ↥H) ↦ m • b) g) : α) ∈ MulAction.orbit.{u_1, u_2} ↥H (↑b : α)

Tactic:
MulAction.mem_orbit _ g

Premises used: Set.Mem, MulAction.mem_orbit
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Subgroup G
x : Quotient G α
b : (↑x.orbit : Type u_2)
g : ↥H
⊢ (↑((fun (m : ↥H) ↦ m • b) g) : α) ∈ MulAction.orbit.{u_1, u_2} ↥H (↑b : α)

Tactic:
exact MulAction.mem_orbit _ g

Premises used: MulAction.mem_orbit
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Subgroup G
x : Quotient G α
a b : (↑x.orbit : Type u_2)
simp_rw :
  (orbitRel ↥H (↑x.orbit : Type u_2) : (↑x.orbit : Type u_2) → (↑x.orbit : Type u_2) → Prop) a b ↔
    (orbitRel (↥H) α : α → α → Prop) (↑a : α) (↑b : α)
⊢ Eq (α := _root_.Quotient (α := (↑x.orbit : Type u_2)) (orbitRel.{u_1, u_2} ↥H (↑x.orbit : Type u_2))) ⟦a⟧ ⟦b⟧ ↔
    ⟦(↑a : α)⟧ = ⟦(↑b : α)⟧

Tactic:
simp_rw [← @Quotient.mk''_eq_mk, Quotient.eq'']

Premises used: Quotient.eq'', Quotient.mk''_eq_mk
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Subgroup G
x : Quotient G α
a b : (↑x.orbit : Type u_2)
⊢ (orbitRel ↥H (↑x.orbit : Type u_2) : (↑x.orbit : Type u_2) → (↑x.orbit : Type u_2) → Prop) a b ↔
    (orbitRel (↥H) α : α → α → Prop) (↑a : α) (↑b : α)

Tactic:
orbitRel.Quotient.mem_subgroup_orbit_iff.symm

Premises used: MulAction.orbitRel.Quotient.mem_subgroup_orbit_iff, Iff.symm
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Subgroup G
x : Quotient G α
a b : (↑x.orbit : Type u_2)
⊢ (orbitRel ↥H (↑x.orbit : Type u_2) : (↑x.orbit : Type u_2) → (↑x.orbit : Type u_2) → Prop) a b ↔
    (orbitRel (↥H) α : α → α → Prop) (↑a : α) (↑b : α)

Tactic:
exact orbitRel.Quotient.mem_subgroup_orbit_iff.symm

Premises used: MulAction.orbitRel.Quotient.mem_subgroup_orbit_iff, Iff.symm
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Subgroup G
x : Quotient G α
a b : (↑x.orbit : Type u_2)
c : α
h : Eq (α := _root_.Quotient (α := (↑x.orbit : Type u_2)) (orbitRel.{u_1, u_2} ↥H (↑x.orbit : Type u_2))) ⟦a⟧ ⟦b⟧
simp_rw : c ∈ MulAction.orbit.{u_1, u_2} ↥H (↑a : α) ↔ c ∈ MulAction.orbit.{u_1, u_2} ↥H (↑b : α)
⊢ (↑a : α) ∈ MulAction.orbit.{u_1, u_2} (↥H) c ↔ (↑b : α) ∈ MulAction.orbit.{u_1, u_2} (↥H) c

Tactic:
simp_rw [mem_orbit_symm (a₂ := c)]

Premises used: MulAction.mem_orbit_symm
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Subgroup G
x : Quotient G α
a b : (↑x.orbit : Type u_2)
c : α
h : Eq (α := _root_.Quotient (α := (↑x.orbit : Type u_2)) (orbitRel.{u_1, u_2} ↥H (↑x.orbit : Type u_2))) ⟦a⟧ ⟦b⟧
⊢ c ∈ MulAction.orbit.{u_1, u_2} ↥H (↑a : α) ↔ c ∈ MulAction.orbit.{u_1, u_2} ↥H (↑a : α)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Subgroup G
x : Quotient G α
a b : (↑x.orbit : Type u_2)
c : α
h : Eq (α := _root_.Quotient (α := (↑x.orbit : Type u_2)) (orbitRel.{u_1, u_2} ↥H (↑x.orbit : Type u_2))) ⟦a⟧ ⟦b⟧
h₁ : MulAction.orbit.{u_1, u_2} ↥H (↑b : α) = MulAction.orbit.{u_1, u_2} ↥H (↑a : α)
⊢ c ∈ MulAction.orbit.{u_1, u_2} ↥H (↑a : α) ↔ c ∈ MulAction.orbit.{u_1, u_2} ↥H (↑b : α)

Tactic:
convert! Iff.rfl using 2

Premises used: Iff.rfl
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Subgroup G
x : Quotient G α
a b : (↑x.orbit : Type u_2)
c : α
h : Eq (α := _root_.Quotient (α := (↑x.orbit : Type u_2)) (orbitRel.{u_1, u_2} ↥H (↑x.orbit : Type u_2))) ⟦a⟧ ⟦b⟧
h₁ : (↑b : α) ∈ MulAction.orbit.{u_1, u_2} ↥H (↑a : α)
⊢ MulAction.orbit.{u_1, u_2} ↥H (↑b : α) = MulAction.orbit.{u_1, u_2} ↥H (↑a : α)

Tactic:
rw [orbit_eq_iff]

Premises used: MulAction.orbit_eq_iff
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Subgroup G
x : Quotient G α
a b : (↑x.orbit : Type u_2)
c : α
h : Eq (α := _root_.Quotient (α := (↑x.orbit : Type u_2)) (orbitRel.{u_1, u_2} ↥H (↑x.orbit : Type u_2))) ⟦a⟧ ⟦b⟧
hb : b ∈ orbit.{u_1, u_2} (G := ↥H) ⟦a⟧
⊢ b ∈ MulAction.orbit.{u_1, u_2} (↥H) (Quotient.out (s := orbitRel.{u_1, u_2} ↥H (↑x.orbit : Type u_2)) ⟦a⟧)

Tactic:
rw [orbitRel.Quotient.orbit_eq_orbit_out (⟦a⟧ : orbitRel.Quotient H x.orbit) Quotient.out_eq']
       at hb

Premises used: Quotient.out_eq', Quotient.mk, MulAction.orbitRel.Quotient.orbit_eq_orbit_out
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Subgroup G
x : Quotient G α
a b : (↑x.orbit : Type u_2)
c : α
h : Eq (α := _root_.Quotient (α := (↑x.orbit : Type u_2)) (orbitRel.{u_1, u_2} ↥H (↑x.orbit : Type u_2))) ⟦a⟧ ⟦b⟧
hb : b ∈ MulAction.orbit.{u_1, u_2} (↥H) (Quotient.out (s := orbitRel.{u_1, u_2} ↥H (↑x.orbit : Type u_2)) ⟦a⟧)
rw : b ∈ MulAction.orbit.{u_1, u_2} (↥H) a
⊢ (↑b : α) ∈ MulAction.orbit.{u_1, u_2} ↥H (↑a : α)

Tactic:
rw [orbitRel.Quotient.mem_subgroup_orbit_iff]

Premises used: MulAction.orbitRel.Quotient.mem_subgroup_orbit_iff
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Subgroup G
x : Quotient G α
a b : (↑x.orbit : Type u_2)
c : α
h : Eq (α := _root_.Quotient (α := (↑x.orbit : Type u_2)) (orbitRel.{u_1, u_2} ↥H (↑x.orbit : Type u_2))) ⟦a⟧ ⟦b⟧
hb : b ∈ MulAction.orbit.{u_1, u_2} (↥H) (Quotient.out (s := orbitRel.{u_1, u_2} ↥H (↑x.orbit : Type u_2)) ⟦a⟧)
⊢ b ∈ MulAction.orbit.{u_1, u_2} (↥H) (Quotient.out (s := orbitRel.{u_1, u_2} ↥H (↑x.orbit : Type u_2)) ⟦a⟧)

Tactic:
hb
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Subgroup G
x : Quotient G α
a b : (↑x.orbit : Type u_2)
c : α
h : Eq (α := _root_.Quotient (α := (↑x.orbit : Type u_2)) (orbitRel.{u_1, u_2} ↥H (↑x.orbit : Type u_2))) ⟦a⟧ ⟦b⟧
hb : b ∈ MulAction.orbit.{u_1, u_2} (↥H) (Quotient.out (s := orbitRel.{u_1, u_2} ↥H (↑x.orbit : Type u_2)) ⟦a⟧)
h₁ :
  MulAction.orbit.{u_1, u_2} (↥H) a =
    MulAction.orbit.{u_1, u_2} (↥H) (Quotient.out (s := orbitRel.{u_1, u_2} ↥H (↑x.orbit : Type u_2)) ⟦a⟧)
⊢ b ∈ MulAction.orbit.{u_1, u_2} (↥H) a

Tactic:
convert! hb using 1
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Subgroup G
x : Quotient G α
a b : (↑x.orbit : Type u_2)
c : α
h : Eq (α := _root_.Quotient (α := (↑x.orbit : Type u_2)) (orbitRel.{u_1, u_2} ↥H (↑x.orbit : Type u_2))) ⟦a⟧ ⟦b⟧
hb : b ∈ MulAction.orbit.{u_1, u_2} (↥H) (Quotient.out (s := orbitRel.{u_1, u_2} ↥H (↑x.orbit : Type u_2)) ⟦a⟧)
h₁ : a ∈ MulAction.orbit.{u_1, u_2} (↥H) (Quotient.out (s := orbitRel.{u_1, u_2} ↥H (↑x.orbit : Type u_2)) ⟦a⟧)
h₂ :
  (orbitRel ↥H (↑x.orbit : Type u_2) : (↑x.orbit : Type u_2) → (↑x.orbit : Type u_2) → Prop) a
    (Quotient.out (s := orbitRel.{u_1, u_2} ↥H (↑x.orbit : Type u_2)) ⟦a⟧)
h₃ :
  Eq (α := _root_.Quotient (α := (↑x.orbit : Type u_2)) (orbitRel.{u_1, u_2} ↥H (↑x.orbit : Type u_2)))
    (Quotient.mk'' a) (Quotient.mk'' (Quotient.out (s := orbitRel.{u_1, u_2} ↥H (↑x.orbit : Type u_2)) ⟦a⟧))
h₄ :
  Eq (α := _root_.Quotient (α := (↑x.orbit : Type u_2)) (orbitRel.{u_1, u_2} ↥H (↑x.orbit : Type u_2)))
    (Quotient.mk'' a) ⟦a⟧
h₅ h₆ : Eq (α := _root_.Quotient (α := (↑x.orbit : Type u_2)) (orbitRel.{u_1, u_2} ↥H (↑x.orbit : Type u_2))) ⟦a⟧ ⟦a⟧
⊢ MulAction.orbit.{u_1, u_2} (↥H) a =
    MulAction.orbit.{u_1, u_2} (↥H) (Quotient.out (s := orbitRel.{u_1, u_2} ↥H (↑x.orbit : Type u_2)) ⟦a⟧)

Tactic:
rw [orbit_eq_iff, ← orbitRel_apply, ← Quotient.eq'', Quotient.out_eq', @Quotient.mk''_eq_mk]

Premises used: Quotient.out_eq', Quotient.eq'', MulAction.orbitRel_apply, MulAction.orbit_eq_iff, Quotient.mk''_eq_mk
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Subgroup G
x : Quotient G α
a b : (↑x.orbit : Type u_2)
c : α
h : Eq (α := _root_.Quotient (α := (↑x.orbit : Type u_2)) (orbitRel.{u_1, u_2} ↥H (↑x.orbit : Type u_2))) ⟦a⟧ ⟦b⟧
h₁ : b ∈ orbit.{u_1, u_2} (G := ↥H) ⟦a⟧
⊢ (↑b : α) ∈ MulAction.orbit.{u_1, u_2} ↥H (↑a : α)

Tactic:
suffices hb : ↑b ∈ orbitRel.Quotient.orbit (⟦a⟧ : orbitRel.Quotient H x.orbit) by
    rw [orbitRel.Quotient.orbit_eq_orbit_out (⟦a⟧ : orbitRel.Quotient H x.orbit) Quotient.out_eq']
       at hb
    rw [orbitRel.Quotient.mem_subgroup_orbit_iff]
    convert! hb using 1
    rw [orbit_eq_iff, ← orbitRel_apply, ← Quotient.eq'', Quotient.out_eq', @Quotient.mk''_eq_mk]
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Subgroup G
x : Quotient G α
a b : (↑x.orbit : Type u_2)
c : α
h : Eq (α := _root_.Quotient (α := (↑x.orbit : Type u_2)) (orbitRel.{u_1, u_2} ↥H (↑x.orbit : Type u_2))) ⟦a⟧ ⟦b⟧
h₁ :
  Eq (α := _root_.Quotient (α := (↑x.orbit : Type u_2)) (orbitRel.{u_1, u_2} ↥H (↑x.orbit : Type u_2)))
    (Quotient.mk'' b) ⟦a⟧
h₂ :
  Eq (α := _root_.Quotient (α := (↑x.orbit : Type u_2)) (orbitRel.{u_1, u_2} ↥H (↑x.orbit : Type u_2)))
    (Quotient.mk'' b) ⟦b⟧
h₃ h₄ : Eq (α := _root_.Quotient (α := (↑x.orbit : Type u_2)) (orbitRel.{u_1, u_2} ↥H (↑x.orbit : Type u_2))) ⟦b⟧ ⟦b⟧
⊢ b ∈ orbit.{u_1, u_2} (G := ↥H) ⟦a⟧

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

Premises used: MulAction.orbitRel.Quotient.mem_orbit, Quotient.mk''_eq_mk
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
h : ∀ (x : α), Membership.mem (γ := Set α) Set.univ x ↔ Membership.mem (γ := Set α) (⋃ (x : Ω), x.orbit) x
⊢ Eq.{u_2 + 1} (α := Set α) Set.univ (⋃ (x : Ω), x.orbit)

Tactic:
ext x