awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
hs : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
rw :
  ∀ (x : ↥(ofFixingSubgroup M (s ∩ g • s))),
    ∃ (g_1 : ↥(fixingSubgroup M (s ∩ g • s))),
      g_1 •
          Subtype.mk (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α)
              (ofFixingSubgroup M (s ∩ g • s)) x)
            a ha' =
        x
⊢ IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))

Tactic:
rw [MulAction.isPretransitive_iff_base (⟨a, ha'⟩ : ofFixingSubgroup M (s ∩ g • s))]

Premises used: MulAction.isPretransitive_iff_base, Subtype.mk
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
hs : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx :
  Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α) (ofFixingSubgroup M (s ∩ g • s)) x
⊢ x ∉ s ∨ x ∉ g • s

Tactic:
rw [mem_ofFixingSubgroup_iff, Set.mem_inter_iff, not_and_or] at hx

Premises used: Set.mem_inter_iff, not_and_or, SubMulAction.mem_ofFixingSubgroup_iff
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
hs : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx_1 :
  Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α) (ofFixingSubgroup M (s ∩ g • s)) x
hx : x ∉ s ∨ x ∉ g • s
inl :
  ∀ (hx : x ∉ s),
    ∃ (g_1 : ↥(fixingSubgroup M (s ∩ g • s))),
      g_1 •
          Subtype.mk (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α)
              (ofFixingSubgroup M (s ∩ g • s)) x)
            a ha' =
        Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α)
            (ofFixingSubgroup M (s ∩ g • s)) x)
          x hx_1
inr :
  ∀ (hx : x ∉ g • s),
    ∃ (g_1 : ↥(fixingSubgroup M (s ∩ g • s))),
      g_1 •
          Subtype.mk (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α)
              (ofFixingSubgroup M (s ∩ g • s)) x)
            a ha' =
        Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α)
            (ofFixingSubgroup M (s ∩ g • s)) x)
          x hx_1
⊢ ∃ (g_1 : ↥(fixingSubgroup M (s ∩ g • s))),
    g_1 •
        Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α)
            (ofFixingSubgroup M (s ∩ g • s)) x)
          a ha' =
      Subtype.mk (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α)
          (ofFixingSubgroup M (s ∩ g • s)) x)
        x hx_1

Tactic:
rcases hx with hx | hx
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
hs : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx_1 :
  Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α) (ofFixingSubgroup M (s ∩ g • s)) x
hx : x ∉ s
inl :
  ∀ (k : M) (hk : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k)
    (hkax :
      Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) k hk •
          Subtype.mk (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) a ⋯ =
        Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) x hx),
    ∃ (g_1 : ↥(fixingSubgroup M (s ∩ g • s))),
      g_1 •
          Subtype.mk (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α)
              (ofFixingSubgroup M (s ∩ g • s)) x)
            a ha' =
        Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α)
            (ofFixingSubgroup M (s ∩ g • s)) x)
          x hx_1
⊢ ∃ (g_1 : ↥(fixingSubgroup M (s ∩ g • s))),
    g_1 •
        Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α)
            (ofFixingSubgroup M (s ∩ g • s)) x)
          a ha' =
      Subtype.mk (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α)
          (ofFixingSubgroup M (s ∩ g • s)) x)
        x hx_1

Tactic:
obtain ⟨⟨k, hk⟩, hkax⟩ := hs.exists_smul_eq ⟨a, ha.1⟩ ⟨x, hx⟩

Premises used: MulAction.IsPretransitive.exists_smul_eq, Subtype.mk, And.left
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
hs : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx_1 :
  Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α) (ofFixingSubgroup M (s ∩ g • s)) x
hx : x ∉ s
k : M
hk : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
hkax :
  Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) k hk •
      Subtype.mk (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) a ⋯ =
    Subtype.mk (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) x hx
h :
  HSMul.hSMul (α := ↥(fixingSubgroup M (s ∩ g • s)))
      (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M (s ∩ g • s)) x) k ⋯)
      (Subtype.mk (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α)
          (ofFixingSubgroup M (s ∩ g • s)) x)
        a ha') =
    Subtype.mk (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α) (ofFixingSubgroup M (s ∩ g • s))
        x)
      x hx_1
⊢ ∃ (g_1 : ↥(fixingSubgroup M (s ∩ g • s))),
    g_1 •
        Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α)
            (ofFixingSubgroup M (s ∩ g • s)) x)
          a ha' =
      Subtype.mk (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α)
          (ofFixingSubgroup M (s ∩ g • s)) x)
        x hx_1

Tactic:
use ⟨k, fun ⟨y, hy⟩ ↦ hk ⟨y, hy.1⟩⟩
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
hs : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx_1 :
  Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α) (ofFixingSubgroup M (s ∩ g • s)) x
hx : x ∉ s
k : M
hk : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
hkax :
  Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) k hk •
      Subtype.mk (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) a ⋯ =
    Subtype.mk (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) x hx
