tactic combinator <|>

Stream: lean4

[Adam Topaz]

What is Lean4's analogue of the tactic combinator <|>? E.g.

example (p q : Prop) (h : p) (h' : q) : q := by
  exact h <|> exact h

[Adam Topaz]

This works, but seems way too verbose?

example (p q : Prop) (h : p) (h' : q) : q := by
  try { exact h } <;> exact h'

[David Renshaw]

example (p q : Prop) (h : p) (h' : q) : q := by
  first | exact h | exact h'

[Arien Malec]

See: https://leanprover.github.io/theorem_proving_in_lean4/tactics.html#tactic-combinators

[Adam Topaz]

Thanks!