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 α
t : Set ↥(ofFixingSubgroup M s)
⊢ Disjoint s
    (Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ''
      t)
have rw : s ∩
    Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ''
      t ⊆
  ∅
Tactic: rw [Set.disjoint_iff]
-- 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 α
⊢ Bijective.{u_2 + 1, u_2 + 1} (α := ↥(ofFixingSubgroup M ∅)) (β := α)
    (⇑(ofFixingSubgroup_equivariantMap M ∅) : (a : ↥(ofFixingSubgroup M ∅)) → α)
have refine : ∀ (x : α),
  ∃ (a : ↥(ofFixingSubgroup M ∅)), (ofFixingSubgroup_equivariantMap M ∅ : (a : ↥(ofFixingSubgroup M ∅)) → α) a = x
Tactic: refine ⟨ofFixingSubgroup_equivariantMap_injective, fun 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 α
a : α
s : Set ↥(ofStabilizer M a)
⊢ Eq (α := Subgroup M) (fixingSubgroup M (α := α) (insert a ((fun (x : ↥(ofStabilizer M a)) ↦ (↑x : α)) '' s)))
    (Subgroup.map (G := ↥(stabilizer M a)) (Subgroup.subtype (stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) s))
have h : ∀ (m : M),
  Membership.mem (γ := Subgroup M)
      (fixingSubgroup M (α := α) (insert a ((fun (x : ↥(ofStabilizer M a)) ↦ (↑x : α)) '' s))) m ↔
    Membership.mem (γ := Subgroup M)
      (Subgroup.map (G := ↥(stabilizer M a)) (Subgroup.subtype (stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) s))
      m
Tactic: ext m
-- 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_1 : Set α
a : α
s : Set ↥(ofStabilizer M a)
m :
  ↥(fixingSubgroup M
      (insert a
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
          s)))
x_1 : (↑s : Type u_2)
x : ↥(ofStabilizer M a)
hx : x ∈ s
⊢ HSMul.hSMul (α := ↥(stabilizer M a))
      (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (stabilizer M a) x) (↑m : M) ⋯)
      (↑(Subtype.mk (p := fun (x : ↥(ofStabilizer M a)) ↦ x ∈ s) x hx) : ↥(ofStabilizer M a)) =
    (↑(Subtype.mk (p := fun (x : ↥(ofStabilizer M a)) ↦ x ∈ s) x hx) : ↥(ofStabilizer M a))
have simp : (↑(HSMul.hSMul (α := ↥(stabilizer M a))
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (stabilizer M a) x) (↑m : M) sorry) x) :
    α) =
  (↑x : α)
Tactic: simp only [← SetLike.coe_eq_coe]
-- 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_1 : Set α
a : α
s : Set ↥(ofStabilizer M a)
m :
  ↥(fixingSubgroup M
      (insert a
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
          s)))
x_1 : (↑s : Type u_2)
x : ↥(ofStabilizer M a)
hx : x ∈ s
⊢ (↑(HSMul.hSMul (α := ↥(stabilizer M a))
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (stabilizer M a) x) (↑m : M) ⋯) x) :
      α) =
    (↑x : α)
have refine : (↑x : α) ∈
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
    s
Tactic: refine (mem_fixingSubgroup_iff M).mp m.prop _ (Set.mem_insert_of_mem a ?_)
-- 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_1 : Set α
a : α
s : Set ↥(ofStabilizer M a)
x :
  ↥(ofFixingSubgroup M
      (insert a
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
          s)))
⊢ ↥(ofFixingSubgroup (↥(stabilizer M a)) s)
have hx : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) (↑x : α)
Tactic: choose hx hx' using (mem_ofFixingSubgroup_insert_iff.mp x.prop)
-- 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_1 : Set α
a : α
s : Set ↥(ofStabilizer M a)
x :
  ↥(ofFixingSubgroup M
      (insert a
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
          s)))
