compound repeat first tactic no longer solves all three permutations of `\and` propositions

[jordane95]

The tactics chapter states that

In the first example, the left branch succeeds, whereas in the second one, it is the right one that succeeds. In the next three examples, the same compound tactic succeeds in each case:

example (p q r : Prop) (hp : p) : p ∨ q ∨ r :=
  by repeat (first | apply Or.inl; assumption | apply Or.inr | assumption)

example (p q r : Prop) (hq : q) : p ∨ q ∨ r :=
  by repeat (first | apply Or.inl; assumption | apply Or.inr | assumption)

example (p q r : Prop) (hr : r) : p ∨ q ∨ r :=
  by repeat (first | apply Or.inl; assumption | apply Or.inr | assumption)

The tactic tries to solve the left disjunct immediately by assumption; if that fails, it tries to focus on the right disjunct; and if that doesn't work, it invokes the assumption tactic.

However, running it locally cannot solve all the subgoals. Here is the state left unsolved

example (p q r : Prop) (hq : q) : p ∨ q ∨ r :=
  /-
  case h
  p q r : Prop
  hq : q
  ⊢ q ∨ r
  -/
  by repeat (first | apply Or.inl; assumption | apply Or.inr | assumption)