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 α
x_1 : ↥(fixingSubgroup M s)
x : α
c : M
hc_1 : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) c
hc : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) c⁻¹
simp : Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) c hc_1 • x ∈ s → x ∈ s
⊢ x ∈ sᶜ → Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) c hc_1 • x ∈ sᶜ

Tactic:
simp only [Set.mem_compl_iff, not_imp_not]

Premises used: Set.mem_compl_iff, not_imp_not
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
x_1 : ↥(fixingSubgroup M s)
x : α
c : M
hc_1 : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) c
hc : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) c⁻¹
hcx : Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) c hc_1 • x ∈ s
rwa : HSMul.hSMul.{u_1, u_2, u_2} (α := M) 1 x ∈ s
rwa₁ : (c⁻¹ * c) • x ∈ s
rwa₂ : c⁻¹ • c • x ∈ s
rwa₃ rwa₄ rwa₅ rwa₆ : c • x ∈ s
⊢ x ∈ s

Tactic:
rwa [← one_smul M x, ← inv_mul_cancel c, mul_smul, (mem_fixingSubgroup_iff M).mp hc (c • x) hcx]

Premises used: inv_mul_cancel, one_smul, Iff.mp, HSMul.hSMul, mem_fixingSubgroup_iff, 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 α
⊢ carrier (R := ↥(fixingSubgroup M s)) (ofFixingSubgroup M s) = sᶜ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
x : α
⊢ Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x ↔ x ∉ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Not
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
x : ↥(ofFixingSubgroup M s)
⊢ (↑x : α) ∉ s

Tactic:
x.prop

Premises used: Set.Mem, setOf, Subtype.prop, Not
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
t : Set ↥(ofFixingSubgroup M s)
rw :
  s ∩
      Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ''
        t ⊆
    ∅
⊢ Disjoint 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]

Premises used: Set.disjoint_iff
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
t : Set ↥(ofFixingSubgroup M s)
b : ↥(ofFixingSubgroup M s)
left : b ∈ t
hbs : (↑b : α) ∈ s
⊢ Membership.mem (γ := Set α) ∅ (↑b : α)

Tactic:
(b.prop hbs).elim

Premises used: False.elim, Subtype.prop
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
t : Set ↥(ofFixingSubgroup M s)
b : ↥(ofFixingSubgroup M s)
left : b ∈ t
hbs : (↑b : α) ∈ s
⊢ Membership.mem (γ := Set α) ∅ (↑b : α)

Tactic:
exact (b.prop hbs).elim

Premises used: False.elim, Subtype.prop
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
x : α
hx : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x
y : α
hy : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) y
hxy :
  Eq (α := α)
    ((ofFixingSubgroup_equivariantMap M s : (a : ↥(ofFixingSubgroup M s)) → α)
        (Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) x hx) :
      α)
    ((ofFixingSubgroup_equivariantMap M s : (a : ↥(ofFixingSubgroup M s)) → α)
        (Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) y hy) :
      α)
⊢ 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 : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) y hy

Tactic:
simpa [Subtype.mk.injEq] using hxy

Premises used: Subtype.mk.injEq
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
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 ∅)) → α)

Tactic:
⟨ofFixingSubgroup_equivariantMap_injective, fun x ↦ ?_⟩

Premises used: SubMulAction.ofFixingSubgroup_equivariantMap_injective, And.intro, Function.Bijective
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
refine :
  ∀ (x : α),
    ∃ (a : ↥(ofFixingSubgroup M ∅)), (ofFixingSubgroup_equivariantMap M ∅ : (a : ↥(ofFixingSubgroup M ∅)) → α) a = x
⊢ Bijective.{u_2 + 1, u_2 + 1} (α := ↥(ofFixingSubgroup M ∅)) (β := α)
    (⇑(ofFixingSubgroup_equivariantMap M ∅) : (a : ↥(ofFixingSubgroup M ∅)) → α)

Tactic:
refine ⟨ofFixingSubgroup_equivariantMap_injective, fun x ↦ ?_⟩
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
x : α
⊢ ∃ (a : ↥(ofFixingSubgroup M ∅)), (ofFixingSubgroup_equivariantMap M ∅ : (a : ↥(ofFixingSubgroup M ∅)) → α) a = x

