awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun (x : α) ↦ g • x) u = a
⊢ g⁻¹ • a ∈ U
have h : HSMul.hSMul (β := α) g⁻¹ ((fun (x : α) ↦ g • x) u) ∈ U
Tactic: rw [← hu₂]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun (x : α) ↦ g • x) u = a
⊢ HSMul.hSMul (β := α) g⁻¹ ((fun (x : α) ↦ g • x) u) ∈ U
have h : HSMul.hSMul (β := α) g⁻¹ ((fun (x : α) ↦ g • x) u) = u
Tactic: convert! hu₁
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
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
have 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
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⟩⟩, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
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
⊢ Disjoint (f '' U) (f '' V) ↔ ∀ x ∈ U, ∀ (g : G), g • x ∉ V
have refine_2 : (∀ x ∈ U, ∀ (g : G), g • x ∉ V) → Disjoint (f '' U) (f '' 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⟩⟩, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
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
⊢ Disjoint (f '' U) (f '' V)
have refine_2 : ∀ ⦃a : Quotient (orbitRel G α)⦄, a ∈ f '' U → a ∉ f '' V
Tactic: rw [Set.disjoint_left]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
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
⊢ False
have refine_2 : ∀ (g : G) (hc₁ : (fun (m : G) ↦ m • b) g ∈ V) (hc₂ : f ((fun (m : G) ↦ m • b) g) = a), False
Tactic: obtain ⟨g, rfl⟩ := Quotient.exact (hc₂.trans hb₂.symm)
Cleared hypotheses: c, hc₁, hc₂
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
a : α
x : Quotient G α
⊢ a ∈ x.orbit ↔ Quotient.mk'' a = x
have 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)
Tactic: induction x using Quotient.inductionOn'
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
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) ↔
    Eq (α := _root_.Quotient (orbitRel G α)) (Quotient.mk'' a) (Quotient.mk'' a_1)