hx : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) (↑x : α)
⊢ ↥(ofFixingSubgroup (↥(stabilizer M a)) s)
have hx' : Membership.mem (γ := SubMulAction.{u_1, u_2} ↥(fixingSubgroup (↥(stabilizer M a)) s) ↥(ofStabilizer M a))
  (ofFixingSubgroup (↥(stabilizer M a)) s)
  (Subtype.mk (p := fun (x : α) ↦
    Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) (↑x : α) hx)
Tactic: choose hx hx' using (mem_ofFixingSubgroup_insert_iff.mp x.prop)
-- 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 α
a : α
s : Set ↥(ofStabilizer M a)
⊢ Bijective (α :=
    ↥(ofFixingSubgroup M
        (insert a
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
            s))))
    (β := ↥(ofFixingSubgroup (↥(stabilizer M a)) s))
    (⇑(ofFixingSubgroup_insert_map a s) :
      (a_1 : ↥(ofFixingSubgroup M (insert a (Subtype.val '' s)))) → ↥(ofFixingSubgroup (↥(stabilizer M a)) s))
have left : Injective (α :=
  ↥(ofFixingSubgroup M
      (insert a
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
          s))))
  (β := ↥(ofFixingSubgroup (↥(stabilizer M a)) s))
  (⇑(ofFixingSubgroup_insert_map a s) :
    (a_1 : ↥(ofFixingSubgroup M (insert a (Subtype.val '' s)))) → ↥(ofFixingSubgroup (↥(stabilizer M a)) s))
Tactic: constructor
-- 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 α
a : α
s : Set ↥(ofStabilizer M a)
left :
  Injective (α :=
    ↥(ofFixingSubgroup M
        (insert a
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
            s))))
    (β := ↥(ofFixingSubgroup (↥(stabilizer M a)) s))
    (⇑(ofFixingSubgroup_insert_map a s) :
      (a_1 : ↥(ofFixingSubgroup M (insert a (Subtype.val '' s)))) → ↥(ofFixingSubgroup (↥(stabilizer M a)) s))
⊢ Bijective (α :=
    ↥(ofFixingSubgroup M
        (insert a
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
            s))))
    (β := ↥(ofFixingSubgroup (↥(stabilizer M a)) s))
    (⇑(ofFixingSubgroup_insert_map a s) :
      (a_1 : ↥(ofFixingSubgroup M (insert a (Subtype.val '' s)))) → ↥(ofFixingSubgroup (↥(stabilizer M a)) s))
have right : Surjective (α :=
  ↥(ofFixingSubgroup M
      (insert a
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
          s))))
  (β := ↥(ofFixingSubgroup (↥(stabilizer M a)) s))
  (⇑(ofFixingSubgroup_insert_map a s) :
    (a_1 : ↥(ofFixingSubgroup M (insert a (Subtype.val '' s)))) → ↥(ofFixingSubgroup (↥(stabilizer M a)) s))
Tactic: constructor
-- 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 t : Set α
g : M
hg : g • t = s
k : M
hk : Membership.mem (γ := Subgroup M) (fixingSubgroup M t) k
⊢ Membership.mem (α := M) (γ := Subgroup M) (fixingSubgroup M s)
    ((((MulAut.conj : (a : M) → MulAut M) g : MulAut M) : (a : M) → M) k : M)
have simp : ∀ (hk : ∀ y ∈ t, k • y = y),
  ∀ y ∈ s, HSMul.hSMul (α := M) ((((MulAut.conj : (a : M) → MulAut M) g : MulAut M) : (a : M) → M) k : M) y = y
