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_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'_1 :
  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)
hx' : x ∈ t
simp : Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) (↑m : M) ⋯ • x = x
⊢ 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'_1) :
        ↥(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'_1) :
      ↥(ofFixingSubgroup M s))

Tactic:
simp only [← SetLike.coe_eq_coe, SubMulAction.val_smul_of_tower]

Premises used: SetLike.coe_eq_coe, SubMulAction.val_smul_of_tower
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
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'_1 :
  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)
hx' : x ∈ t
⊢ Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) (↑m : M) ⋯ • x = x

Tactic:
(mem_fixingSubgroup_union_iff.mp m.prop).2 ⟨x, hx'⟩

Premises used: Subtype.mk, And.right, Subtype.prop, Iff.mp, SubMulAction.mem_fixingSubgroup_union_iff
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
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'_1 :
  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)
hx' : x ∈ t
⊢ Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) (↑m : M) ⋯ • x = x

Tactic:
exact (mem_fixingSubgroup_union_iff.mp m.prop).2 ⟨x, hx'⟩

Premises used: Subtype.mk, And.right, Subtype.prop, Iff.mp, SubMulAction.mem_fixingSubgroup_union_iff
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s_1 s t : Set α
⊢ Eq.{u_1 + 1} (α :=
    ↥(fixingSubgroup ↥(fixingSubgroup M s) (α := ↥(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 : ↥(fixingSubgroup M s)) ↦
      Membership.mem (γ := Subgroup ↥(fixingSubgroup M s))
        (fixingSubgroup ↥(fixingSubgroup M s) (α := ↥(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 : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) (↑1 : M) ⋯) ⋯)
    1

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 s t : Set α
x x_1 : ↥(fixingSubgroup M (s ∪ t))
⊢ Subtype.mk (p := fun (x : ↥(fixingSubgroup M s)) ↦
      Membership.mem (γ := Subgroup ↥(fixingSubgroup M s))
        (fixingSubgroup ↥(fixingSubgroup M s) (α := ↥(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 : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) (↑(x * x_1) : M) ⋯) ⋯ =
    Subtype.mk (p := fun (x : ↥(fixingSubgroup M s)) ↦
        Membership.mem (γ := Subgroup ↥(fixingSubgroup M s))
          (fixingSubgroup ↥(fixingSubgroup M s) (α := ↥(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 : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) (↑x : M) ⋯) ⋯ *
      Subtype.mk (p := fun (x : ↥(fixingSubgroup M s)) ↦
        Membership.mem (γ := Subgroup ↥(fixingSubgroup M s))
          (fixingSubgroup ↥(fixingSubgroup M s) (α := ↥(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 : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) (↑x_1 : M) ⋯) ⋯

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 s t : Set α
m : ↥(fixingSubgroup M (s ∪ t))
hm : Membership.mem (γ := Subgroup M) (fixingSubgroup M (s ∪ t)) (↑m : M) := ⋯
⊢ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) (↑m : M) ∧
    Membership.mem (γ := Subgroup M) (fixingSubgroup M t) (↑m : M)

Tactic:
simp only [fixingSubgroup_union, Subgroup.mem_inf] at hm

Premises used: fixingSubgroup_union, Subgroup.mem_inf
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
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))
hm :
  Membership.mem (γ := Subgroup M) (fixingSubgroup M s) (↑m : M) ∧
    Membership.mem (γ := Subgroup M) (fixingSubgroup M t) (↑m : M)
⊢ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) (↑m : M)

Tactic:
hm.left

Premises used: And.left
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
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))
hm :
  Membership.mem (γ := Subgroup M) (fixingSubgroup M s) (↑m : M) ∧
    Membership.mem (γ := Subgroup M) (fixingSubgroup M t) (↑m : M)
⊢ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) (↑m : M)

Tactic:
exact hm.left

Premises used: And.left
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
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))
hm :
  Membership.mem (γ := Subgroup M) (fixingSubgroup M s) (↑m : M) ∧
    Membership.mem (γ := Subgroup M) (fixingSubgroup M t) (↑m : M)
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)
⊢ x ∈ t

Tactic:
simp only [Set.mem_preimage] at hx'

Premises used: Set.mem_preimage
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
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))
hm :
  Membership.mem (γ := Subgroup M) (fixingSubgroup M s) (↑m : M) ∧
    Membership.mem (γ := Subgroup M) (fixingSubgroup M t) (↑m : M)
