Yet another beginner question

Stream: new members

[Ilmārs Cīrulis]

I often see that I do this construction:

lemma L (a : ℕ) : True := by
  have h : a = 0 ∨ a = 1 ∨ 2 ≤ n := sorry
  obtain h | h | h := h
  sorry

I want to keep the type of h visible just to understand the proof better. (Sometimes, for me, the Lean proof is the first thing and then human understanding of proof follows, hopefully. :sweat_smile: )

Is that possible somehow in one line? Or should I forget about types and just do obtain h | h | h := sorry?

[Aaron Liu]

obtain h | h | h : a = 0 ∨ a = 1 ∨ 2 ≤ n := sorry

[Ilmārs Cīrulis]

Thank you very much!