Tactic: simp only [mem_fixingSubgroup_iff] at hk ⊢
Cleared hypotheses: hk
-- 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 t : Set α
g : M
hg : g • t = s
k : M
hk : ∀ y ∈ t, k • y = y
y : α
hy : y ∈ s
⊢ HSMul.hSMul (α := M) ((((MulAut.conj : (a : M) → MulAut M) g : MulAut M) : (a : M) → M) k : M) y = y
have rw : k • g⁻¹ • y = g⁻¹ • y
Tactic: rw [MulAut.conj_apply, eq_comm, mul_smul, mul_smul, ← inv_smul_eq_iff, eq_comm]
-- 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 t : Set α
g : M
hg : g • t = s
k : M
hk : ∀ y ∈ t, k • y = y
y : α
hy : y ∈ s
⊢ k • g⁻¹ • y = g⁻¹ • y
have a : g⁻¹ • y ∈ t
Tactic: apply hk
-- 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 t : Set α
g : M
hg : g • t = s
⊢ Eq (α := Subgroup M) (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : M) → MulAut M) g)) (fixingSubgroup M t))
    (fixingSubgroup M s)
have h : ∀ (k : M),
  Membership.mem (γ := Subgroup M)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : M) → MulAut M) g)) (fixingSubgroup M t)) k ↔
    Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
Tactic: ext k
-- 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 t : Set α
g : M
hg : g • t = s
k : M
⊢ Membership.mem (γ := Subgroup M)
      (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : M) → MulAut M) g)) (fixingSubgroup M t)) k ↔
    Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
have h : (∃ (x : M),
    Membership.mem (γ := Subgroup M) (fixingSubgroup M t) x ∧
      (((MulAut.conj : (a : M) → MulAut M) g : MulAut M) : (a : M) → M) x = k) ↔
  Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
Tactic: simp only [MulEquiv.toMonoidHom_eq_coe, Subgroup.mem_map, MonoidHom.coe_coe]
-- 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 t : Set α
g : M
hg : g • t = s
k : M
⊢ (∃ (x : M),
      Membership.mem (γ := Subgroup M) (fixingSubgroup M t) x ∧
        (((MulAut.conj : (a : M) → MulAut M) g : MulAut M) : (a : M) → M) x = k) ↔
    Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
have h : (∃ (x : M),
    Membership.mem (γ := Subgroup M) (fixingSubgroup M t) x ∧
      (((MulAut.conj : (a : M) → MulAut M) g : MulAut M) : (a : M) → M) x = k) →
  Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
Tactic: constructor
-- 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 t : Set α
g : M
hg : g • t = s
k : M
h :
  (∃ (x : M),
      Membership.mem (γ := Subgroup M) (fixingSubgroup M t) x ∧
        (((MulAut.conj : (a : M) → MulAut M) g : MulAut M) : (a : M) → M) x = k) →
    Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
⊢ (∃ (x : M),
      Membership.mem (γ := Subgroup M) (fixingSubgroup M t) x ∧
        (((MulAut.conj : (a : M) → MulAut M) g : MulAut M) : (a : M) → M) x = k) ↔
    Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
have h₁ : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k →
  ∃ (x : M),
    Membership.mem (γ := Subgroup M) (fixingSubgroup M t) x ∧
      (((MulAut.conj : (a : M) → MulAut M) g : MulAut M) : (a : M) → M) x = k
Tactic: constructor
-- 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 t : Set α
g : M
hg : g • t = s
k : M
hk : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
⊢ ∃ (x : M),
    Membership.mem (γ := Subgroup M) (fixingSubgroup M t) x ∧
      (((MulAut.conj : (a : M) → MulAut M) g : MulAut M) : (a : M) → M) x = k
have h : Membership.mem (α := M) (γ := Subgroup M) (fixingSubgroup M t)
    ((((MulAut.conj : (a : M) → MulAut M) g⁻¹ : MulAut M) : (a : M) → M) k : M) ∧
  (((MulAut.conj : (a : M) → MulAut M) g : MulAut M) : (a : M) → M)
      ((((MulAut.conj : (a : M) → MulAut M) g⁻¹ : MulAut M) : (a : M) → M) k : M) =
    k
Tactic: use MulAut.conj g⁻¹ k
-- 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 t : Set α
g : M
hg : g • t = s
k : M
hk : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
⊢ Membership.mem (α := M) (γ := Subgroup M) (fixingSubgroup M t)
      ((((MulAut.conj : (a : M) → MulAut M) g⁻¹ : MulAut M) : (a : M) → M) k : M) ∧
    (((MulAut.conj : (a : M) → MulAut M) g : MulAut M) : (a : M) → M)
        ((((MulAut.conj : (a : M) → MulAut M) g⁻¹ : MulAut M) : (a : M) → M) k : M) =
      k
