leanprover-community / leanprover-community/mathlib4

`exact?` doesn't close the goal

Open
#6,937 6 comments 0 reactions 1 assignee View on GitHub

@kim-em is already working on this.

Since Sep 4, 2023.

Dominant language
Lean
Stars
4.1k
Forks
1.7k
No merged PRs in 30d

Description

From https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/exact.3F.20doesn't.20close.20the.20goal

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]

Contributor guide

Open the contributing guide

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.