awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
g h : G
h₁ : ∀ (a : α), a ∈ h • fixedBy α g ↔ a ∈ fixedBy α (h * g * h⁻¹)
⊢ h • fixedBy α g = fixedBy α (h * g * h⁻¹)

Tactic:
ext a
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
g h : G
a : α
h₁ : h⁻¹ • a ∈ fixedBy α g ↔ a ∈ fixedBy α (h * g * h⁻¹)
h₂ : g • h⁻¹ • a = h⁻¹ • a ↔ (h * g * h⁻¹) • a = a
h₃ : g • h⁻¹ • a = h⁻¹ • a ↔ h • g • h⁻¹ • a = a
⊢ a ∈ h • fixedBy α g ↔ a ∈ fixedBy α (h * g * h⁻¹)

Tactic:
simp_rw [Set.mem_smul_set_iff_inv_smul_mem, mem_fixedBy, mul_smul, smul_eq_iff_eq_inv_smul h]

Premises used: Set.mem_smul_set_iff_inv_smul_mem, smul_eq_iff_eq_inv_smul, SemigroupAction.mul_smul, MulAction.mem_fixedBy
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
M : Type u_3
inst : Monoid M
inst_1 : IsRightCancelMul M
m : M
⊢ fixedBy M m = ∅ ↔ m ≠ 1

Tactic:
simp [MulAction.fixedBy, Set.eq_empty_iff_forall_notMem]

Premises used: MulAction.fixedBy, Set.eq_empty_iff_forall_notMem
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
M : Type u_3
inst : Monoid M
inst_1 : IsLeftCancelMul M
m : M
⊢ fixedBy M (MulOpposite.op m) = ∅ ↔ m ≠ 1

Tactic:
simp [MulAction.fixedBy, Set.eq_empty_iff_forall_notMem]

Premises used: MulAction.fixedBy, Set.eq_empty_iff_forall_notMem
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
simp_rw : g • s = s ↔ ∀ (x : α), g • x ∈ s ↔ x ∈ s
simp_rw₁ : s = g⁻¹ • s ↔ ∀ (x : α), g • x ∈ s ↔ x ∈ s
simp_rw₂ : (∀ (x : α), x ∈ s ↔ x ∈ g⁻¹ • s) ↔ ∀ (x : α), g • x ∈ s ↔ x ∈ s
simp_rw₃ : (∀ (x : α), x ∈ s ↔ g • x ∈ s) ↔ ∀ (x : α), g • x ∈ s ↔ x ∈ s
⊢ Membership.mem (γ := Set (Set α)) (fixedBy (Set α) g) s ↔ ∀ (x : α), g • x ∈ s ↔ x ∈ s

Tactic:
simp_rw [mem_fixedBy, ← eq_inv_smul_iff, Set.ext_iff, Set.mem_inv_smul_set_iff, Iff.comm]

Premises used: Set.mem_inv_smul_set_iff, Iff.comm, Set.ext_iff, MulAction.mem_fixedBy, eq_inv_smul_iff
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
s_in_fixedBy : Membership.mem (γ := Set (Set α)) (fixedBy (Set α) g) s
x : α
⊢ g • x ∈ s ↔ x ∈ s

Tactic:
(set_mem_fixedBy_iff s g).mp s_in_fixedBy x

Premises used: MulAction.set_mem_fixedBy_iff, Iff.mp
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
s_ss_fixedBy : s ⊆ fixedBy α g
rw : Membership.mem (γ := Set (Set α)) (fixedBy (Set α) g⁻¹) s
⊢ Membership.mem (γ := Set (Set α)) (fixedBy (Set α) g) s

Tactic:
rw [← fixedBy_inv]

Premises used: MulAction.fixedBy_inv
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
s_ss_fixedBy : s ⊆ fixedBy α g
h : ∀ (x : α), x ∈ g⁻¹ • s ↔ x ∈ s
⊢ Membership.mem (γ := Set (Set α)) (fixedBy (Set α) g⁻¹) s

Tactic:
ext x
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
s_ss_fixedBy : s ⊆ fixedBy α g
x : α
h : g • x ∈ s ↔ x ∈ s
⊢ x ∈ g⁻¹ • s ↔ x ∈ s

Tactic:
rw [Set.mem_inv_smul_set_iff]

