Commit 2023-05-02 22:58 755fcb97

feat: better display of partial results from library_search (#3743) On @PatrickMassot's example:

import Mathlib.Topology.Instances.Real
import Mathlib.Topology.Algebra.Order.Compact
import Mathlib.Tactic.LibrarySearch
example (f : ℝ → ℝ) {K : Set ℝ} (hK: IsCompact K) : ∃ x ∈ K, ∀ y ∈ K, f x ≤ f y := by
  library_search

we have:

• refine IsCompact.exists_forall_le hK ?_ ?_ as one of the suggested solutions
• in fact, as the first solution (on the basis that it uses more local hypotheses than alternatives)
• none of the spurious results which use False.elim ?_
• and better display of the result, with hints:

refine IsCompact.exists_forall_le hK ?_ ?_
-- Remaining subgoals:
-- ⊢ Set.Nonempty K
-- ⊢ ContinuousOn (fun x ↦ f x) K