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 α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx1 : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x
hx2 :
  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 hx1)
⊢ ∃ (a_1 :
    ↥(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_insert_map a s :
          (a_2 : ↥(ofFixingSubgroup M (insert a (Subtype.val '' s)))) → ↥(ofFixingSubgroup (↥(stabilizer M a)) s))
        a_1 =
      Subtype.mk (p := fun (x : ↥(ofStabilizer M a)) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} ↥(fixingSubgroup (↥(stabilizer M a)) s) ↥(ofStabilizer M a))
          (ofFixingSubgroup (↥(stabilizer M a)) s) x)
        (Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) x hx1)
        hx2

Tactic:
⟨⟨x, mem_ofFixingSubgroup_insert_iff.mpr ⟨hx1, hx2⟩⟩, rfl⟩

Premises used: Iff.mpr, Subtype.mk, SubMulAction.mem_ofFixingSubgroup_insert_iff, Exists.intro, 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)
x : α
hx1 : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x
hx2 :
  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 hx1)
⊢ ∃ (a_1 :
    ↥(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_insert_map a s :
          (a_2 : ↥(ofFixingSubgroup M (insert a (Subtype.val '' s)))) → ↥(ofFixingSubgroup (↥(stabilizer M a)) s))
        a_1 =
      Subtype.mk (p := fun (x : ↥(ofStabilizer M a)) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} ↥(fixingSubgroup (↥(stabilizer M a)) s) ↥(ofStabilizer M a))
          (ofFixingSubgroup (↥(stabilizer M a)) s) x)
        (Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) x hx1)
        hx2

Tactic:
exact ⟨⟨x, mem_ofFixingSubgroup_insert_iff.mpr ⟨hx1, hx2⟩⟩, 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 α
g : M
hg : g • t = s
k : M
hk : Membership.mem (γ := Subgroup M) (fixingSubgroup M t) k
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
⊢ Membership.mem (α := M) (γ := Subgroup M) (fixingSubgroup M s)
    ((((MulAut.conj : (a : M) → MulAut M) g : MulAut M) : (a : M) → M) k : M)

Tactic:
simp only [mem_fixingSubgroup_iff] at hk ⊢

Premises used: mem_fixingSubgroup_iff
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s t : Set α
g : M
hg : g • t = s
k : M
hk : ∀ y ∈ t, k • y = y
y : α
hy : y ∈ s
rw : k • g⁻¹ • y = g⁻¹ • y
⊢ HSMul.hSMul (α := M) ((((MulAut.conj : (a : M) → MulAut M) g : MulAut M) : (a : M) → M) k : M) y = y

Tactic:
rw [MulAut.conj_apply, eq_comm, mul_smul, mul_smul, ← inv_smul_eq_iff, eq_comm]

Premises used: inv_smul_eq_iff, eq_comm, MulAut.conj_apply, 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 t : Set α
g : M
hg : g • t = s
k : M
hk : ∀ y ∈ t, k • y = y
y : α
hy : y ∈ s
a : g⁻¹ • y ∈ t
⊢ k • g⁻¹ • y = g⁻¹ • y

Tactic:
apply hk
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
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 a : y ∈ s
⊢ g⁻¹ • y ∈ t

Tactic:
rw [← Set.mem_smul_set_iff_inv_smul_mem, hg]

Premises used: Set.mem_smul_set_iff_inv_smul_mem
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s t : Set α
g : M
hg : g • t = s
k : M
hk : ∀ y ∈ t, k • y = y
y : α
hy : y ∈ s
⊢ y ∈ s

Tactic:
hy
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
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
⊢ y ∈ s

Tactic:
exact hy
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s t : Set α
g : M
hg : g • t = s
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
⊢ Eq (α := Subgroup M) (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : M) → MulAut M) g)) (fixingSubgroup M t))
    (fixingSubgroup M s)

Tactic:
ext k
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
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
⊢ 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:
simp only [MulEquiv.toMonoidHom_eq_coe, Subgroup.mem_map, MonoidHom.coe_coe]

Premises used: MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_coe, Subgroup.mem_map
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
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
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
⊢ (∃ (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
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s t : Set α
g : M
hg : g • t = s
n : M
hn : Membership.mem (γ := Subgroup M) (fixingSubgroup M t) n
⊢ Membership.mem (α := M) (γ := Subgroup M) (fixingSubgroup M s)
    ((((MulAut.conj : (a : M) → MulAut M) g : MulAut M) : (a : M) → M) n : M)

Tactic:
Set.conj_mem_fixingSubgroup hg hn

Premises used: Set.conj_mem_fixingSubgroup
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s t : Set α
g : M
hg : g • t = s
n : M
hn : Membership.mem (γ := Subgroup M) (fixingSubgroup M t) n
⊢ Membership.mem (α := M) (γ := Subgroup M) (fixingSubgroup M s)
    ((((MulAut.conj : (a : M) → MulAut M) g : MulAut M) : (a : M) → M) n : M)

Tactic:
exact Set.conj_mem_fixingSubgroup hg hn

Premises used: Set.conj_mem_fixingSubgroup
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
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) ∧
    (((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
⊢ ∃ (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:
use MulAut.conj g⁻¹ k

Premises used: MulAut.conj, Inv.inv, DFunLike.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 α
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)
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
⊢ 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:
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 α
g : M
hg : g • t = s
k : M
hk : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
apply : g⁻¹ • s = t
⊢ Membership.mem (α := M) (γ := Subgroup M) (fixingSubgroup M t)
    ((((MulAut.conj : (a : M) → MulAut M) g⁻¹ : MulAut M) : (a : M) → M) k : M)

Tactic:
apply Set.conj_mem_fixingSubgroup _ hk

Premises used: Set.conj_mem_fixingSubgroup
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
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
rw₁ rw₂ : s = s
⊢ g⁻¹ • s = t

Tactic:
rw [inv_smul_eq_iff, hg]

Premises used: inv_smul_eq_iff
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
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 : g * (g⁻¹ * k * g) * g⁻¹ = 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

Tactic:
simp [MulAut.conj]

Premises used: MulAut.conj
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
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 * (g⁻¹ * k * g) * g⁻¹ = k

Tactic:
group
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
g : M
⊢ Eq (α := Subgroup M) (fixingSubgroup M (g • s))
    (Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : M) → MulAut M) g)) (fixingSubgroup M s))

