Rule of thumb: `cases`, `cases'`, `rcases` vs. `rintro`

Stream: new members

[Isak Colboubrani]

For those teaching Lean/Mathlib (or others with relevant insights): do you have any practical rules of thumb that can reduce students’ cognitive load when deciding between intro/cases, intro/cases', intro/rcases, or rintro in situations where any of them would work, or more generally?

Examples:

-- Option 1.
intro h
cases h with
| … => …
| … => …

-- Option 2.
intro h
cases' h with … …

-- Option 3.
intro h
rcases h with … | …

-- Option 4.
rintro (… | … | …)

[Bolton Bailey]

I think the tactic cheatsheet is perhaps what you're looking for?

[Ilmārs Cīrulis]

Somehow I still haven't learned about cases', rcases or rintro, because the 1st option is completely sufficient for me. This is my way of 'reducing cognitive load', probably.

[Bolton Bailey]

Hmm, seems the cheatsheet doesn't actually cover rintro or cases

[Jon Eugster]

So far my take on this was to just introduce two tactics: intro and obtain and say that all the cases-variations are just different stylistic choices to use instead of obtain. So concretely I've just settled on Option 3 above but with obtain:

• I introduced intro as the tactic to make progress on A → B. rintro seemed mostly superfluous as one can write intro ⟨a, b⟩, too. Only rintro a | b seems not to work with intro but then I'd say to just use intro followed by obtain.
• obtain ⟨a, b⟩ := h and obtain a | b := h (or a blank obtain ⟨⟩ := h for both) is used to split an existing assumption.
  • Afaik rcases is literally the same as obtain just a different syntax.
  • cases' I see as a backwards-compatibility syntax for obtain (aka Lean3-style syntax) which shouldn't be used too much, but it's here if you like it.
  • cases I see as a more verbose version of obtain which might be nice if the students are familiar with term mode and match statements, but otherwise I'd prefer obtain due to it's similarity to have _ := _

[Jireh Loreaux]

The one nice thing about cases over obtain is that the match arms have names as opposed to a focusing dot ·. However, we recently had a discussion about extended the pattern syntax to allow naming of the arms.