have h : a ∈ orbit.{u_1, u_2} (G := G) (Quotient.mk'' a_1) ↔ (orbitRel G α : α → α → Prop) a a_1
Tactic: rw [Quotient.eq'']
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x : Quotient G α
φ : Quotient G α → α
hφ : RightInverse φ Quotient.mk'
| x.orbit
have rw : orbit.{u_1, u_2} (G := G) (Quotient.mk' (φ x))
Tactic: rw [← hφ x]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x : Quotient G α
φ : Quotient G α → α
hφ : RightInverse φ Quotient.mk'
⊢ x.orbit = MulAction.orbit G (φ x)
have conv_lhs : orbit.{u_1, u_2} (G := G) (Quotient.mk' (φ x)) = MulAction.orbit G (φ x)
Tactic: conv_lhs => rw [← hφ x]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (hypothesis)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x y : Quotient G α
h : x.orbit = y.orbit
⊢ x = y
have h₁ : (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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Subgroup G
a b : α
h : ⟦a⟧ = ⟦b⟧
⊢ ⟦a⟧ = ⟦b⟧
have rw : ∀ (h : (orbitRel (↥H) α : α → α → Prop) a b), (orbitRel G α : α → α → Prop) a b
Tactic: rw [@Quotient.eq] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x : Quotient G α
⊢ x.orbit.Nonempty
have rw : (MulAction.orbit G (Quotient.out x)).Nonempty
Tactic: rw [orbitRel.Quotient.orbit_eq_orbit_out x Quotient.out_eq']
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
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) x.orbit x.orbit
have rw : Set.MapsTo (fun (x : α) ↦ g • x) (MulAction.orbit G (Quotient.out x)) (MulAction.orbit G (Quotient.out x))
Tactic: rw [orbitRel.Quotient.orbit_eq_orbit_out x Quotient.out_eq']
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
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
have refine_1 : ∀ (h : (↑a : α) ∈ MulAction.orbit.{u_1, u_2} ↥H (↑b : α)), a ∈ MulAction.orbit.{u_1, u_2} (↥H) b
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
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
⊢ (↑a : α) ∈ MulAction.orbit.{u_1, u_2} ↥H (↑b : α) ↔ a ∈ MulAction.orbit.{u_1, u_2} (↥H) b
have refine_2 : ∀ (h : a ∈ MulAction.orbit.{u_1, u_2} (↥H) b), (↑a : α) ∈ MulAction.orbit.{u_1, u_2} ↥H (↑b : α)
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
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 : α)
⊢ a ∈ MulAction.orbit.{u_1, u_2} (↥H) b
have refine_1 : ∀ (g : ↥H) (h : (fun (m : ↥H) ↦ m • (↑b : α)) g = (↑a : α)), a ∈ MulAction.orbit.{u_1, u_2} (↥H) b
Tactic: rcases h with ⟨g, h⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (hypothesis)
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 : α)
⊢ a ∈ MulAction.orbit.{u_1, u_2} (↥H) b
have h₁ : (↑g : G) • b = a
Tactic: rw [subgroup_smul_def, ← orbit.coe_smul, ← Subtype.ext_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
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
⊢ a ∈ MulAction.orbit.{u_1, u_2} (↥H) b
have refine_1 : (↑g : G) • b ∈ MulAction.orbit.{u_1, u_2} (↥H) b
Tactic: subst h
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
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
⊢ (↑a : α) ∈ MulAction.orbit.{u_1, u_2} ↥H (↑b : α)
have refine_2 : ∀ (g : ↥H), (↑((fun (m : ↥H) ↦ m • b) g) : α) ∈ MulAction.orbit.{u_1, u_2} ↥H (↑b : α)
Tactic: rcases h with ⟨g, rfl⟩
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
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)
⊢ Eq (α := _root_.Quotient (α := (↑x.orbit : Type u_2)) (orbitRel.{u_1, u_2} ↥H (↑x.orbit : Type u_2))) ⟦a⟧ ⟦b⟧ ↔
    ⟦(↑a : α)⟧ = ⟦(↑b : α)⟧
have 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 : α)
Tactic: simp_rw [← @Quotient.mk''_eq_mk, Quotient.eq'']
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
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⟧
⊢ (↑a : α) ∈ MulAction.orbit.{u_1, u_2} (↥H) c ↔ (↑b : α) ∈ MulAction.orbit.{u_1, u_2} (↥H) c
have simp_rw : c ∈ MulAction.orbit.{u_1, u_2} ↥H (↑a : α) ↔ c ∈ MulAction.orbit.{u_1, u_2} ↥H (↑b : α)
Tactic: simp_rw [mem_orbit_symm (a₂ := c)]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
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 (↑b : α)
have h₁ : MulAction.orbit.{u_1, u_2} ↥H (↑b : α) = MulAction.orbit.{u_1, u_2} ↥H (↑a : α)
Tactic: convert! Iff.rfl using 2
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
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⟧
⊢ MulAction.orbit.{u_1, u_2} ↥H (↑b : α) = MulAction.orbit.{u_1, u_2} ↥H (↑a : α)
have h₁ : (↑b : α) ∈ MulAction.orbit.{u_1, u_2} ↥H (↑a : α)
Tactic: rw [orbit_eq_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (hypothesis)
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 (↑a : α)
have hb₁ : 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
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
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 (↑a : α)
have rw : b ∈ MulAction.orbit.{u_1, u_2} (↥H) a
Tactic: rw [orbitRel.Quotient.mem_subgroup_orbit_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
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) a
have 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⟧)
Tactic: convert! hb using 1
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
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⟧)
⊢ 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⟧)
have 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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
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⟧)
⊢ 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⟧)
have 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⟧)
Tactic: rw [orbit_eq_iff, ← orbitRel_apply, ← Quotient.eq'', Quotient.out_eq', @Quotient.mk''_eq_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
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⟧)
⊢ 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⟧)
have 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⟧))
Tactic: rw [orbit_eq_iff, ← orbitRel_apply, ← Quotient.eq'', Quotient.out_eq', @Quotient.mk''_eq_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
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⟧))
⊢ 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⟧)
have h₄ : Eq (α := _root_.Quotient (α := (↑x.orbit : Type u_2)) (orbitRel.{u_1, u_2} ↥H (↑x.orbit : Type u_2))) (Quotient.mk'' a)
  ⟦a⟧