Premises used: Set.mem_inv_smul_set_iff
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
s_ss_fixedBy : s ⊆ fixedBy α g
x : α
⊢ g • x ∈ s ↔ x ∈ s

Tactic:
⟨fun gxs => ?xs, fun xs => (s_ss_fixedBy xs).symm ▸ xs⟩

Premises used: Eq.rec, Iff.intro, Eq.symm
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
s_ss_fixedBy : s ⊆ fixedBy α g
x : α
xs : ∀ (gxs : g • x ∈ s), x ∈ s
⊢ g • x ∈ s ↔ x ∈ s

Tactic:
refine ⟨fun gxs => ?xs, fun xs => (s_ss_fixedBy xs).symm ▸ xs⟩
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
s_ss_fixedBy : s ⊆ fixedBy α g
x : α
gxs : g • x ∈ s
xs : ∀ (s_ss_fixedBy : s ⊆ fixedBy α g⁻¹) (x : α) (gxs : g • x ∈ s), x ∈ s
⊢ x ∈ s

Tactic:
rw [← fixedBy_inv] at s_ss_fixedBy

Premises used: MulAction.fixedBy_inv
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
s_ss_fixedBy : s ⊆ fixedBy α g⁻¹
x : α
gxs : g • x ∈ s
xs : ∀ (gxs : g⁻¹ • g • x ∈ s), x ∈ s
xs₁ xs₂ xs₃ xs₄ : ∀ (gxs : x ∈ s), x ∈ s
⊢ x ∈ s

Tactic:
rwa [← s_ss_fixedBy gxs, inv_smul_smul] at gxs

Premises used: inv_smul_smul
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s t : Set α
g : G
t_ss_s : t ⊆ s
s_in_fixedBy : Membership.mem (γ := Set (Set α)) (fixedBy (Set α) g) s
⊢ g • t ⊆ s

Tactic:
(Set.smul_set_subset_smul_set_iff.mpr t_ss_s).trans s_in_fixedBy.subset

Premises used: Iff.mpr, HasSubset.Subset.trans, Eq.subset, Set.smul_set_subset_smul_set_iff
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
rw : Membership.mem (γ := Set (Set α)) (fixedBy (Set α) g⁻¹) s
⊢ Membership.mem (γ := Set (Set α)) (fixedBy (Set α) g) s

Tactic:
rw [← fixedBy_inv]

Premises used: MulAction.fixedBy_inv
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
h : ∀ (a : α), a ∈ g⁻¹ • s ↔ a ∈ s
⊢ Membership.mem (γ := Set (Set α)) (fixedBy (Set α) g⁻¹) s

Tactic:
ext a
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
a : α
h : g • a ∈ s ↔ a ∈ s
⊢ a ∈ g⁻¹ • s ↔ a ∈ s

Tactic:
rw [Set.mem_inv_smul_set_iff]

Premises used: Set.mem_inv_smul_set_iff
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
a : α
pos : a ∈ fixedBy α g → (g • a ∈ s ↔ a ∈ s)
neg : a ∉ fixedBy α g → (g • a ∈ s ↔ a ∈ s)
⊢ g • a ∈ s ↔ a ∈ s

Tactic:
by_cases a ∈ fixedBy α g

Premises used: MulAction.fixedBy
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
a : α
a_fixed : a ∈ fixedBy α g
rw rw₁ : a ∈ s ↔ a ∈ s
⊢ g • a ∈ s ↔ a ∈ s

Tactic:
rw [a_fixed]
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
a : α
h : a ∈ fixedBy α g
⊢ g • a ∈ s ↔ a ∈ s

Tactic:
case pos a_fixed =>
    rw [a_fixed]
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
a : α
a_moved : a ∉ fixedBy α g
mp : g • a ∈ s → a ∈ s
mpr : a ∈ s → g • a ∈ s
⊢ g • a ∈ s ↔ a ∈ s

Tactic:
constructor
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
a : α
a_moved : a ∉ fixedBy α g
h : g • a ∈ s
mp : a ∈ (fixedBy α g)ᶜ
⊢ a ∈ s

Tactic:
apply s_subset
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
a : α
a_moved : a ∉ fixedBy α g
h : a ∈ s
mpr : g • a ∈ (fixedBy α g)ᶜ
⊢ g • a ∈ s

Tactic:
apply s_subset
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
a : α
a_moved : a ∉ fixedBy α g
h : g • a ∈ s
⊢ a ∈ (fixedBy α g)ᶜ

