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