exact? failing to find a lemma which closes the goal

Stream: mathlib4

[Bhavik Mehta]

import Mathlib.Data.Set.Lattice
import Mathlib.Tactic.LibrarySearch

example {α : Type*} {s t : Set α} : Disjoint (t ∩ s) (t \ s) := by exact?

This exact? call fails, but disjoint_inf_sdiff closes the goal directly. Why does exact? struggle here?

[Ruben Van de Velde]

Probably because of the difference between inf and inter

[Bhavik Mehta]

Ah I assumed that it was smart enough to see through that defeq, but I guess in general that's too slow. Cases like this seem unhelpful for beginners...

[Ruben Van de Velde]

Clearly we should drop the set notation :innocent:

[Yaël Dillies]

cc @Kyle Miller whom I talked about this with

[Ruben Van de Velde]

Or if we're entertaining heretical ideas, use \cup and \cap for lattice operations

[Yaël Dillies]

Our idea with Kyle was to kill the set-specific operators and let lattice notation delaborate to it instead.

[Yaël Dillies]

Then we'd only have ⊔ and ⊓ in the terms, but we would keep ∪ and ∩ in the infoview.

[Scott Morrison]

Thereby making copy and paste unnecessarily dangerous? :-)

[Scott Morrison]

Bhavik Mehta said:

Ah I assumed that it was smart enough to see through that defeq, but I guess in general that's too slow. Cases like this seem unhelpful for beginners...

Now that exact? is so much faster than in Lean 3, it might be possible to let it see though more defeq. Someone should try!

[Yaël Dillies]

Scott Morrison said:

Thereby making copy and paste unnecessarily dangerous? :-)

How so? That would only be a problem if you copy-pasted a Set expression and used it as a Lattice expression (which is already a problem currently). You will still be able to input code using ∪/∩/ It just won't show up differently from ⊔/⊓ in the term.