exact? errors

Stream: lean4

[Shreyas Srinivas]

The following is an #mwe for the errors I am encountering:

import Mathlib


example {α : Type} : ∀ x y : α, x ≠ y → Disjoint ({x} : Finset α) ({y} : Finset α )  := by
  -- exact?
  -- Below is the proof deduced by exact?
  exact fun x y a => (fun {α} {a b} => Finset.disjoint_singleton.mpr) a
  sorry



example {α : Type} : ∀ x y : α, x ≠ y → Disjoint ({x} : Finset α) ({y} : Finset α )  := by
  -- exact?
  -- Below is the correct proof
  exact fun x y a => (Finset.disjoint_singleton.mpr) a

[Shreyas Srinivas]

why is exact? adding some extra binders?

[Shreyas Srinivas]

I should point out that it exact? continues to work very well when I intro everything

[Eric Wieser]

To be fair, exact? really is finding that proof, the pretty-printing just doesn't round-trip:

theorem foo {α : Type} : ∀ x y : α, x ≠ y → Disjoint ({x} : Finset α) ({y} : Finset α )  := by
  exact?

#print foo

[Shreyas Srinivas]

It's a bit more weird. See the "observe errors" thread below this one

[Shreyas Srinivas]

I recall that observe is similar to exact? inside a have

[Eric Wieser]

Interestingly even set_option pp.all true fails to round-trip here

[Eric Wieser]

I filed lean4#6122

[Markus Himmel]

Is this a duplicate of lean4#5407 ?

[Kevin Buzzard]

Does doing all the intros first fix this problem? This has come up before and sensible intros was a workaround for the previous example

[Shreyas Srinivas]

Oh it does. I already mentioned it above