awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
α : Type u_1
M : Type u_2
G : Type u_3
inst : Monoid M
x : Mˣ
u : ↥(MulAction.stabilizer (ConjAct Mˣ) x)
this : (↑u : ConjAct Mˣ) • x = x
rwa :
  ∀
    (this :
      HMul.hMul (β := Mˣ) (HMul.hMul (α := Mˣ) ((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ) : Mˣ) x)
          (((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ))⁻¹ : Mˣ) =
        x),
    (↑x : M) * (↑((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ)) : M) =
      (↑((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ)) : M) * (↑x : M)
rwa₁ :
  ∀
    (this :
      HMul.hMul (α := Mˣ) ((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ) : Mˣ) x =
        HMul.hMul (β := Mˣ) x ((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ) : Mˣ)),
    (↑x : M) * (↑((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ)) : M) =
      (↑((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ)) : M) * (↑x : M)
rwa₂ :
  ∀
    (this :
      (↑(HMul.hMul (α := Mˣ) ((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ) : Mˣ) x) : M) =
        (↑(HMul.hMul (β := Mˣ) x ((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ) : Mˣ)) : M)),
    (↑x : M) * (↑((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ)) : M) =
      (↑((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ)) : M) * (↑x : M)
rwa₃ rwa₄ rwa₅ rwa₆ :
  ∀
    (this :
      (↑(HMul.hMul (β := Mˣ) x ((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ) : Mˣ)) : M) =
        (↑(HMul.hMul (α := Mˣ) ((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ) : Mˣ) x) : M)),
    (↑x : M) * (↑((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ)) : M) =
      (↑((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ)) : M) * (↑x : M)
⊢ (↑x : M) * (↑((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ)) : M) =
    (↑((ConjAct.ofConjAct : (a : ConjAct Mˣ) → Mˣ) (↑u : ConjAct Mˣ)) : M) * (↑x : M)

Tactic:
rwa [ConjAct.smul_def, mul_inv_eq_iff_eq_mul, Units.ext_iff, eq_comm] at this

Premises used: ConjAct.smul_def, Units.ext_iff, eq_comm, mul_inv_eq_iff_eq_mul
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
α : Type u_1
M : Type u_2
G : Type u_3
inst : Monoid M
x : Mˣ
u : (↥(Submonoid.centralizer {(↑x : M)}))ˣ
simp :
  HMul.hMul (α := Mˣ)
      ((Units.map (Submonoid.subtype (Submonoid.centralizer {(↑x : M)})) :
            (a : (↥(Submonoid.centralizer {(↑x : M)}))ˣ) → Mˣ)
          u :
        Mˣ)
      x =
    HMul.hMul (β := Mˣ) x
      ((Units.map (Submonoid.subtype (Submonoid.centralizer {(↑x : M)})) :
            (a : (↥(Submonoid.centralizer {(↑x : M)}))ˣ) → Mˣ)
          u :
        Mˣ)
⊢ HSMul.hSMul (α := ConjAct Mˣ)
      ((ConjAct.toConjAct : (a : Mˣ) → ConjAct Mˣ)
          ((Units.map (Submonoid.subtype (Submonoid.centralizer {(↑x : M)})) :
              (a : (↥(Submonoid.centralizer {(↑x : M)}))ˣ) → Mˣ)
            u) :
        ConjAct Mˣ)
      x =
    x

Tactic:
simp only [ConjAct.smul_def, ConjAct.ofConjAct_toConjAct, mul_inv_eq_iff_eq_mul]

Premises used: ConjAct.smul_def, ConjAct.ofConjAct_toConjAct, mul_inv_eq_iff_eq_mul
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
α : Type u_1
M : Type u_2
G : Type u_3
inst : Monoid M
x : Mˣ
u : (↥(Submonoid.centralizer {(↑x : M)}))ˣ
⊢ HMul.hMul (α := Mˣ)
      ((Units.map (Submonoid.subtype (Submonoid.centralizer {(↑x : M)})) :
            (a : (↥(Submonoid.centralizer {(↑x : M)}))ˣ) → Mˣ)
          u :
        Mˣ)
      x =
    HMul.hMul (β := Mˣ) x
      ((Units.map (Submonoid.subtype (Submonoid.centralizer {(↑x : M)})) :
            (a : (↥(Submonoid.centralizer {(↑x : M)}))ˣ) → Mˣ)
          u :
        Mˣ)

