rintro tactic

Stream: new members

[Maris Ozols]

I started learning Lean very recently and I'm working my way through Buzzard's Formalizing Mathematics course at my own pace. One thing I'm struggling to understand is the rintro tactic. Here are two examples where it's being used:

example : P ∧ Q → Q ∧ R → P ∧ R := by
  rintro ⟨hP, hQ⟩ ⟨-, hR⟩
  exact ⟨hP, hR⟩
example : False ↔ P ∧ False := by
  constructor
  · rintro ⟨⟩
  · rintro ⟨-, ⟨⟩⟩

Can somebody explain how I can make sense of this?

[Kevin Buzzard]

Do you know about the rcases tactic? rintro is just intro followed by rcases. The docs for the tactics used in the course are here. Ask again if these don't answer your questions!