Tactic:
⟨⟨x, (mem_ofFixingSubgroup_iff M).mp (Set.notMem_empty x)⟩, rfl⟩

Premises used: Subtype.mk, Exists.intro, Iff.mp, Set.notMem_empty, SubMulAction.mem_ofFixingSubgroup_iff, rfl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
x : α
⊢ ∃ (a : ↥(ofFixingSubgroup M ∅)), (ofFixingSubgroup_equivariantMap M ∅ : (a : ↥(ofFixingSubgroup M ∅)) → α) a = x

Tactic:
exact ⟨⟨x, (mem_ofFixingSubgroup_iff M).mp (Set.notMem_empty x)⟩, rfl⟩
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
g : M
⊢ Membership.mem (γ := Subgroup M) (fixingSubgroup.{u_1, u_2} M (α := α) ∅) g

Tactic:
simp
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
a : α
s : Set α
m : M
⊢ Membership.mem (γ := Subgroup M) (fixingSubgroup M (insert a s)) m ↔
    m • a = a ∧ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) m

Tactic:
simp [mem_fixingSubgroup_iff]

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 α
a : α
s : Set ↥(ofStabilizer M a)
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
⊢ 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))

Tactic:
ext m
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
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:
simp [mem_fixingSubgroup_iff, mem_ofStabilizer_iff, subgroup_smul_def, and_comm]

Premises used: and_comm, SubMulAction.mem_ofStabilizer_iff, MulAction.subgroup_smul_def, mem_fixingSubgroup_iff
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
⊢ Membership.mem (γ :=
      SubMulAction.{u_1, u_2}
        (↥(fixingSubgroup M (α := α) (insert a ((fun (x : ↥(ofStabilizer M a)) ↦ (↑x : α)) '' s)))) α)
      (ofFixingSubgroup M (insert a ((fun (x : ↥(ofStabilizer M a)) ↦ (↑x : α)) '' s))) x ↔
    ∃ (hx : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x),
      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:
grind [mem_ofFixingSubgroup_iff, mem_ofStabilizer_iff]

Premises used: SubMulAction.mem_ofStabilizer_iff, 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_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
simp :
  (↑(HSMul.hSMul (α := ↥(stabilizer M a))
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (stabilizer M a) x) (↑m : M) ⋯) x) :
      α) =
    (↑x : α)
⊢ 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))

Tactic:
simp only [← SetLike.coe_eq_coe]

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_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 : α)

Tactic:
(mem_fixingSubgroup_iff M).mp m.prop _ (Set.mem_insert_of_mem a ?_)

Premises used: Set.mem_insert_of_mem, Subtype.prop, Iff.mp, 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_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
refine :
  (↑x : α) ∈
    Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) 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 : α)

Tactic:
refine (mem_fixingSubgroup_iff M).mp m.prop _ (Set.mem_insert_of_mem a ?_)

Premises used: Set.mem_insert_of_mem, Subtype.prop, Iff.mp, 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_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
⊢ (↑x : α) ∈
    Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
      s

Tactic:
⟨⟨x, (SubMulAction.mem_ofStabilizer_iff  M a).mp x.prop⟩, hx, rfl⟩

Premises used: Set.Mem, setOf, Subtype.mk, SubMulAction.mem_ofStabilizer_iff, Subtype.prop, And.intro, Exists.intro, Iff.mp, Set.image, Subtype.val, rfl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
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
⊢ (↑x : α) ∈
    Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
      s

Tactic:
exact ⟨⟨x, (SubMulAction.mem_ofStabilizer_iff  M a).mp x.prop⟩, hx, rfl⟩
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
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 (↥(stabilizer M a)) s)
⊢ Membership.mem (γ := Subgroup 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)))
    (↑(↑m : ↥(stabilizer M a)) : M)

Tactic:
simp [fixingSubgroup_of_insert]

