How to use defining property of a submonoid?

Stream: new members

[Scott Carnahan]

I'm trying to use set-wise stabilizers, but I got suck trying to used the submonoid I defined:

import Mathlib.GroupTheory.GroupAction.Defs

variable (M : Type u) {α : Type v} [Monoid M] [MulAction M α]

def setStabilizerMonoid (s : Set α) : Submonoid M :=
  {
    carrier := { g | ∀ (x : α), x ∈ s ↔ g • x ∈ s }
    one_mem' := by
      sorry -- not too hard
    mul_mem' := by
      sorry -- a little tricky
  }

theorem setStabilizerIff (s : Set α) (g : setStabilizerMonoid M s) (x : α) : x ∈ s ↔ g • x ∈ s := by
  sorry -- My normal approach is useless here

[Eric Wieser]

Does this help?

theorem setStabilizerIff (s : Set α) (g : setStabilizerMonoid M s) (x : α) : x ∈ s ↔ g • x ∈ s := by
  have : ∀ (x : α), x ∈ s ↔ g • x ∈ s := g.prop
  sorry

[Eric Wieser]

Note that docs#stabilizerSubmonoid already exists, but I assume you were writing it as an exercise

[Eric Wieser]

(also, it seems for your code to work in the latest mathlib, it needs import Mathlib.GroupTheory.GroupAction.Basic)

[Eric Wieser]

The have there is a bit magic; normally instead of pulling the statement of thin air, you'd write an API lemma:

def setStabilizerMonoid (s : Set α) : Submonoid M where
  carrier := { g | ∀ (x : α), x ∈ s ↔ g • x ∈ s }
  one_mem' := by
    sorry -- not too hard
  mul_mem' := by
    sorry -- a little tricky

-- this is the API lemma, and you should write it as soon as possible after the `def`
@[simp]
theorem mem_setStabilizerMonoid_iff {s : Set α} {g : M} :
    g ∈ setStabilizerMonoid M s ↔ ∀ (x : α), x ∈ s ↔ g • x ∈ s :=
  Iff.rfl

theorem setStabilizerIff (s : Set α) (g : setStabilizerMonoid M s) (x : α) : x ∈ s ↔ g • x ∈ s := by
  have := g.prop
  rw [mem_setStabilizerMonoid_iff] at this
  sorry