Zulip Chat Archive

Stream: general

Topic: exact? doesn't close the goal


Wen Yang (Sep 03 2023 at 04:21):

I find that the suggestion from exact? doesn't always close the goal. For example:

import Mathlib.Analysis.NormedSpace.Basic
variable (a : ) (h1 : 0  a)
example : a = dist a 0 := by
  rw [dist_eq_norm]
  simp
  exact?
  -- Try this: exact Eq.symm ((fun {α} [LinearOrderedRing α] {a} => abs_eq_self.mpr) h1)

It doesn't close the goal, since

typeclass instance problem is stuck, it is often due to metavariables
  LinearOrderedRing ?m.551

What actually close the goal is:

rw_mod_cast [abs_eq_self.mpr h1]

Is that a normal behavior?

Scott Morrison (Sep 03 2023 at 23:32):

Could you open an issue on the mathlib4 repository for this one? It's not clear to me if this is a problem in exact?, a problem in the pretty printer, or something else.

Wen Yang (Sep 04 2023 at 01:30):

I have opened an issue at https://github.com/leanprover-community/mathlib4/issues/6937


Last updated: Dec 20 2023 at 11:08 UTC