Tactic:
a_moved

Premises used: Set.Mem, setOf, Not
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
a : α
a_moved : a ∉ fixedBy α g
h : g • a ∈ s
⊢ a ∈ (fixedBy α g)ᶜ

Tactic:
exact a_moved
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
a : α
a_moved : a ∉ fixedBy α g
h : a ∈ s
mpr : g • a ∉ fixedBy α g
mpr₁ mpr₂ mpr₃ mpr₄ : a ∉ fixedBy α g
⊢ g • a ∈ (fixedBy α g)ᶜ

Tactic:
rwa [Set.mem_compl_iff, smul_mem_fixedBy_iff_mem_fixedBy]

Premises used: MulAction.smul_mem_fixedBy_iff_mem_fixedBy, Set.mem_compl_iff
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
g h : G
comm : Commute g h
h₁ : ∀ (x : α), x ∈ h • fixedBy α g ↔ x ∈ fixedBy α g
⊢ Membership.mem (γ := Set (Set α)) (fixedBy (Set α) h) (fixedBy α g)

Tactic:
ext x
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
g h : G
comm : Commute g h
x : α
h₁ : h⁻¹ • x ∈ fixedBy α g ↔ x ∈ fixedBy α g
h₂ : g • h⁻¹ • x = h⁻¹ • x ↔ x ∈ fixedBy α g
h₃ : (g * h⁻¹) • x = h⁻¹ • x ↔ x ∈ fixedBy α g
h₄ : (h⁻¹ * g) • x = h⁻¹ • x ↔ x ∈ fixedBy α g
h₅ : h⁻¹ • g • x = h⁻¹ • x ↔ x ∈ fixedBy α g
h₆ : g • x = x ↔ x ∈ fixedBy α g
h₇ h₈ : g • x = x ↔ g • x = x
⊢ x ∈ h • fixedBy α g ↔ x ∈ fixedBy α g

Tactic:
rw [Set.mem_smul_set_iff_inv_smul_mem, mem_fixedBy, ← mul_smul, comm.inv_right, mul_smul,
    smul_left_cancel_iff, mem_fixedBy]

Premises used: Set.mem_smul_set_iff_inv_smul_mem, SemigroupAction.mul_smul, smul_left_cancel_iff, MulAction.mem_fixedBy, Commute.inv_right
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
g h : G
comm : Commute g h
j : ℤ
⊢ h ^ j • fixedBy α g = fixedBy α g

Tactic:
fixedBy_subset_fixedBy_zpow (Set α) h j (fixedBy_mem_fixedBy_of_commute comm)

Premises used: Set.Mem, setOf, MulAction.fixedBy, MulAction.fixedBy_mem_fixedBy_of_commute, MulAction.fixedBy_subset_fixedBy_zpow, Set
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
g h : G
comm : Commute g h
rw : h • (fixedBy α g)ᶜ = (fixedBy α g)ᶜ
rw₁ : (h • fixedBy α g)ᶜ = (fixedBy α g)ᶜ
rw₂ rw₃ : (fixedBy α g)ᶜ = (fixedBy α g)ᶜ
⊢ Membership.mem (γ := Set (Set α)) (fixedBy (Set α) h) (fixedBy α g)ᶜ

Tactic:
rw [mem_fixedBy, Set.smul_set_compl, fixedBy_mem_fixedBy_of_commute comm]

Premises used: Set.smul_set_compl, MulAction.fixedBy_mem_fixedBy_of_commute, MulAction.mem_fixedBy
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
g h : G
comm : Commute g h
j : ℤ
⊢ h ^ j • (fixedBy α g)ᶜ = (fixedBy α g)ᶜ

Tactic:
fixedBy_subset_fixedBy_zpow (Set α) h j (movedBy_mem_fixedBy_of_commute comm)

Premises used: Set.Mem, setOf, MulAction.fixedBy, MulAction.fixedBy_subset_fixedBy_zpow, MulAction.movedBy_mem_fixedBy_of_commute, Set
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : MulAction M α
inst_2 : FaithfulSMul M α
m : M
rw :
  (∀ (x : α), x ∈ fixedBy α m) ↔
    Eq.{u_1 + 1} (α := α → α) (fun (x2 : α) ↦ m • x2) fun (x2 : α) ↦ HSMul.hSMul.{u_3, u_1, u_1} (α := M) 1 x2