x : α
hx : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x
hx'_1 :
  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)
hx' : x ∈ t
simp : Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) (↑m : M) ⋯ • x = x
⊢ 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'_1) :
        ↥(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'_1) :
      ↥(ofFixingSubgroup M s))

Tactic:
simp only [← SetLike.coe_eq_coe, SubMulAction.val_smul_of_tower]

Premises used: SetLike.coe_eq_coe, SubMulAction.val_smul_of_tower
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
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))
hm :
  Membership.mem (γ := Subgroup M) (fixingSubgroup M s) (↑m : M) ∧
    Membership.mem (γ := Subgroup M) (fixingSubgroup M t) (↑m : M)
x : α
hx : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x
hx'_1 :
  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)
hx' : x ∈ t
⊢ Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) (↑m : M) ⋯ • x = x

Tactic:
hm.right ⟨x, hx'⟩

Premises used: Subtype.mk, And.right
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
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))
hm :
  Membership.mem (γ := Subgroup M) (fixingSubgroup M s) (↑m : M) ∧
    Membership.mem (γ := Subgroup M) (fixingSubgroup M t) (↑m : M)
x : α
hx : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x
hx'_1 :
  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)
hx' : x ∈ t
⊢ Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) (↑m : M) ⋯ • x = x

Tactic:
exact hm.right ⟨x, hx'⟩

Premises used: Subtype.mk, And.right
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s_1 s t : Set α
x : ↥(ofFixingSubgroup M (s ∪ t))
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 : α) ⋯)
apply : (↑x : α) ∈ t
⊢ (↑x : α) ∈ s ∪ t

Tactic:
apply Set.mem_union_right s

Premises used: Set.mem_union_right
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s_1 s t : Set α
x : ↥(ofFixingSubgroup M (s ∪ t))
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 : α) ⋯)
⊢ (↑x : α) ∈ t

Tactic:
simpa only [Set.mem_preimage, Subtype.coe_mk] using hx

Premises used: Subtype.coe_mk, Set.mem_preimage
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s t : Set α
x : ↥(ofFixingSubgroup M (s ∪ t))
⊢ (↑(↑((map_ofFixingSubgroupUnion M s t :
                (a : ↥(ofFixingSubgroup M (s ∪ t))) → ↥(ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)))
              x) :
          ↥(ofFixingSubgroup M s)) :
      α) =
    (↑x : α)

Tactic:
rfl

Premises used: Set.union, Set.Mem, setOf, Not, rfl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s t : Set α
left :
  Injective (α := ↥(ofFixingSubgroup M (s ∪ t))) (β :=
    ↥(ofFixingSubgroup (↥(fixingSubgroup M s))
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
          t)))
    (⇑(map_ofFixingSubgroupUnion M s t) :
      (a : ↥(ofFixingSubgroup M (s ∪ t))) → ↥(ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)))
right :
  Surjective (α := ↥(ofFixingSubgroup M (s ∪ t))) (β :=
    ↥(ofFixingSubgroup (↥(fixingSubgroup M s))
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
          t)))
    (⇑(map_ofFixingSubgroupUnion M s t) :
      (a : ↥(ofFixingSubgroup M (s ∪ t))) → ↥(ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)))
⊢ Bijective (α := ↥(ofFixingSubgroup M (s ∪ t))) (β :=
    ↥(ofFixingSubgroup (↥(fixingSubgroup M s))
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
          t)))
    (⇑(map_ofFixingSubgroupUnion M s t) :
      (a : ↥(ofFixingSubgroup M (s ∪ t))) → ↥(ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)))

Tactic:
constructor
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s t : Set α
a b : ↥(ofFixingSubgroup M (s ∪ t))
h :
  Eq (α :=
    ↥(ofFixingSubgroup (↥(fixingSubgroup M s))
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
          t)))
    ((map_ofFixingSubgroupUnion M s t :
          (a : ↥(ofFixingSubgroup M (s ∪ t))) → ↥(ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)))
        a :
      ↥(ofFixingSubgroup (↥(fixingSubgroup M s))
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
            t)))
    ((map_ofFixingSubgroupUnion M s t :
          (a : ↥(ofFixingSubgroup M (s ∪ t))) → ↥(ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)))
        b :
      ↥(ofFixingSubgroup (↥(fixingSubgroup M s))
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
            t)))
⊢ a = b

