awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup (goal)
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)ᶜ
⊢ a ∈ (s ∩ g • s)ᶜ
have rw : a ∈ sᶜ ∪ (g • s)ᶜ
Tactic: rw [Set.compl_inter]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup (hypothesis)
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)ᶜ
⊢ IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))
have ha' : a ∈ (s ∩ g • s)ᶜ
Tactic: have ha' : a ∈ (s ∩ g • s)ᶜ := by
    rw [Set.compl_inter]
    exact Set.mem_union_left _ ha.1
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup (goal)
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)ᶜ
⊢ IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))
have 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
Tactic: rw [MulAction.isPretransitive_iff_base (⟨a, ha'⟩ : ofFixingSubgroup M (s ∩ g • s))]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup (hypothesis)
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
⊢ ∃ (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
have hx₁ : x ∉ s ∨ x ∉ g • s
Tactic: rw [mem_ofFixingSubgroup_iff, Set.mem_inter_iff, not_and_or] at hx
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup (goal)
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
⊢ ∃ (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
have 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
Tactic: rcases hx with hx | hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup (goal)
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
⊢ ∃ (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
have 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
Tactic: rcases hx with hx | hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup (goal)
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
⊢ ∃ (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
have 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 sorry =
      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
Tactic: obtain ⟨⟨k, hk⟩, hkax⟩ := hs.exists_smul_eq ⟨a, ha.1⟩ ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup (goal)
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
⊢ ∃ (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
have 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 sorry)
    (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⟩⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup (goal)
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
⊢ 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
have 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 sorry) :
        α) =
      (↑(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 sorry)
          (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 ⊢
Cleared hypotheses: hkax
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup (hypothesis)
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
⊢ ∃ (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
have hg'x : 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
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup (hypothesis)
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)
⊢ ∃ (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
have hg'a : 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
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup (goal)
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)
⊢ ∃ (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
have 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
Tactic: obtain ⟨⟨k, hk⟩, hkax⟩ := hs.exists_smul_eq ⟨g⁻¹ • a, hg'a⟩ ⟨g⁻¹ • x, hg'x⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup (goal)
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
⊢ ∃ (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
have 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⁻¹) sorry)
    (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⁻¹, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup (goal)
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
⊢ ∃ (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
have w : Membership.mem (γ := Subgroup M) (fixingSubgroup M (s ∩ g • s)) (g * k * g⁻¹)
Tactic: use ⟨g * k * g⁻¹, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup (goal)
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
⊢ 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
have 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⁻¹) sorry)
          (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
Tactic: simp only [← SetLike.coe_eq_coe] at hkax ⊢