⊢ fixedBy α m = Set.univ ↔ m = 1

Tactic:
rw [← (smul_left_injective' (M := M) (α := α)).eq_iff, Set.eq_univ_iff_forall]

Premises used: smul_left_injective', Set.eq_univ_iff_forall, Function.Injective.eq_iff
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : MulAction M α
inst_2 : FaithfulSMul M α
m : M
simp_rw : (∀ (x : α), x ∈ fixedBy α m) ↔ ∀ (x : α), m • x = HSMul.hSMul.{u_3, u_1, u_1} (α := M) 1 x
simp_rw₁ : (∀ (x : α), x ∈ fixedBy α m) ↔ ∀ (x : α), m • x = x
⊢ (∀ (x : α), x ∈ fixedBy α m) ↔
    Eq.{u_1 + 1} (α := α → α) (fun (x2 : α) ↦ m • x2) fun (x2 : α) ↦ HSMul.hSMul.{u_3, u_1, u_1} (α := M) 1 x2

Tactic:
simp_rw [funext_iff, one_smul, mem_fixedBy]

Premises used: funext_iff, one_smul, MulAction.mem_fixedBy
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : FaithfulSMul G α
g h : G
ne_one : g ≠ 1
disjoint : Disjoint (fixedBy α g)ᶜ (h • (fixedBy α g)ᶜ)
contrapose : ∀ (comm : Commute g h), g = 1
⊢ ¬Commute g h

Tactic:
contrapose ne_one with comm

Premises used: comm
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : FaithfulSMul G α
g h : G
disjoint : Disjoint (fixedBy α g)ᶜ (h • (fixedBy α g)ᶜ)
comm : Commute g h
rwa : ∀ (disjoint : Disjoint (fixedBy α g)ᶜ (fixedBy α g)ᶜ) (comm : Commute g h), g = 1
rwa₁ : ∀ (disjoint : (fixedBy α g)ᶜ = ⊥) (comm : Commute g h), g = 1
rwa₂ : ∀ (disjoint : (fixedBy α g)ᶜ = ∅) (comm : Commute g h), g = 1
rwa₃ : ∀ (disjoint : (fixedBy α g)ᶜ = Set.univᶜ) (comm : Commute g h), g = 1
rwa₄ : ∀ (disjoint : fixedBy α g = Set.univ) (comm : Commute g h), g = 1
rwa₅ rwa₆ rwa₇ rwa₈ : ∀ (disjoint : g = 1) (comm : Commute g h), g = 1
⊢ g = 1

Tactic:
rwa [movedBy_mem_fixedBy_of_commute comm, disjoint_self, Set.bot_eq_empty, ← Set.compl_univ,
    compl_inj_iff, fixedBy_eq_univ_iff_eq_one] at disjoint

Premises used: Set.bot_eq_empty, Set.compl_univ, compl_inj_iff, disjoint_self, MulAction.fixedBy_eq_univ_iff_eq_one, MulAction.movedBy_mem_fixedBy_of_commute
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
G : Type u_1
A : Type u_2
B : Type u_3
inst : Monoid G
inst_1 : MulAction G A
inst_2 : MulAction G B
f : MulActionHom.{u_1, u_1, u_2, u_3} (M := G) id A B
H : Submonoid G
a : A
ha : a ∈ MulAction.fixedPoints.{u_1, u_2} (↥H) A
h : G
property : h ∈ H
⊢ HSMul.hSMul (β := B) (Subtype.mk (p := fun (x : G) ↦ x ∈ H) h property) ((f : (a : A) → B) a : B) =
    (f : (a : A) → B) a

Tactic:
simp_all [← f.map_smul h a]

Premises used: MulActionHom.map_smul
-- Module: Mathlib.GroupTheory.GroupAction.FixedPoints
Goal:
G : Type u_1
A : Type u_2
B : Type u_3
inst : Monoid G
inst_1 : MulAction G A
inst_2 : MulAction G B
f : MulActionHom.{u_1, u_1, u_2, u_3} (M := G) id A B
g : G
a : A
ha : a ∈ MulAction.fixedBy A g
⊢ Membership.mem (α := B) (MulAction.fixedBy B g) ((f : (a : A) → B) a : B)

Tactic:
simpa using congr_arg f ha

Premises used: congr_arg, DFunLike.coe
-- Module: Mathlib.GroupTheory.GroupAction.FixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Monoid M
inst_1 : MulAction M α
s : Set α
x y : M
hx : Membership.mem (γ := Set M) {ϕ : M | ∀ (x : (↑s : Type u_2)), ϕ • (↑x : α) = (↑x : α)} x
hy : Membership.mem (γ := Set M) {ϕ : M | ∀ (x : (↑s : Type u_2)), ϕ • (↑x : α) = (↑x : α)} y
z : (↑s : Type u_2)
rw : x • y • (↑z : α) = (↑z : α)
rw₁ : x • (↑z : α) = (↑z : α)
rw₂ rw₃ : (↑z : α) = (↑z : α)
⊢ (x * y) • (↑z : α) = (↑z : α)

Tactic:
rw [mul_smul, hy z, hx z]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.GroupTheory.GroupAction.FixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Monoid M
inst_1 : MulAction M α
s : Set α
m : M
⊢ Membership.mem (γ := Submonoid M) (fixingSubmonoid M s) m ↔ ∀ y ∈ s, m • y = y

Tactic:
⟨fun hg y hy => hg ⟨y, hy⟩, fun h ⟨y, hy⟩ => h y hy⟩

Premises used: _private.0.mem_fixingSubmonoid_iff.match_1, Subtype.mk, Iff.intro, HSMul.hSMul, Subtype.val, Eq
-- Module: Mathlib.GroupTheory.GroupAction.FixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Monoid M
inst_1 : MulAction M α
⊢ GaloisConnection.{u_2, u_1} (α := Set α) (β := (Submonoid M)ᵒᵈ)
    (Function.comp (β := Submonoid M) (⇑OrderDual.toDual : (a : Submonoid M) → (Submonoid M)ᵒᵈ) (fixingSubmonoid M))
    ((fun (P : Submonoid M) ↦ fixedPoints.{u_1, u_2} (↥P) α) ∘
      (⇑OrderDual.ofDual : (a : (Submonoid M)ᵒᵈ) → Submonoid M))

Tactic:
fun _s _P => ⟨fun h s hs p => h p.2 ⟨s, hs⟩, fun h p hp s => h s.2 ⟨p, hp⟩⟩

Premises used: Subtype.mk, Iff.intro, Subtype.property, GaloisConnection
-- Module: Mathlib.GroupTheory.GroupAction.FixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Monoid M
inst_1 : MulAction M α
⊢ Antitone.{u_2, u_1} (β := Submonoid M) fun (s : Set α) ↦ fixingSubmonoid M s

Tactic:
(fixingSubmonoid_fixedPoints_gc M α).monotone_l

Premises used: Set.Mem, Antitone, fixingSubmonoid_fixedPoints_gc, GaloisConnection.monotone_l
-- Module: Mathlib.GroupTheory.GroupAction.FixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Monoid M
inst_1 : MulAction M α
⊢ Antitone.{u_1, u_2} (β := Set α) fun (P : Submonoid M) ↦ fixedPoints.{u_1, u_2} (↥P) α

Tactic:
(fixingSubmonoid_fixedPoints_gc M α).monotone_u.dual_left

Premises used: GaloisConnection.monotone_u, Set.Mem, setOf, Monotone.dual_left, fixingSubmonoid_fixedPoints_gc, OrderDual, MulAction.fixedPoints
-- Module: Mathlib.GroupTheory.GroupAction.FixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Monoid M
inst_1 : MulAction M α
s t : Set α
⊢ Eq (α := Submonoid M) (fixingSubmonoid M (s ∪ t)) (fixingSubmonoid M s ⊓ fixingSubmonoid M t)

Tactic:
(fixingSubmonoid_fixedPoints_gc M α).l_sup

Premises used: setOf, fixingSubmonoid, fixingSubmonoid_fixedPoints_gc, OrderDual, GaloisConnection.l_sup
-- Module: Mathlib.GroupTheory.GroupAction.FixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Monoid M
inst_1 : MulAction M α
ι : Sort u_3
s : ι → Set α
⊢ Eq (α := Submonoid M) (fixingSubmonoid.{u_1, u_2} M (α := α) (⋃ (i : ι), s i)) (⨅ (i : ι), fixingSubmonoid M (s i))

Tactic:
(fixingSubmonoid_fixedPoints_gc M α).l_iSup

Premises used: iInf, Set.Mem, setOf, fixingSubmonoid, GaloisConnection.l_iSup, fixingSubmonoid_fixedPoints_gc, OrderDual, Set.iUnion
-- Module: Mathlib.GroupTheory.GroupAction.FixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Monoid M
inst_1 : MulAction M α
P Q : Submonoid M
⊢ fixedPoints.{u_1, u_2} (↥(P ⊔ Q)) α = fixedPoints.{u_1, u_2} (↥P) α ∩ fixedPoints.{u_1, u_2} (↥Q) α

Tactic:
(fixingSubmonoid_fixedPoints_gc M α).u_inf

Premises used: Set.Mem, setOf, GaloisConnection.u_inf, fixingSubmonoid_fixedPoints_gc, MulAction.fixedPoints
-- Module: Mathlib.GroupTheory.GroupAction.FixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Monoid M
inst_1 : MulAction M α
ι : Sort u_3
P : ι → Submonoid M
⊢ fixedPoints.{u_1, u_2} (↥(iSup P)) α = ⋂ (i : ι), fixedPoints.{u_1, u_2} (↥(P i)) α

Tactic:
(fixingSubmonoid_fixedPoints_gc M α).u_iInf

Premises used: Set.Mem, Set.iInter, setOf, GaloisConnection.u_iInf, fixingSubmonoid_fixedPoints_gc, OrderDual, MulAction.fixedPoints
-- Module: Mathlib.GroupTheory.GroupAction.FixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
x : M
hx : x ∈ Subsemigroup.carrier (Submonoid.toSubsemigroup (fixingSubmonoid M s))
z : (↑s : Type u_2)
rw : (↑z : α) = x • (↑z : α)
rw₁ rw₂ : (↑z : α) = (↑z : α)
⊢ x⁻¹ • (↑z : α) = (↑z : α)

Tactic:
rw [inv_smul_eq_iff, hx z]

Premises used: inv_smul_eq_iff
-- Module: Mathlib.GroupTheory.GroupAction.FixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
m : M
⊢ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) m ↔ ∀ y ∈ s, m • y = y

Tactic:
⟨fun hg y hy => hg ⟨y, hy⟩, fun h ⟨y, hy⟩ => h y hy⟩

Premises used: _private.0.mem_fixingSubmonoid_iff.match_1, Subtype.mk, Iff.intro, HSMul.hSMul, Subtype.val, Eq
-- Module: Mathlib.GroupTheory.GroupAction.FixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
m : M
simp_rw : (∀ y ∈ s, m • y = y) ↔ s ⊆ fixedBy α m
simp_rw₁ : (∀ y ∈ s, m • y = y) ↔ ∀ x ∈ s, x ∈ fixedBy α m
⊢ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) m ↔ s ⊆ fixedBy α m

