the 70 wat apply?

Stream: lean4

[Julian Berman]

example : wat → wat := by apply? finds exact fun a => a.
example : wat → (wat ∧ wat) := by apply? finds exact fun a => ⟨a, a⟩.

But example : wat → (wat ∧ wat ∧ wat) := by apply? ...

suggests the identical refine fun a => ?_ a -- 70 separate times.

Within these 70 suggestions (which from what I can tell really do just insert the same term if you use the code action), apply? seems to suggest a few different things it thinks are the remaining subgoals (i.e. different things for the same term), though the vast majority from scanning seem to be the same remaining subgoals.

[Johan Commelin]

cc @Kim Morrison

[Kim Morrison]

example : wat → (wat ∧ wat ∧ wat) := by apply?

(Code block so I can open in live.lean-lang.org. :-)

[Kim Morrison]

Thanks for the report, fixed in lean#5589.

[Kim Morrison]

Oh, failed some tests, I guess is it more complicated than that...