rintro

Summary

The rintro tactic can be used to do multiple intro and cases tactics all in one line.

Examples

  1. Faced with the goal

⊢ P → Q ∧ R → S

one could use the following tactics

intro hP,
intro h,
cases h with hQ hR,

to get the tactic state

hP : P
hQ : Q
hR : R
⊢ S

However, one can get there in one line with

rintro hP ⟨hQ, hR⟩,

(the pointy brackets ⟨⟩ can be obtained by typing \< and \> in VS Code.)

  1. Faced with a goal of the form

⊢ P ∨ Q → R

the tactic rintro (hP | hQ) will do the same as intro h, cases h with hP hQ. In particular, after the application of the tactic there will be two goals, one with hypothesis hP : P and the other with hypothesis hQ : Q. Note the round brackets for “or” goals.

  1. There is a rfl easter egg with the rintro tactic. If the goal is

⊢ a = 2 * b → 2 * a = 4 * b

then rintro rfl will, instead of naming the hypothesis a = 2 * b and putting it in the tactic state, instead define a to be 2 * b, leaving the goal as

⊢ 2 * (2 * b) = 4 * b

Details

Note that rintro works up to definitional equality, like intro, so for example if the goal is ⊢ ¬P then rintro hP works fine (because ¬P is definitionally equal to P → false), leaving the tactic state as

hP : P
⊢ false

Further notes

The syntax for rintro with pointy and round brackets is the same as the syntax for rcases.