Tactic:
simp_rw [mem_fixingSubgroup_iff, Set.subset_def, mem_fixedBy]

Premises used: Set.subset_def, mem_fixingSubgroup_iff, MulAction.mem_fixedBy
-- Module: Mathlib.GroupTheory.GroupAction.FixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
m : M
rw : sᶜ ⊆ fixedBy α m ↔ (fixedBy α m)ᶜ ⊆ s
rw₁ rw₂ : (fixedBy α m)ᶜ ⊆ s ↔ (fixedBy α m)ᶜ ⊆ s
⊢ Membership.mem (γ := Subgroup M) (fixingSubgroup M sᶜ) m ↔ (fixedBy α m)ᶜ ⊆ s

Tactic:
rw [mem_fixingSubgroup_iff_subset_fixedBy, Set.compl_subset_comm]

Premises used: Set.compl_subset_comm, mem_fixingSubgroup_iff_subset_fixedBy
-- Module: Mathlib.GroupTheory.GroupAction.FixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
⊢ GaloisConnection.{u_2, u_1} (α := Set α) (β := (Subgroup M)ᵒᵈ)
    (Function.comp (β := Subgroup M) (⇑OrderDual.toDual : (a : Subgroup M) → (Subgroup M)ᵒᵈ) (fixingSubgroup M))
    ((fun (P : Subgroup M) ↦ fixedPoints.{u_1, u_2} (↥P) α) ∘ (⇑OrderDual.ofDual : (a : (Subgroup M)ᵒᵈ) → Subgroup M))