Tactic:
(fixingSubgroup_map_conj_eq rfl).symm

Premises used: SubMulAction.fixingSubgroup_map_conj_eq, Eq.symm, 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 α
g : M
hg : g • t = s
x : ↥(fixingSubgroup M t)
⊢ Eq (α := M)
    ((↑((fixingSubgroupEquivFixingSubgroup (s := s) (t := t) hg : (a : ↥(fixingSubgroup M t)) → ↥(fixingSubgroup M s))
            x) :
        M) :
      M)
    ((((MulAut.conj : (a : M) → MulAut M) g : MulAut M) : (a : M) → M) (↑x : M) : M)

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_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
apply : x ∈ t
⊢ False

Tactic:
apply hx
-- 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 α
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
⊢ g • x ∈ g • t

Tactic:
rw [← hg] at hgxt
-- 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 α
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 ∈ g • t
⊢ x ∈ t

Tactic:
Set.smul_mem_smul_set_iff.mp hgxt

Premises used: Iff.mp, Set.smul_mem_smul_set_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 α
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 ∈ g • t
⊢ x ∈ t

Tactic:
exact Set.smul_mem_smul_set_iff.mp hgxt

Premises used: Iff.mp, Set.smul_mem_smul_set_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 α
g : M
hg : g • t = s
x_1 : ↥(fixingSubgroup M t)
x_2 : ↥(ofFixingSubgroup M t)
m : M
hm : Membership.mem (γ := Subgroup M) (fixingSubgroup M t) m
x : α
hx : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M t)) α) (ofFixingSubgroup M t) x
⊢ (match (motive := ↥(ofFixingSubgroup M t) → ↥(ofFixingSubgroup M s))
      Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M t) x) m hm •
        Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M t)) α) (ofFixingSubgroup M t) x) x hx with
    | ⟨x, hx⟩ =>
      Subtype.mk (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) (g • x) ⋯) =
    HSMul.hSMul (α := ↥(fixingSubgroup M s)) (β := ↥(ofFixingSubgroup M s))
      ((fixingSubgroupEquivFixingSubgroup (s := s) (t := t) hg : (a : ↥(fixingSubgroup M t)) → ↥(fixingSubgroup M s))
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M t) x) m hm) :
        ↥(fixingSubgroup M s))
      (match (motive := ↥(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 with
        | ⟨x, hx⟩ =>
          Subtype.mk (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) (g • x)
            ⋯ :
        ↥(ofFixingSubgroup M s))

Tactic:
simp only [← SetLike.coe_eq_coe, subgroup_smul_def,
      SetLike.val_smul,
      fixingSubgroupEquivFixingSubgroup_coe_apply,
      MulAut.conj_apply, mul_smul, inv_smul_smul]

Premises used: SetLike.coe_eq_coe, inv_smul_smul, MulAut.conj_apply, SetLike.val_smul, MulAction.subgroup_smul_def, SubMulAction.fixingSubgroupEquivFixingSubgroup_coe_apply, 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 t : Set α
g : M
hg : g • t = s
x : ↥(ofFixingSubgroup M t)
⊢ (↑((conjMap_ofFixingSubgroup (s := s) (t := t) hg : (a : ↥(ofFixingSubgroup M t)) → ↥(ofFixingSubgroup M s)) x) : α) =
    g • (↑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 α
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))
right :
  Surjective (α := ↥(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))

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 α
g : M
hst : g • s = t
x y : ↥(ofFixingSubgroup M s)
hxy :
  Eq (α := ↥(ofFixingSubgroup M t))
    ((conjMap_ofFixingSubgroup (s := t) (t := s) hst : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup M t)) x :
      ↥(ofFixingSubgroup M t))
    ((conjMap_ofFixingSubgroup (s := t) (t := s) hst : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup M t)) y :
      ↥(ofFixingSubgroup M t))
⊢ x = y

Tactic:
simpa [← SetLike.coe_eq_coe] using hxy

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 α
g : M
hst : g • s = t
x : α
hx : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M t)) α) (ofFixingSubgroup M t) x
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
⊢ ∃ (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

Premises used: inv_smul_eq_iff, eq_comm
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
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
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
⊢ ∃ (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

Tactic:
use (SubMulAction.conjMap_ofFixingSubgroup hst) ⟨x, hx⟩

Premises used: SubMulAction.conjMap_ofFixingSubgroup, Subtype.mk, DFunLike.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 α
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
⊢ (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:
simp [← 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 t : Set α
g : M
⊢ Membership.mem (γ := Subgroup M) (fixingSubgroup M (s ∪ t)) g ↔
    Membership.mem (γ := Subgroup M) (fixingSubgroup M s) g ∧ Membership.mem (γ := Subgroup M) (fixingSubgroup M t) g

Tactic:
simp [fixingSubgroup_union, Subgroup.mem_inf]

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))
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