Tactic:
Units.ext <| (u.1.2 x <| Set.mem_singleton _).symm

Premises used: Set.mem_singleton, Units.val, Units.ext, Eq.symm, Subtype.property
-- Module: Mathlib.GroupTheory.GroupAction.ConjAct
Goal:
α : Type u_1
M : Type u_2
G : Type u_3
inst : Monoid M
x : Mˣ
u : (↥(Submonoid.centralizer {(↑x : M)}))ˣ
⊢ HMul.hMul (α := Mˣ)
      ((Units.map (Submonoid.subtype (Submonoid.centralizer {(↑x : M)})) :
            (a : (↥(Submonoid.centralizer {(↑x : M)}))ˣ) → Mˣ)
          u :
        Mˣ)
      x =
    HMul.hMul (β := Mˣ) x
      ((Units.map (Submonoid.subtype (Submonoid.centralizer {(↑x : M)})) :
            (a : (↥(Submonoid.centralizer {(↑x : M)}))ˣ) → Mˣ)
          u :
        Mˣ)

Tactic:
exact Units.ext <| (u.1.2 x <| Set.mem_singleton _).symm

Premises used: Set.mem_singleton, Units.val, Units.ext, Eq.symm, Subtype.property
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
γ : Type u_2
α : Type u_3
inst : SMul γ α
a₁ a₂ : α
⊢ a₂ ∈ orbit γ a₁ ↔ ∃ (x : γ), x • a₁ = a₂

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, MulAction.orbit, Set.range
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
γ : Type u_2
α : Type u_3
inst : SMul γ α
a : α
m : γ
⊢ m • a ∈ orbit γ a

Tactic:
⟨m, rfl⟩

Premises used: Set.Mem, setOf, MulAction.orbit, Exists.intro, Set.range, rfl
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
M : Type u_1
α : Type u_3
inst : Monoid M
inst_1 : MulAction M α
a₁ a₂ : α
m : M
h : a₂ ∈ orbit M a₁
obtain : ∀ (x : M) (h : x • a₁ ∈ orbit M a₁), m • x • a₁ ∈ orbit M a₁
⊢ m • a₂ ∈ orbit M a₁

Tactic:
obtain ⟨x, rfl⟩ := mem_orbit_iff.mp h

Premises used: MulAction.mem_orbit_iff, Iff.mp, rfl
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
M : Type u_1
α : Type u_3
inst : Monoid M
inst_1 : MulAction M α
a₁ : α
m x : M
h : x • a₁ ∈ orbit M a₁
⊢ m • x • a₁ ∈ orbit M a₁

Tactic:
simp [smul_smul]

Premises used: smul_smul
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
M : Type u_1
α : Type u_3
inst : Monoid M
inst_1 : MulAction M α
a : α
⊢ (fun (m : M) ↦ m • a) 1 = a

Tactic:
simp
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
M : Type u_1
α : Type u_3
inst : Monoid M
inst_1 : MulAction M α
a : α
⊢ (orbit M a).Nonempty

Tactic:
Set.range_nonempty _

Premises used: MulAction.orbit, Set.range_nonempty
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
M : Type u_1
α : Type u_3
inst : Monoid M
inst_1 : MulAction M α
m : M
a : α
⊢ Set.MapsTo (fun (x : α) ↦ m • x) (orbit M a) (orbit M a)

Tactic:
Set.mapsTo_iff_subset_preimage.mpr <| Set.range_subset_iff.mpr fun m' => ⟨m * m', mul_smul _ _ _⟩

Premises used: Set.mapsTo_iff_subset_preimage, Iff.mpr, HMul.hMul, Exists.intro, Set.range_subset_iff, SemigroupAction.mul_smul
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
M : Type u_1
α : Type u_3
inst : Monoid M
inst_1 : MulAction M α
m : M
a : α
⊢ m • orbit M a ⊆ orbit M a

Tactic:
(mapsTo_smul_orbit m a).image_subset

Premises used: Set.MapsTo.image_subset, MulAction.mapsTo_smul_orbit
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
M : Type u_1
α : Type u_3
inst : Monoid M
inst_1 : MulAction M α
m : M
a : α
⊢ orbit M (m • a) ⊆ orbit M a

