simp for MulAut.inv_def

Stream: mathlib4

[Antoine Chambert-Loir]

Would it be reasonable to have:

@[simp]
theorem MulAut.inv_apply {M : Type*} [Mul M] (e : MulAut M) (x : M) :
      e⁻¹ x = e.symm x := by
  rw [MulAut.inv_def]

or even a simp tag on docs#MulAut.inv_def

[Eric Wieser]

inv_apply (and same for mul, one) looks good to me, under the premise that if you are applying your morphisms you no longer care about the group structure

[Eric Wieser]

If we make this simp we should do it globally for all the endomorphisms / automorphisms

[Eric Wieser]

(not only for consistency, but that's more likely to alert us if this is a bad idea after all)

[Edward van de Meent]

i guess this could be a reasonable simp because this is in application form, rather than just a plain e⁻¹ = e.symm?

[Edward van de Meent]

i suspect tagging MulAut.inv_def with simp will have adverse effects though

[Edward van de Meent]

in particular because this is breaking the abstraction barrier between (M ≃* M) and MulAut M, whereas the applied form already has broken that barrier, so doesn't worsen it

[Antoine Chambert-Loir]

Well, MulAut.inv_apply doesn't suffice, in fact, what I need is

@[simp]
theorem MulAut.symm_inv_apply {M : Type*} [Mul M] (e : MulAut M) (x : M) : (e⁻¹).symm x = e x := by
  simp only [MulAut.inv_def, MulEquiv.symm_symm]

[Antoine Chambert-Loir]

(I was led to that after a mere simp).

[Edward van de Meent]

right, because you don't get to apply inv_inv

[Eric Wieser]

I think probably we want (e⁻¹).symm = e and e.symm⁻¹ = e as simp lemmas too

[Edward van de Meent]

yes, i think that makes sense...

[Edward van de Meent]

weird question, but should some of these be marked with something like push_cast?

[Antoine Chambert-Loir]

(docs#MulAut.mul_apply and docs#MulAut.one_apply are already marked as simp.)

[Antoine Chambert-Loir]

I did that in #24082. I expect that I will have to de-simp one things or two.

[Edward van de Meent]

things like MulAut.apply_inv_self :thinking:

[Antoine Chambert-Loir]

That one doesn't prove by simp, but then, the next one, docs#MulAut.apply_symm_self does.