have h : Membership.mem (α := M) (γ := Subgroup M) (fixingSubgroup M t)
  ((((MulAut.conj : (a : M) → MulAut M) g⁻¹ : MulAut M) : (a : M) → M) k : M)
Tactic: constructor
-- 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 t : Set α
g : M
hg : g • t = s
k : M
hk : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
h :
  Membership.mem (α := M) (γ := Subgroup M) (fixingSubgroup M t)
    ((((MulAut.conj : (a : M) → MulAut M) g⁻¹ : MulAut M) : (a : M) → M) k : M)
⊢ Membership.mem (α := M) (γ := Subgroup M) (fixingSubgroup M t)
      ((((MulAut.conj : (a : M) → MulAut M) g⁻¹ : MulAut M) : (a : M) → M) k : M) ∧
    (((MulAut.conj : (a : M) → MulAut M) g : MulAut M) : (a : M) → M)
        ((((MulAut.conj : (a : M) → MulAut M) g⁻¹ : MulAut M) : (a : M) → M) k : M) =
      k
have h₁ : (((MulAut.conj : (a : M) → MulAut M) g : MulAut M) : (a : M) → M)
    ((((MulAut.conj : (a : M) → MulAut M) g⁻¹ : MulAut M) : (a : M) → M) k : M) =
  k
Tactic: constructor
-- 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 t : Set α
g : M
hg : g • t = s
k : M
hk : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
⊢ Membership.mem (α := M) (γ := Subgroup M) (fixingSubgroup M t)
    ((((MulAut.conj : (a : M) → MulAut M) g⁻¹ : MulAut M) : (a : M) → M) k : M)
have apply : g⁻¹ • s = t
Tactic: apply Set.conj_mem_fixingSubgroup _ hk
-- 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 t : Set α
g : M
hg : g • t = s
k : M
hk : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
⊢ g⁻¹ • s = t
have rw : s = g • t
Tactic: rw [inv_smul_eq_iff, hg]
-- 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 t : Set α
g : M
hg : g • t = s
k : M
hk : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
rw : s = g • t
⊢ g⁻¹ • s = t
have rw₁ : s = s
Tactic: rw [inv_smul_eq_iff, hg]
-- 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 t : Set α
g : M
hg : g • t = s
k : M
hk : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
⊢ (((MulAut.conj : (a : M) → MulAut M) g : MulAut M) : (a : M) → M)
      ((((MulAut.conj : (a : M) → MulAut M) g⁻¹ : MulAut M) : (a : M) → M) k : M) =
    k
have h : g * (g⁻¹ * k * g) * g⁻¹ = k
Tactic: simp [MulAut.conj]
-- 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_1 s t : Set α
g : M
hg : g • t = s
x_1 : ↥(ofFixingSubgroup M t)
x : α
hx : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M t)) α) (ofFixingSubgroup M t) x
hgxt : g • x ∈ s
⊢ False
have apply : x ∈ t
Tactic: apply 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_1 s t : Set α
g : M
hg : g • t = s
x_1 : ↥(ofFixingSubgroup M t)
x : α
hx : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M t)) α) (ofFixingSubgroup M t) x
hgxt : g • x ∈ s
⊢ x ∈ t
have hgxt₁ : g • x ∈ g • t
Tactic: rw [← hg] at hgxt
Cleared hypotheses: hgxt
-- 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 t : Set α
g : M
hst : g • s = t
⊢ Bijective (α := ↥(ofFixingSubgroup M s)) (β := ↥(ofFixingSubgroup M t))
    (⇑(conjMap_ofFixingSubgroup (s := t) (t := s) hst) : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup M t))
have left : Injective (α := ↥(ofFixingSubgroup M s)) (β := ↥(ofFixingSubgroup M t))
  (⇑(conjMap_ofFixingSubgroup (s := t) (t := s) hst) : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup M t))
Tactic: constructor
-- 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 t : Set α
g : M
hst : g • s = t
left :
  Injective (α := ↥(ofFixingSubgroup M s)) (β := ↥(ofFixingSubgroup M t))
    (⇑(conjMap_ofFixingSubgroup (s := t) (t := s) hst) : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup M t))
⊢ Bijective (α := ↥(ofFixingSubgroup M s)) (β := ↥(ofFixingSubgroup M t))
    (⇑(conjMap_ofFixingSubgroup (s := t) (t := s) hst) : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup M t))
have right : Surjective (α := ↥(ofFixingSubgroup M s)) (β := ↥(ofFixingSubgroup M t))
  (⇑(conjMap_ofFixingSubgroup (s := t) (t := s) hst) : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup M t))
Tactic: constructor
-- 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 t : Set α
g : M
hst : g • s = t
x : α
hx : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M t)) α) (ofFixingSubgroup M t) x
⊢ ∃ (a : ↥(ofFixingSubgroup M s)),
    (conjMap_ofFixingSubgroup (s := t) (t := s) hst : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup M t)) a =
      Subtype.mk (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M t)) α) (ofFixingSubgroup M t) x) x hx
have right : ∀ (hst_1 : g⁻¹ • t = s) (x : α)
  (hx : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M t)) α) (ofFixingSubgroup M t) x),
  ∃ (a : ↥(ofFixingSubgroup M s)),
    (conjMap_ofFixingSubgroup (s := t) (t := s) hst : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup M t)) a =
      Subtype.mk (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M t)) α) (ofFixingSubgroup M t) x) x hx
Tactic: rw [eq_comm, ← inv_smul_eq_iff] at hst
Cleared hypotheses: 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 t : Set α
g : M
hst_1 : g • s = t
hst : g⁻¹ • t = s
x : α
hx : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M t)) α) (ofFixingSubgroup M t) x
⊢ ∃ (a : ↥(ofFixingSubgroup M s)),
    (conjMap_ofFixingSubgroup (s := t) (t := s) hst_1 : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup M t)) a =
      Subtype.mk (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M t)) α) (ofFixingSubgroup M t) x) x hx
have h : (conjMap_ofFixingSubgroup (s := t) (t := s) hst_1 : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup M t))
    ((conjMap_ofFixingSubgroup (s := s) (t := t) hst : (a : ↥(ofFixingSubgroup M t)) → ↥(ofFixingSubgroup M s))
      (Subtype.mk (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M t)) α) (ofFixingSubgroup M t) x) x hx)) =
  Subtype.mk (p := fun (x : α) ↦
    Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M t)) α) (ofFixingSubgroup M t) x) x hx
Tactic: use (SubMulAction.conjMap_ofFixingSubgroup hst) ⟨x, 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_1 s t : Set α
m : ↥(fixingSubgroup M (s ∪ t))
x : α
hx : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x
hx' :
  Membership.mem (γ := Set ↥(ofFixingSubgroup M s))
    (Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
      t)
    (Subtype.mk (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) x hx)
⊢ Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) (↑m : M) ⋯ •
      (↑(Subtype.mk (p := fun (x : ↥(ofFixingSubgroup M s)) ↦
            Membership.mem (γ := Set ↥(ofFixingSubgroup M s))
              (Subtype.val (p := fun (x : α) ↦
                  Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
                t)
              x)
            (Subtype.mk (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) x hx)
            hx') :
        ↥(ofFixingSubgroup M s)) =
    (↑(Subtype.mk (p := fun (x : ↥(ofFixingSubgroup M s)) ↦
          Membership.mem (γ := Set ↥(ofFixingSubgroup M s))
            (Subtype.val (p := fun (x : α) ↦
                Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
              t)
            x)
          (Subtype.mk (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) x hx)
          hx') :
      ↥(ofFixingSubgroup M s))
have hx'₁ : x ∈ t
Tactic: simp only [Set.mem_preimage] at hx'