exact?

Stream: general

[Bolton Bailey]

I was under the impression that exact? is the lean4 library_search. But the following code doesn't work, even though there is an exact which does work.

import Mathlib.Data.Polynomial.Degree.Definitions

open Polynomial

variable {R : Type} [CommRing R] {p : Polynomial R}

theorem foo (hfd : p.natDegree = 0) : p = C (p.coeff 0) :=
  by
  -- exact Polynomial.eq_C_of_natDegree_eq_zero hfd -- works
  exact? -- doesn't work
  -- library_search -- doesn't close goal

Am I doing something wrong?

[Scott Morrison]

Have to run now, but:

-- Enable this option for tracing:
-- set_option trace.Tactic.librarySearch true
-- And this option to trace all candidate lemmas before application.
-- set_option trace.Tactic.librarySearch.lemmas true
-- It may also be useful to enable
-- set_option trace.Meta.Tactic.solveByElim true

[Scott Morrison]

I'll try to look later today.