Tactic:
fun _s _P => ⟨fun h s hs p => h p.2 ⟨s, hs⟩, fun h p hp s => h s.2 ⟨p, hp⟩⟩

Premises used: Subtype.mk, Iff.intro, Subtype.property, GaloisConnection
-- Module: Mathlib.GroupTheory.GroupAction.FixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
⊢ Eq (α := Subgroup M) (fixingSubgroup.{u_1, u_2} M (α := α) ∅) ⊤

Tactic:
GaloisConnection.l_bot (fixingSubgroup_fixedPoints_gc M α)

Premises used: fixingSubgroup, GaloisConnection.l_bot, fixingSubgroup_fixedPoints_gc, OrderDual
-- Module: Mathlib.GroupTheory.GroupAction.FixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
⊢ Antitone.{u_2, u_1} (α := Set α) (β := Subgroup M) (fixingSubgroup M)

Tactic:
(fixingSubgroup_fixedPoints_gc M α).monotone_l

Premises used: Set.Mem, Antitone, fixingSubgroup_fixedPoints_gc, GaloisConnection.monotone_l
-- Module: Mathlib.GroupTheory.GroupAction.FixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
⊢ Antitone.{u_1, u_2} (β := Set α) fun (P : Subgroup M) ↦ fixedPoints.{u_1, u_2} (↥P) α