h h₁ h₂ h₃ :
  ∀
    (hkax :
      (↑(Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) k hk •
              Subtype.mk (p := fun (x : α) ↦
                Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) a ⋯) :
          α) =
        (↑(Subtype.mk (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) x hx) :
          α)),
    (↑(HSMul.hSMul (α := ↥(fixingSubgroup M (s ∩ g • s)))
            (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M (s ∩ g • s)) x) k ⋯)
            (Subtype.mk (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α)
                (ofFixingSubgroup M (s ∩ g • s)) x)
              a ha')) :
        α) =
      (↑(Subtype.mk (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α)
              (ofFixingSubgroup M (s ∩ g • s)) x)
            x hx_1) :
        α)
⊢ HSMul.hSMul (α := ↥(fixingSubgroup M (s ∩ g • s)))
      (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M (s ∩ g • s)) x) k ⋯)
      (Subtype.mk (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α)
          (ofFixingSubgroup M (s ∩ g • s)) x)
        a ha') =
    Subtype.mk (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α) (ofFixingSubgroup M (s ∩ g • s))
        x)
      x hx_1

Tactic:
rwa [Subtype.ext_iff] at hkax ⊢

Premises used: Subtype.ext_iff
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
hs : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx_1 :
  Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α) (ofFixingSubgroup M (s ∩ g • s)) x
hx : x ∉ g • s
⊢ Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) (g⁻¹ • x)

Tactic:
have hg'x : g⁻¹ • x ∈ ofFixingSubgroup M s := mt Set.mem_smul_set_iff_inv_smul_mem.mpr hx
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
hs : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx_1 :
  Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α) (ofFixingSubgroup M (s ∩ g • s)) x
hx : x ∉ g • s
hg'x : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) (g⁻¹ • x)
⊢ Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) (g⁻¹ • a)

Tactic:
have hg'a : g⁻¹ • a ∈ ofFixingSubgroup M s := mt Set.mem_smul_set_iff_inv_smul_mem.mpr ha.2
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
hs : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx_1 :
  Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α) (ofFixingSubgroup M (s ∩ g • s)) x
hx : x ∉ g • s
hg'x : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) (g⁻¹ • x)
hg'a : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) (g⁻¹ • a)
inr :
  ∀ (k : M) (hk : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k)
    (hkax :
      Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) k hk •
          Subtype.mk (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) (g⁻¹ • a)
            hg'a =
        Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) (g⁻¹ • x)
          hg'x),
    ∃ (g_1 : ↥(fixingSubgroup M (s ∩ g • s))),
      g_1 •
          Subtype.mk (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α)
              (ofFixingSubgroup M (s ∩ g • s)) x)
            a ha' =
        Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α)
            (ofFixingSubgroup M (s ∩ g • s)) x)
          x hx_1
⊢ ∃ (g_1 : ↥(fixingSubgroup M (s ∩ g • s))),
    g_1 •
        Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α)
            (ofFixingSubgroup M (s ∩ g • s)) x)
          a ha' =
      Subtype.mk (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α)
          (ofFixingSubgroup M (s ∩ g • s)) x)
        x hx_1

Tactic:
obtain ⟨⟨k, hk⟩, hkax⟩ := hs.exists_smul_eq ⟨g⁻¹ • a, hg'a⟩ ⟨g⁻¹ • x, hg'x⟩

Premises used: MulAction.IsPretransitive.exists_smul_eq, Subtype.mk, Inv.inv, HSMul.hSMul
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
hs : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx_1 :
  Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α) (ofFixingSubgroup M (s ∩ g • s)) x
hx : x ∉ g • s
hg'x : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) (g⁻¹ • x)
hg'a : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) (g⁻¹ • a)
k : M
hk : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
hkax :
  Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) k hk •
      Subtype.mk (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) (g⁻¹ • a)
        hg'a =
    Subtype.mk (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) (g⁻¹ • x) hg'x
h :
  HSMul.hSMul (α := ↥(fixingSubgroup M (s ∩ g • s)))
      (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M (s ∩ g • s)) x) (g * k * g⁻¹)
        ⋯)
      (Subtype.mk (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α)
          (ofFixingSubgroup M (s ∩ g • s)) x)
        a ha') =
    Subtype.mk (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α) (ofFixingSubgroup M (s ∩ g • s))
        x)
      x hx_1
w : Membership.mem (γ := Subgroup M) (fixingSubgroup M (s ∩ g • s)) (g * k * g⁻¹)
⊢ ∃ (g_1 : ↥(fixingSubgroup M (s ∩ g • s))),
    g_1 •
        Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α)
            (ofFixingSubgroup M (s ∩ g • s)) x)
          a ha' =
      Subtype.mk (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α)
          (ofFixingSubgroup M (s ∩ g • s)) x)
        x hx_1

Tactic:
use ⟨g * k * g⁻¹, ?_⟩
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
hs : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx_1 :
  Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α) (ofFixingSubgroup M (s ∩ g • s)) x