Premises used: SubMulAction.fixingSubgroup_of_insert
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
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 :
  ↥(fixingSubgroup M
      (insert a
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
          s)))
⊢ (fun (m : ↥(fixingSubgroup (↥(stabilizer M a)) s)) ↦
        Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Subgroup 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)
          (↑(↑m : ↥(stabilizer M a)) : M) ⋯)
      ((fun
            (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)))) ↦
          (Subtype.mk (p := fun (x : ↥(stabilizer M a)) ↦
              Membership.mem (γ := Subgroup ↥(stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) s) x)
              (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (stabilizer M a) x) (↑m : M) ⋯) ⋯ :
            ↥(fixingSubgroup (↥(stabilizer M a)) s)))
        x) =
    x

Tactic:
simp
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
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 : ↥(fixingSubgroup (↥(stabilizer M a)) s)
⊢ (fun
          (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)))) ↦
        (Subtype.mk (p := fun (x : ↥(stabilizer M a)) ↦
            Membership.mem (γ := Subgroup ↥(stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) s) x)
            (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (stabilizer M a) x) (↑m : M) ⋯) ⋯ :
          ↥(fixingSubgroup (↥(stabilizer M a)) s)))
      ((fun (m : ↥(fixingSubgroup (↥(stabilizer M a)) s)) ↦
          Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := Subgroup 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)
            (↑(↑m : ↥(stabilizer M a)) : M) ⋯)
        x) =
    x

Tactic:
simp
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
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 x_1 :
  ↥(fixingSubgroup M
      (insert a
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
          s)))
⊢ Subtype.mk (p := fun (x : ↥(stabilizer M a)) ↦
      Membership.mem (γ := Subgroup ↥(stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) s) x)
      (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (stabilizer M a) x) (↑(x * x_1) : M) ⋯) ⋯ =
    HMul.hMul (α := ↥(fixingSubgroup (↥(stabilizer M a)) s))
      (Subtype.mk (p := fun (x : ↥(stabilizer M a)) ↦
        Membership.mem (γ := Subgroup ↥(stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) s) x)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (stabilizer M a) x) (↑x : M) ⋯) ⋯)
      (Subtype.mk (p := fun (x : ↥(stabilizer M a)) ↦
        Membership.mem (γ := Subgroup ↥(stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) s) x)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (stabilizer M a) x) (↑x_1 : M) ⋯) ⋯)

Tactic:
simp [← Subtype.coe_inj]

Premises used: Subtype.coe_inj
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
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)))
⊢ 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)

Premises used: SubMulAction.mem_ofFixingSubgroup_insert_iff, Subtype.prop, Iff.mp
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
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 : α)
⊢ 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)

Premises used: SubMulAction.mem_ofFixingSubgroup_insert_iff, Subtype.prop, Iff.mp
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
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 : α)
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)
⊢ ↥(ofFixingSubgroup (↥(stabilizer M a)) s)

Tactic:
exact ⟨_, hx'⟩
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx :
  Membership.mem (γ :=
    SubMulAction.{u_1, u_2}
      (↥(fixingSubgroup M
          (insert a
            (Subtype.val (p := fun (x : α) ↦
                Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
              s))))
      α)
    (ofFixingSubgroup M
      (insert a
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
          s)))
    x
⊢ (↑(↑((ofFixingSubgroup_insert_map a s :
                (a_1 : ↥(ofFixingSubgroup M (insert a (Subtype.val '' s)))) → ↥(ofFixingSubgroup (↥(stabilizer M a)) s))
              (Subtype.mk (p := fun (x : α) ↦
                Membership.mem (γ :=
                  SubMulAction.{u_1, u_2}
                    (↥(fixingSubgroup M
                        (insert a
                          (Subtype.val (p := fun (x : α) ↦
                              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a)
                                x) ''
                            s))))
                    α)
                  (ofFixingSubgroup M
                    (insert a
                      (Subtype.val (p := fun (x : α) ↦
                          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
                        s)))
                  x)
                x hx)) :
          ↥(ofStabilizer M a)) :
      α) =
    x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
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))
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))
⊢ 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))

Tactic:
constructor