Tactic:
simpa only [← SetLike.coe_eq_coe] using h

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 t : Set α
a : α
ha : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) a
ha' :
  Membership.mem (γ :=
    SubMulAction.{u_1, u_2}
      ↥(fixingSubgroup ↥(fixingSubgroup M s) (α := ↥(ofFixingSubgroup M s))
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
            t))
      ↥(ofFixingSubgroup M s))
    (ofFixingSubgroup (↥(fixingSubgroup 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) a ha)
this : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∪ t))) α) (ofFixingSubgroup M (s ∪ t)) a
⊢ ∃ (a_1 : ↥(ofFixingSubgroup M (s ∪ t))),
    (map_ofFixingSubgroupUnion M s t :
          (a : ↥(ofFixingSubgroup M (s ∪ t))) → ↥(ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)))
        a_1 =
      Subtype.mk (p := fun (x : ↥(ofFixingSubgroup M s)) ↦
        Membership.mem (γ :=
          SubMulAction.{u_1, u_2}
            ↥(fixingSubgroup ↥(fixingSubgroup M s) (α := ↥(ofFixingSubgroup M s))
                (Subtype.val (p := fun (x : α) ↦
                    Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s)
                      x) ⁻¹'
                  t))
            ↥(ofFixingSubgroup M s))
          (ofFixingSubgroup (↥(fixingSubgroup 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) a ha)
        ha'

Tactic:
⟨⟨a, this⟩,  rfl⟩

Premises used: Subtype.mk, Exists.intro, rfl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s t : Set α
a : α
ha : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) a
ha' :
  Membership.mem (γ :=
    SubMulAction.{u_1, u_2}
      ↥(fixingSubgroup ↥(fixingSubgroup M s) (α := ↥(ofFixingSubgroup M s))
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
            t))
      ↥(ofFixingSubgroup M s))
    (ofFixingSubgroup (↥(fixingSubgroup 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) a ha)
this : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∪ t))) α) (ofFixingSubgroup M (s ∪ t)) a
⊢ ∃ (a_1 : ↥(ofFixingSubgroup M (s ∪ t))),
    (map_ofFixingSubgroupUnion M s t :
          (a : ↥(ofFixingSubgroup M (s ∪ t))) → ↥(ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)))
        a_1 =
      Subtype.mk (p := fun (x : ↥(ofFixingSubgroup M s)) ↦
        Membership.mem (γ :=
          SubMulAction.{u_1, u_2}
            ↥(fixingSubgroup ↥(fixingSubgroup M s) (α := ↥(ofFixingSubgroup M s))
                (Subtype.val (p := fun (x : α) ↦
                    Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s)
                      x) ⁻¹'
                  t))
            ↥(ofFixingSubgroup M s))
          (ofFixingSubgroup (↥(fixingSubgroup 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) a ha)
        ha'

Tactic:
exact ⟨⟨a, this⟩,  rfl⟩
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s t : Set α
a : α
ha : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) a
ha' :
  Membership.mem (γ :=
    SubMulAction.{u_1, u_2}
      ↥(fixingSubgroup ↥(fixingSubgroup M s) (α := ↥(ofFixingSubgroup M s))
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
            t))
      ↥(ofFixingSubgroup M s))
    (ofFixingSubgroup (↥(fixingSubgroup 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) a ha)
right : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∪ t))) α) (ofFixingSubgroup M (s ∪ t)) a
⊢ ∃ (a_1 : ↥(ofFixingSubgroup M (s ∪ t))),
    (map_ofFixingSubgroupUnion M s t :
          (a : ↥(ofFixingSubgroup M (s ∪ t))) → ↥(ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)))
        a_1 =
      Subtype.mk (p := fun (x : ↥(ofFixingSubgroup M s)) ↦
        Membership.mem (γ :=
          SubMulAction.{u_1, u_2}
            ↥(fixingSubgroup ↥(fixingSubgroup M s) (α := ↥(ofFixingSubgroup M s))
                (Subtype.val (p := fun (x : α) ↦
                    Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s)
                      x) ⁻¹'
                  t))
            ↥(ofFixingSubgroup M s))
          (ofFixingSubgroup (↥(fixingSubgroup 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) a ha)
        ha'

Tactic:
suffices a ∈ ofFixingSubgroup M (s ∪ t) by
      exact ⟨⟨a, this⟩,  rfl⟩