RFC: Unify what `MyInductiveType.elim` means

Proposal

Currently, the .elim lemmas are all over the place in terms of argument order:

• X.elim with x : X as the first argument: Nonempty.elim (core), Or.elim (core), Not.elim (core), Ne.elim (core), Exists.elim (core), Option.elim (core), Or.elim3 (Mathlib),
• X.elim with x : X as the last argument: And.elim (core), Iff.elim (core), Sum.elim (Batteries), Option.elim' (Mathlib)

It would be good for the benefit of everyone if these discrepancies were fixed.

I would further like to argue that we should fix these discrepancies by having:

• X.elim take x : X as the last argument
• X.elimOn take x : X as the first argument

This would match the naming of X.rec and X.recOn.

Community Feedback

This was discussed on Zulip in Lean 3 and in Lean 4. Recently, there was #15448 by @urkud.

Here is a summary of what was said:

• Yes, the current situation is indeed a mess
• We definitely want the version with the X argument last in cases where we are building functions out of (not-so-large) large combinations of inductive types. Eg Sum.elim (Sum.elim (fun _ => trivial) fun _ => trivial) fun _ => trivial is nicer than fun x => x.elim (fun y => y.elim (fun _ => trivial) fun _ => trivial) fun _ => trivial when building a term of type α ⊕ β ⊕ γ → True. This also shows up in Mathlib vector notation.
• We want the version with the X argument first when we want to do a "poor-man's match statement" to be able to see what each branch is after having provided the main premise. But this need can be circumvented by either using
  • dot notation: myX.elim _ _
  • a named argument, assuming the main premise is a named argument: X.elim (x := myX) _ _

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start by reviewing the listed core, Batteries, and Mathlib eliminators, then read the linked Zulip discussions and issue #15448. Done would require an agreed argument-order convention and the corresponding coordinated changes across the affected APIs.