hx : x ∉ g • s
hg'x : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) (g⁻¹ • x)
hg'a : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) (g⁻¹ • a)
k : M
hk : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
hkax :
  Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) k hk •
      Subtype.mk (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) (g⁻¹ • a)
        hg'a =
    Subtype.mk (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) (g⁻¹ • x) hg'x
h :
  ∀
    (hkax :
      (↑(Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) k hk •
              Subtype.mk (p := fun (x : α) ↦
                Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x)
                (g⁻¹ • a) hg'a) :
          α) =
        g⁻¹ • x),
    (↑(HSMul.hSMul (α := ↥(fixingSubgroup M (s ∩ g • s)))
            (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M (s ∩ g • s)) x)
              (g * k * g⁻¹) ⋯)
            (Subtype.mk (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α)
                (ofFixingSubgroup M (s ∩ g • s)) x)
              a ha')) :
        α) =
      x
⊢ HSMul.hSMul (α := ↥(fixingSubgroup M (s ∩ g • s)))
      (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M (s ∩ g • s)) x) (g * k * g⁻¹)
        ⋯)
      (Subtype.mk (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α)
          (ofFixingSubgroup M (s ∩ g • s)) x)
        a ha') =
    Subtype.mk (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α) (ofFixingSubgroup M (s ∩ g • s))
        x)
      x hx_1

Tactic:
simp only [← SetLike.coe_eq_coe] at hkax ⊢

Premises used: SetLike.coe_eq_coe
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
hs : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx_1 :
  Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α) (ofFixingSubgroup M (s ∩ g • s)) x
hx : x ∉ g • s
hg'x : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) (g⁻¹ • x)
hg'a : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) (g⁻¹ • a)
k : M
hk : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
hkax :
  Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) k hk •
      Subtype.mk (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) (g⁻¹ • a)
        hg'a =
    Subtype.mk (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) (g⁻¹ • x) hg'x
w :
  ∀ (hk_1 : ∀ y ∈ s, k • y = y)
    (hkax :
      Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) k hk •
          Subtype.mk (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) (g⁻¹ • a)
            hg'a =
        Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) (g⁻¹ • x)
          hg'x),
    ∀ y ∈ s ∩ g • s, (g * k * g⁻¹) • y = y
⊢ Membership.mem (γ := Subgroup M) (fixingSubgroup M (s ∩ g • s)) (g * k * g⁻¹)

Tactic:
rw [mem_fixingSubgroup_iff] at hk ⊢

Premises used: mem_fixingSubgroup_iff
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
hs : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx_1 :
  Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α) (ofFixingSubgroup M (s ∩ g • s)) x
hx : x ∉ g • s
hg'x : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) (g⁻¹ • x)
hg'a : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) (g⁻¹ • a)
k : M
hk_1 : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
hk : ∀ y ∈ s, k • y = y
hkax :
  Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) k hk_1 •
      Subtype.mk (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) (g⁻¹ • a)
        hg'a =
    Subtype.mk (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) (g⁻¹ • x) hg'x
y : α
hy : y ∈ s ∩ g • s
w : k • g⁻¹ • y = g⁻¹ • y
⊢ (g * k * g⁻¹) • y = y

Tactic:
rw [mul_smul, mul_smul, smul_eq_iff_eq_inv_smul g]

Premises used: smul_eq_iff_eq_inv_smul, SemigroupAction.mul_smul
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
hs : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx_1 :
  Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α) (ofFixingSubgroup M (s ∩ g • s)) x
hx : x ∉ g • s
hg'x : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) (g⁻¹ • x)
hg'a : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) (g⁻¹ • a)
k : M
hk_1 : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
hk : ∀ y ∈ s, k • y = y
hkax :
  Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) k hk_1 •
      Subtype.mk (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) (g⁻¹ • a)
        hg'a =
    Subtype.mk (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) (g⁻¹ • x) hg'x
y : α
hy : y ∈ s ∩ g • s
⊢ k • g⁻¹ • y = g⁻¹ • y

Tactic:
hk _ (Set.mem_smul_set_iff_inv_smul_mem.mp hy.2)

Premises used: And.right, Iff.mp, Set.mem_smul_set_iff_inv_smul_mem
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
hs : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx_1 :
  Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α) (ofFixingSubgroup M (s ∩ g • s)) x
hx : x ∉ g • s
hg'x : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) (g⁻¹ • x)
hg'a : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) (g⁻¹ • a)
k : M
hk_1 : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
hk : ∀ y ∈ s, k • y = y
hkax :
  Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) k hk_1 •
      Subtype.mk (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) (g⁻¹ • a)
        hg'a =
    Subtype.mk (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) (g⁻¹ • x) hg'x
y : α
hy : y ∈ s ∩ g • s
⊢ k • g⁻¹ • y = g⁻¹ • y

Tactic:
exact hk _ (Set.mem_smul_set_iff_inv_smul_mem.mp hy.2)

Premises used: And.right, Iff.mp, Set.mem_smul_set_iff_inv_smul_mem