Tactic: rw [orbit_eq_iff, ← orbitRel_apply, ← Quotient.eq'', Quotient.out_eq', @Quotient.mk''_eq_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
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⟧
⊢ 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⟧)
have h₅ : Eq (α := _root_.Quotient (α := (↑x.orbit : Type u_2)) (orbitRel.{u_1, u_2} ↥H (↑x.orbit : Type u_2))) ⟦a⟧ ⟦a⟧
Tactic: rw [orbit_eq_iff, ← orbitRel_apply, ← Quotient.eq'', Quotient.out_eq', @Quotient.mk''_eq_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
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⟧
⊢ (↑b : α) ∈ MulAction.orbit.{u_1, u_2} ↥H (↑a : α)
have h₁ : b ∈ orbit.{u_1, u_2} (G := ↥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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
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⟧
⊢ b ∈ orbit.{u_1, u_2} (G := ↥H) ⟦a⟧
have h₁ : Eq (α := _root_.Quotient (α := (↑x.orbit : Type u_2)) (orbitRel.{u_1, u_2} ↥H (↑x.orbit : Type u_2))) (Quotient.mk'' b)
  ⟦a⟧
Tactic: rw [orbitRel.Quotient.mem_orbit, h, @Quotient.mk''_eq_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
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⟧
⊢ b ∈ orbit.{u_1, u_2} (G := ↥H) ⟦a⟧
have h₂ : Eq (α := _root_.Quotient (α := (↑x.orbit : Type u_2)) (orbitRel.{u_1, u_2} ↥H (↑x.orbit : Type u_2))) (Quotient.mk'' b)
  ⟦b⟧
Tactic: rw [orbitRel.Quotient.mem_orbit, h, @Quotient.mk''_eq_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
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⟧
⊢ b ∈ orbit.{u_1, u_2} (G := ↥H) ⟦a⟧
have h₃ : Eq (α := _root_.Quotient (α := (↑x.orbit : Type u_2)) (orbitRel.{u_1, u_2} ↥H (↑x.orbit : Type u_2))) ⟦b⟧ ⟦b⟧
Tactic: rw [orbitRel.Quotient.mem_orbit, h, @Quotient.mk''_eq_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
⊢ Eq.{u_2 + 1} (α := Set α) Set.univ (⋃ (x : Ω), x.orbit)
have h : ∀ (x : α), Membership.mem (γ := Set α) Set.univ x ↔ Membership.mem (γ := Set α) (⋃ (x : Ω), x.orbit) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x : α
⊢ Membership.mem (γ := Set α) Set.univ x ↔ Membership.mem (γ := Set α) (⋃ (x : Ω), x.orbit) x
have h : ∃ (i : Ω), x ∈ i.orbit
Tactic: simp only [Set.mem_univ, Set.mem_iUnion, true_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MulAction G β
a : α
m : G
ha : m • a = a
⊢ m⁻¹ • a = a
have rw : a = m • a
Tactic: rw [inv_smul_eq_iff, ha]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MulAction G β
a : α
m : G
ha : m • a = a
rw : a = m • a
⊢ m⁻¹ • a = a
have rw₁ : a = a
Tactic: rw [inv_smul_eq_iff, ha]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MulAction G β
inst_3 : SMul α β
inst_4 : IsScalarTower G α β
a : α
b : β
⊢ LE.le (α := Subgroup G) (stabilizer G a) (stabilizer G (a • b))
have simp_rw : ∀ ⦃x : G⦄, x • a = a → (x • a) • b = a • b
Tactic: simp_rw [SetLike.le_def, mem_stabilizer_iff, ← smul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MulAction G β
inst_3 : SMul α β
inst_4 : IsScalarTower G α β
a_1 : α
b : β
a : G
h : a • a_1 = a_1
⊢ (a • a_1) • b = a_1 • b
have rw : a_1 • b = a_1 • b
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
Goal:
α : Type u_2
β : Type u_3
G' : Type u_4
inst : Group G'
inst_1 : SMul α β
inst_2 : MulAction G' β
inst_3 : SMulCommClass G' α β
a : α
b : β
⊢ LE.le (α := Subgroup G') (stabilizer G' b) (stabilizer G' (a • b))
have simp_rw : ∀ ⦃x : G'⦄, x • b = b → a • x • b = a • b
Tactic: simp_rw [SetLike.le_def, mem_stabilizer_iff, smul_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Defs (goal)
Goal:
α : Type u_2
β : Type u_3
G' : Type u_4
inst : Group G'
inst_1 : SMul α β
inst_2 : MulAction G' β
inst_3 : SMulCommClass G' α β
a_1 : α
b : β
a : G'
h : a • b = b
⊢ a_1 • a • b = a_1 • b
have rw : a_1 • b = a_1 • b
Tactic: rw [h]