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 then 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 you can solve the goal with

intro h
rw [h]
ring

but there’s a trick: 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

so now ring solves the goal immediately.

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, where more examples are given.