Is Function.onFun preferred?

Stream: mathlib4

[Eric Wieser]

I made #9256 a while ago, which replaces things like (s : Set ι).Pairwise fun i j => Commute (f i) (f j) with (s : Set ι).Pairwise (Commute on f), where on is preexisting notation for docs#Function.onFun.

Is this a good change? If so, then I'd argue we should upstream onFun to Std so that we can make similar changes there for consistency; if not, then perhaps we should eliminate onFun entirely.

[Emilie (Shad Amethyst)]

I'm hitting a weird corner case where simp can't apply onFun_apply if the output type is a Prop, but rw can:

example {α : Type*} {f : α → α} {g : α → α → Prop} (a b : α) : (g on f) a b ↔ g (f a) (f b) ∧ True := by
  simp only [Function.onFun_apply] -- error: simp made no progress
  rw [and_true]

example {α : Type*} {f : α → α} {g : α → α → Prop} (a b : α) : (g on f) a b ↔ g (f a) (f b) ∧ True := by
  rw [Function.onFun_apply, and_true] -- works

[Kevin Buzzard]

Is this relevant to Eric's question? If not, you could post your question in the interminable simp X fails, rw X works thread (or even move these two messages to that thread)

[Emilie (Shad Amethyst)]

Well, it's a corner case that I've encountered more than once before, and it makes me want to avoid using onFun in my proofs; I'll send a MWE there, though