exact? regression?

Stream: mathlib4

[Kevin Buzzard]

I just upgraded my mathlib and now I have this:

import Mathlib

example (a b c : ℤ) (hc : c ≠ 0) (h : a * c = b * c) : a = b := by
  exact?
  /-
  function expected
    @ι' (φ j)
  -/

Was that a thing before?

[Sébastien Gouëzel]

It's a known issue, soon to be fixed, see https://leanprover.zulipchat.com/#narrow/stream/113486-announce/topic/v4.2E7.2E0-rc1/near/424799730. It should work with fewer imports.

[Kevin Buzzard]

Oh yeah I just realised this myself. Thanks!

[Kim Morrison]

This is fixed now on master.

[Kevin Buzzard]

Indeed, now exact? fails for an older reason :-) (it doesn't find mul_right_cancel₀ hc h because exact? doesn't seem to work on equalities in general)