use tactic is no longer finishing

Stream: mathlib4

[Patrick Massot]

A small detail that is not very important but a bit confusing. In Lean 3 you could use use as a finishing tactic, as in

example : true ∧ true := by
  use [trivial, trivial]

[Patrick Massot]

This no longer works:

example : True ∧ True := by
  use trivial, trivial

[Patrick Massot]

invalid constructor ⟨...⟩, insufficient number of arguments, constructs 'True.intro' does not have explicit fields, but #2 provided

[Heather Macbeth]

@Patrick Massot The capabilities of use have been changing, most recently I downgraded them slightly: mathlib4#1153

[Patrick Massot]

I think this is completely unrelated. Here I'm not using the trivial tactic, only the term.

[Patrick Massot]

Maybe a less confusing example would be

example : ∃ n : nat, n = n  := by
  use [0, rfl]

vs

example : ∃ n : Nat, n = n  := by
  use 0, rfl

[Patrick Massot]

The first one works in Lean 3.

[Moritz Doll]

I've ran into this issue as well. My fix was changing use 0, rfl to exact ⟨0, rfl⟩, which is probably better style anyways. Looking at it now, I suspect that the issue is that use expects at least one more argument (since it is defined as refine ⟨a, ?_⟩ <?> bla).

[Mario Carneiro]

I think use 0; rfl would also work in these examples