Tactic:
(fixingSubgroup_fixedPoints_gc M α).monotone_u.dual_left

Premises used: GaloisConnection.monotone_u, Set.Mem, setOf, Monotone.dual_left, fixingSubgroup_fixedPoints_gc, OrderDual, MulAction.fixedPoints
-- Module: Mathlib.GroupTheory.GroupAction.FixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s t : Set α
⊢ Eq (α := Subgroup M) (fixingSubgroup M (s ∪ t)) (fixingSubgroup M s ⊓ fixingSubgroup M t)

Tactic:
(fixingSubgroup_fixedPoints_gc M α).l_sup

Premises used: fixingSubgroup, fixingSubgroup_fixedPoints_gc, OrderDual, GaloisConnection.l_sup
-- Module: Mathlib.GroupTheory.GroupAction.FixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
ι : Sort u_3
s : ι → Set α
⊢ Eq (α := Subgroup M) (fixingSubgroup.{u_1, u_2} M (α := α) (⋃ (i : ι), s i)) (⨅ (i : ι), fixingSubgroup M (s i))

Tactic:
(fixingSubgroup_fixedPoints_gc M α).l_iSup

Premises used: iInf, Set.Mem, fixingSubgroup, GaloisConnection.l_iSup, fixingSubgroup_fixedPoints_gc, OrderDual, Set.iUnion
-- Module: Mathlib.GroupTheory.GroupAction.FixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
P Q : Subgroup M
⊢ fixedPoints.{u_1, u_2} (↥(P ⊔ Q)) α = fixedPoints.{u_1, u_2} (↥P) α ∩ fixedPoints.{u_1, u_2} (↥Q) α

Tactic:
(fixingSubgroup_fixedPoints_gc M α).u_inf

Premises used: Set.Mem, setOf, GaloisConnection.u_inf, fixingSubgroup_fixedPoints_gc, MulAction.fixedPoints
-- Module: Mathlib.GroupTheory.GroupAction.FixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
ι : Sort u_3
P : ι → Subgroup M
⊢ fixedPoints.{u_1, u_2} (↥(iSup P)) α = ⋂ (i : ι), fixedPoints.{u_1, u_2} (↥(P i)) α

Tactic:
(fixingSubgroup_fixedPoints_gc M α).u_iInf

Premises used: Set.Mem, Set.iInter, setOf, GaloisConnection.u_iInf, fixingSubgroup_fixedPoints_gc, OrderDual, MulAction.fixedPoints
-- Module: Mathlib.GroupTheory.GroupAction.FixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
a : α
a_in_s : a ∈ s
b : α
b_in_orbit : b ∈ orbit.{u_1, u_2} (↥(fixingSubgroup M sᶜ)) a
let :
  ∀ (g : M) (g_fixing : Membership.mem (γ := Subgroup M) (fixingSubgroup M sᶜ) g)
    (g_eq :
      Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M sᶜ) x) g g_fixing • a = b),
    b ∈ s
⊢ b ∈ s

Tactic:
let ⟨⟨g, g_fixing⟩, g_eq⟩ := MulAction.mem_orbit_iff.mp b_in_orbit