[Merged by Bors] - feat(group_theory/group_action/sub_mul_action): orbit and stabilizer lemmas

[AntoineChambert-Loir]

Feat: add lemmas for stabilizer and orbit for sub_mul_action

---

[eric-wieser]

This lemma is a tautology, both sides are syntactically identical. Did you mean

lemma coe_image_orbit {p : sub_mul_action R M} (m : p) :
  coe '' mul_action.orbit R m = mul_action.orbit R (m : M) :=
(set.range_comp _ _).symm

[AntoineChambert-Loir]

Actually, I meant what I had written, because at some point I felt it had to exist.
(It is not clear to me why the orbit, a member of (set p), is automatically viewed as a member of (set M).
Let me try to understand what you wrote.

[AntoineChambert-Loir]

(I switched my lemma to yours, but it is not clear to me why the first one in syntactically obvious and not yours…)

[eric-wieser]

(It is not clear to me why the orbit, a member of (set p), is automatically viewed as a member of (set M).

That's precisely the problem, that's not what you asked lean to do. When you write (mul_action.orbit R m : set M), that means "mul_action.orbit R m will be a term of type set M", from which the elaborator concludes "m must be a term of type M", and replaces it with ↑m".

My guess is that you thought you'd written something equivalent to (↑(mul_action.orbit R m) : set M),
Which doesn't work because no such automatic coercion exists

[eric-wieser]

it is not clear to me why the first one in syntactically obvious and not yours

Put your cursor after the := in your original lemma. The goal view will show that both sides are already exactly the same.

[AntoineChambert-Loir]

You taught me something about how Lean's elaborator “thinks”.
I really expected that seeing (mul_action.orbit R m : set M)', it would want to make (mul_action.orbit R m)' a member of `set M'.

[AntoineChambert-Loir]

Actually, I wrote this lemma by a mere desire of completing the square (If something is proven about stabilizer, something about orbits has to, and the lemma for orbits was the wrong one, as you observed!), but I don't think I had to use it.

[eric-wieser]

You seem to have removed the --- from the PR description, which separates what bors will put in the commit from things like the gitpod button that do not belong in the commit.

[AntoineChambert-Loir]

Is this better now?

[riccardobrasca]

Thanks!

bors d+

[bors]

✌️ AntoineChambert-Loir can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[AntoineChambert-Loir]

bors r+

[bors]

This PR was included in a batch that was canceled, it will be automatically retried

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests