Should Injective be aesop simp

Stream: mathlib4

[Violeta Hernández]

I'm often surprised that aesop can't do anything on a Function.Injective f goal, without first using intro to unfold the predicate. Wondering if we should just tag it as aesop simp, or even just simp.

[Yaël Dillies]

It's a difficult call, because you might want to reason at the level of the predicates, for example docs#Function.surjective_comp_left_iff. But I have been having the same question as you, mostly for things like docs#Set.MapsTo, docs#Set.LeftInvOn, docs#Set.RightInvOn (why is this an abbrev of Set.LeftInvOn?!), docs#lowerBounds (here I believe we are just missing simp on docs#mem_lowerBounds)

[Violeta Hernández]

Oh my god thanks for bringing up mem_lowerBounds

[Violeta Hernández]

Here I've been thinking that was a design decision!

[Yaël Dillies]

PR welcome :grinning_face_with_smiling_eyes: (I would do it myself but I have too many things on my plate already)