Tactic:
Set.range_subset_iff.2 fun m' => mul_smul m' m a ▸ mem_orbit _ _

Premises used: Iff.mpr, HMul.hMul, Eq.rec, MulAction.orbit, MulAction.mem_orbit, Set.range_subset_iff, SemigroupAction.mul_smul
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
M : Type u_1
α : Type u_3
inst : Monoid M
inst_1 : MulAction M α
a : α
m : M
a' : (↑(orbit M a) : Type u_3)
⊢ (↑(m • a') : α) = m • (↑a' : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
M : Type u_1
α : Type u_3
inst : Monoid M
inst_1 : MulAction M α
S : Submonoid M
a : α
g : ↥S
⊢ (fun (m : ↥S) ↦ m • a) g ∈ orbit M a

Tactic:
mem_orbit _ _

Premises used: Set.Mem, MulAction.mem_orbit
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
M : Type u_1
α : Type u_3
inst : Monoid M
inst_1 : MulAction M α
S : Submonoid M
a : α
g : ↥S
⊢ (fun (m : ↥S) ↦ m • a) g ∈ orbit M a

Tactic:
exact mem_orbit _ _

Premises used: MulAction.mem_orbit
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
M : Type u_1
α : Type u_3
inst : Monoid M
inst_1 : MulAction M α
S : Submonoid M
a b : α
h : a ∈ orbit.{u_1, u_3} (↥S) b
⊢ a ∈ orbit M b

Tactic:
orbit_submonoid_subset S _ h

Premises used: MulAction.orbit_submonoid_subset
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
M : Type u_1
α : Type u_3
inst : Monoid M
inst_1 : MulAction M α
⊢ fixedPoints M α = ⋂ (m : M), fixedBy α m

Tactic:
Set.ext fun _ =>
    ⟨fun hx => Set.mem_iInter.2 fun m => hx m, fun hx m => (Set.mem_iInter.1 hx m :)⟩

Premises used: Iff.mpr, Set.ext, Set.mem_iInter, Iff.intro, Iff.mp
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
M : Type u_1
α : Type u_3
inst : Monoid M
inst_1 : MulAction M α
a : α
⊢ a ∈ fixedPoints M α ↔ ∀ (m : M), m • a = a

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, MulAction.fixedPoints
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
M : Type u_1
α : Type u_3
inst : Monoid M
inst_1 : MulAction M α
m : M
a : α
⊢ a ∈ fixedBy α m ↔ m • a = a

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, MulAction.fixedBy
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
M : Type u_1
α : Type u_3
inst : Monoid M
inst_1 : MulAction M α
a : α
⊢ a ∈ fixedPoints M α ↔ ∀ a' ∈ orbit M a, a' = a

Tactic:
⟨fun h _ h₁ =>
    let ⟨m, hm⟩ := mem_orbit_iff.1 h₁
    hm ▸ h m,
    fun h _ => h _ (mem_orbit _ _)⟩

Premises used: MulAction.mem_orbit_iff, Eq.rec, _private.0.MulAction.mem_fixedPoints'.match_1, Iff.intro, MulAction.mem_orbit, Iff.mp, HSMul.hSMul, Eq
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
M : Type u_1
γ : Type u_2
α : Type u_3
inst : SMul γ α
inst_1 : Monoid M
inst_2 : MulAction M α
a : α
m m' : M
ha : m • a = a
hb : m' • a = a
rw : m • m' • a = a
rw₁ : m • a = a
rw₂ rw₃ : a = a
⊢ (m * m') • a = a

Tactic:
rw [← smul_smul, hb, ha]

Premises used: smul_smul
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
M : Type u_1
α : Type u_3
inst : Monoid M
inst_1 : MulAction M α
a : α
m : M
⊢ Membership.mem (γ := Submonoid M) (stabilizerSubmonoid M a) m ↔ m • a = a

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
M : Type u
α : Type v
inst : Monoid M
inst_1 : Monoid α
inst_2 : MulDistribMulAction M α
a b : α
ha : a ∈ MulAction.fixedPoints M α
hb : b ∈ MulAction.fixedPoints M α
x : M
rw : x • a * x • b = a * b
rw₁ : a * x • b = a * b
rw₂ rw₃ : a * b = a * b
⊢ x • (a * b) = a * b

Tactic:
rw [smul_mul', ha, hb]

Premises used: smul_mul'
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
M : Type u
α : Type v
inst : Monoid M
inst_1 : Monoid α
inst_2 : MulDistribMulAction M α
a : α
⊢ Membership.mem (γ := Submonoid α) (submonoid M α) a ↔ ∀ (m : M), m • a = a

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, MulAction.fixedPoints
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
M : Type u
α : Type v
inst : Monoid M
inst_1 : Group α
inst_2 : MulDistribMulAction M α
x : α
ha : x ∈ Subsemigroup.carrier (Submonoid.toSubsemigroup (submonoid M α))
x_1 : M
rw : (x_1 • x)⁻¹ = x⁻¹
rw₁ rw₂ : x⁻¹ = x⁻¹
⊢ x_1 • x⁻¹ = x⁻¹

Tactic:
rw [smul_inv', ha]

Premises used: smul_inv'
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
M : Type u
α : Type v
inst : Monoid M
inst_1 : Group α
inst_2 : MulDistribMulAction M α
a : α
⊢ Membership.mem (γ := Subgroup α) (α^*M) a ↔ ∀ (m : M), m • a = a

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, MulAction.fixedPoints
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
M : Type u
α : Type v
inst : Monoid M
inst_1 : Group α
inst_2 : MulDistribMulAction M α
⊢ Eq (α := Submonoid α) (Subgroup.toSubmonoid (α^*M)) (submonoid M α)

Tactic:
rfl

Premises used: FixedPoints.submonoid, rfl
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
g : G
a : α
rw rw₁ : orbit G a = orbit G a
⊢ orbit G a = orbit G (g⁻¹ • g • a)

Tactic:
rw [inv_smul_smul]

Premises used: inv_smul_smul
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
a b : α
⊢ orbit G a = orbit G b ↔ a ∈ orbit G b

Tactic:
⟨fun h => h ▸ mem_orbit_self _, fun ⟨_, hc⟩ => hc ▸ orbit_smul _ _⟩

Premises used: Eq.rec, MulAction.orbit, Iff.intro, MulAction.orbit_smul, Eq, _private.0.MulAction.orbit_eq_iff.match_1, MulAction.mem_orbit_self
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
g : G
a : α
⊢ a ∈ orbit G (g • a)

Tactic:
simp only [orbit_smul, mem_orbit_self]

Premises used: MulAction.orbit_smul, MulAction.mem_orbit_self
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
g h : G
a : α
⊢ g • a ∈ orbit G (h • a)

Tactic:
simp only [orbit_smul, mem_orbit]

Premises used: MulAction.orbit_smul, 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
a : ↥H
b : α
⊢ a • b = (↑a : G) • b

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
a : α
⊢ orbit.{u_1, u_2} (↥H) a ⊆ orbit G a

Tactic:
orbit_submonoid_subset H.toSubmonoid a

Premises used: Set.Mem, MulAction.orbit_submonoid_subset, Subgroup.toSubmonoid
-- 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 ∈ orbit.{u_1, u_2} (↥H) b
⊢ a ∈ orbit G b

Tactic:
orbit_subgroup_subset H _ h

Premises used: MulAction.orbit_subgroup_subset
-- Module: Mathlib.GroupTheory.GroupAction.Defs
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
a₁ a₂ : α
simp_rw : orbit G a₁ = orbit G a₂ ↔ orbit G a₂ = orbit G a₁
⊢ a₁ ∈ orbit G a₂ ↔ a₂ ∈ orbit G a₁

Tactic:
simp_rw [← orbit_eq_iff, eq_comm]

Premises used: eq_comm, 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 : α
a b : (↑(orbit G x) : Type u_2)
⊢ a ∈ orbit.{u_1, u_2} (↥H) b ↔ (↑a : α) ∈ 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 : α
a b : (↑(orbit G x) : Type u_2)
refine_1 : ∀ (h : a ∈ orbit.{u_1, u_2} (↥H) b), (↑a : α) ∈ orbit.{u_1, u_2} ↥H (↑b : α)
refine_2 : ∀ (h : (↑a : α) ∈ orbit.{u_1, u_2} ↥H (↑b : α)), a ∈ orbit.{u_1, u_2} (↥H) b
⊢ a ∈ orbit.{u_1, u_2} (↥H) b ↔ (↑a : α) ∈ 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 : α
a b : (↑(orbit G x) : Type u_2)
h : a ∈ orbit.{u_1, u_2} (↥H) b
refine_1 : ∀ (g : ↥H), (↑((fun (m : ↥H) ↦ m • b) g) : α) ∈ orbit.{u_1, u_2} ↥H (↑b : α)
⊢ (↑a : α) ∈ 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 : α
b : (↑(orbit G x) : Type u_2)
g : ↥H
⊢ (↑((fun (m : ↥H) ↦ m • b) g) : α) ∈ 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 : α
b : (↑(orbit G x) : Type u_2)
g : ↥H
⊢ (↑((fun (m : ↥H) ↦ m • b) g) : α) ∈ 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 : α
a b : (↑(orbit G x) : Type u_2)
h : (↑a : α) ∈ orbit.{u_1, u_2} ↥H (↑b : α)
refine_2 : ∀ (g : ↥H) (h : (fun (m : ↥H) ↦ m • (↑b : α)) g = (↑a : α)), a ∈ orbit.{u_1, u_2} (↥H) b
⊢ a ∈ 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 : α
a b : (↑(orbit G x) : 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: Subtype.ext_iff, MulAction.orbit.coe_smul, 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 : α
a b : (↑(orbit G x) : Type u_2)
g : ↥H
h : (↑g : G) • b = a
refine_2 : (↑g : G) • b ∈ orbit.{u_1, u_2} (↥H) b
⊢ a ∈ 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 : α
b : (↑(orbit G x) : Type u_2)
g : ↥H
⊢ (↑g : G) • b ∈ 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 : α
b : (↑(orbit G x) : Type u_2)
g : ↥H
⊢ (↑g : G) • b ∈ 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
β : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MulAction G β
⊢ ∀ {x y z : α}, x ∈ orbit G y → y ∈ orbit G z → x ∈ orbit G z

Tactic:
grind [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 α
a b : α
⊢ (orbitRel G α : α → α → Prop) a b ↔ a ∈ orbit G b

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 α
U : Set α
this : Setoid α := orbitRel G α
set :
  let f : α → Quotient (orbitRel G α) := Quotient.mk';
  f ⁻¹' f '' U = ⋃ (g : G), (fun (x : α) ↦ g • x) '' U
⊢ Set.preimage (β := Quotient (orbitRel G α)) Quotient.mk' (Quotient.mk' '' U) = ⋃ (g : G), (fun (x : α) ↦ g • x) '' U

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 : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
h : ∀ (a : α), a ∈ f ⁻¹' f '' U ↔ Membership.mem (γ := Set α) (⋃ (g : G), (fun (x : α) ↦ g • x) '' U) a
⊢ f ⁻¹' f '' U = ⋃ (g : G), (fun (x : α) ↦ g • x) '' U

Tactic:
ext a
-- Module: Mathlib.GroupTheory.GroupAction.Defs
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 : α
h : a ∈ f ⁻¹' f '' U → Membership.mem (γ := Set α) (⋃ (g : G), (fun (x : α) ↦ g • x) '' U) a
h₁ : Membership.mem (γ := Set α) (⋃ (g : G), (fun (x : α) ↦ g • x) '' U) a → a ∈ f ⁻¹' f '' U
⊢ a ∈ f ⁻¹' f '' U ↔ Membership.mem (γ := Set α) (⋃ (g : G), (fun (x : α) ↦ g • x) '' U) a

Tactic:
constructor
-- Module: Mathlib.GroupTheory.GroupAction.Defs
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 b : α
hb : b ∈ U
hab : f b = f a
h :
  ∀ (g : G) (hb : (fun (m : G) ↦ m • a) g ∈ U) (hab : f ((fun (m : G) ↦ m • a) g) = f a),
    Membership.mem (γ := Set α) (⋃ (g : G), (fun (x : α) ↦ g • x) '' U) a
⊢ Membership.mem (γ := Set α) (⋃ (g : G), (fun (x : α) ↦ g • x) '' U) a

Tactic:
obtain ⟨g, rfl⟩ := Quotient.exact hab

Premises used: Quotient.exact, rfl
-- Module: Mathlib.GroupTheory.GroupAction.Defs
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
hb : (fun (m : G) ↦ m • a) g ∈ U
hab : f ((fun (m : G) ↦ m • a) g) = f a
h : ∃ (i : G), Membership.mem (γ := Set α) ((fun (x : α) ↦ i • x) '' U) a
⊢ Membership.mem (γ := Set α) (⋃ (g : G), (fun (x : α) ↦ g • x) '' U) a

Tactic:
rw [Set.mem_iUnion]

Premises used: Set.mem_iUnion
-- Module: Mathlib.GroupTheory.GroupAction.Defs
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
hb : (fun (m : G) ↦ m • a) g ∈ U
hab : f ((fun (m : G) ↦ m • a) g) = f a
⊢ ∃ (i : G), Membership.mem (γ := Set α) ((fun (x : α) ↦ i • x) '' U) a

Tactic:
⟨g⁻¹, g • a, hb, inv_smul_smul g a⟩

Premises used: inv_smul_smul, Inv.inv, And.intro, Exists.intro, HSMul.hSMul
-- Module: Mathlib.GroupTheory.GroupAction.Defs
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
hb : (fun (m : G) ↦ m • a) g ∈ U
hab : f ((fun (m : G) ↦ m • a) g) = f a
⊢ ∃ (i : G), Membership.mem (γ := Set α) ((fun (x : α) ↦ i • x) '' U) a

Tactic:
exact ⟨g⁻¹, g • a, hb, inv_smul_smul g a⟩
-- Module: Mathlib.GroupTheory.GroupAction.Defs
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 : α
hx : Membership.mem (γ := Set α) (⋃ (g : G), (fun (x : α) ↦ g • x) '' U) a
⊢ ∃ (i : G), Membership.mem (γ := Set α) ((fun (x : α) ↦ i • x) '' U) a

Tactic:
rw [Set.mem_iUnion] at hx

Premises used: Set.mem_iUnion
-- Module: Mathlib.GroupTheory.GroupAction.Defs
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 : α
hx : ∃ (i : G), Membership.mem (γ := Set α) ((fun (x : α) ↦ i • x) '' U) a
h : ∀ (g : G) (u : α) (hu₁ : u ∈ U) (hu₂ : (fun (x : α) ↦ g • x) u = a), a ∈ f ⁻¹' f '' U
⊢ a ∈ f ⁻¹' f '' U

Tactic:
obtain ⟨g, u, hu₁, hu₂⟩ := hx
-- Module: Mathlib.GroupTheory.GroupAction.Defs
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
⊢ f (g⁻¹ • a) = f a

Tactic:
simp +instances [f, orbitRel, Quotient.eq']

Premises used: MulAction.orbitRel, Quotient.eq'
-- Module: Mathlib.GroupTheory.GroupAction.Defs
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
h : g⁻¹ • a ∈ U
⊢ ∃ x ∈ U, f x = f a

Tactic:
refine ⟨g⁻¹ • a, ?_, by simp +instances [f, orbitRel, Quotient.eq']⟩
-- Module: Mathlib.GroupTheory.GroupAction.Defs
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
h : HSMul.hSMul (β := α) g⁻¹ ((fun (x : α) ↦ g • x) u) ∈ U
⊢ g⁻¹ • a ∈ U

Tactic:
rw [← hu₂]
-- Module: Mathlib.GroupTheory.GroupAction.Defs
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
⊢ u ∈ U

Tactic:
hu₁
-- Module: Mathlib.GroupTheory.GroupAction.Defs
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
h : HSMul.hSMul (β := α) g⁻¹ ((fun (x : α) ↦ g • x) u) = u
⊢ HSMul.hSMul (β := α) g⁻¹ ((fun (x : α) ↦ g • x) u) ∈ U

Tactic:
convert! hu₁
-- Module: Mathlib.GroupTheory.GroupAction.Defs
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

Tactic:
simp only [inv_smul_smul]

Premises used: inv_smul_smul