Eliminating function applications

Stream: general

[Eric Wieser]

I've found myself faced with a goal like f a = a multiple times now, where f is some bundled morphism.
In these cases, I have tools availabe to work with equalities of morphisms directly, but f is some horrible expression so using suffices : f = id isn't feasible.

It's tempting to add a lemma like:

lemma linear_map.idem_iff_id {M : Type*} [add_comm_monoid M] [semimodule R M] (f : M →ₗ[R] M) :
  (∀ a, f a = a) ↔ f = linear_map.id :=
⟨λ hm, linear_map.ext hm, λ h, h.symm ▸ λ a, rfl⟩

Is this type of lemma sensible? Can anyone suggest a better name than idem_iff_id?

[Floris van Doorn]

If we have a version of docs#linear_map.ext_iff with g (and f) explicit, you could easily do what you want with that lemma by setting g := linear_map.id, and that would be a generalization of your lemma. I'm not sure if it's worth it to also add your lemma.