compound repeat first tactic no longer solves 3 and props

Stream: new members

[jordane95]

I'm reading the theorem proving in lean4 book. 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:

```lean
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)

[jordane95]

Does anyone know why?

[Ruben Van de Velde]

Can you try replacing the pipe after inr by a semicolon?

[Damiano Testa]

In the online server, all 4 examples are successful.

[Damiano Testa]

I think that the differenceasymmetry between | and ; is due to how or associates: either on the left there is a prop that is an assumption or you keep destructuring.

[jordane95]

Ruben Van de Velde said:

Can you try replacing the pipe after inr by a semicolon?

tried, doesn't work