apply? giving output which then fails

Stream: mathlib4

[Bolton Bailey]

import Mathlib

theorem MvPolynomial.degreeOf_C_mul_le {R σ : Type} [CommSemiring R] [DecidableEq σ] (j : σ)
    (c : R) (f : MvPolynomial σ R) :
    MvPolynomial.degreeOf j (MvPolynomial.C c * f) ≤ MvPolynomial.degreeOf j f := by
  unfold degreeOf
  have := degrees_mul (C c) f
  simp [MvPolynomial.degrees_C] at this
  -- exact?  -- exact Multiset.count_le_of_le j this
  exact Multiset.count_le_of_le j this -- type mismatch

[Ruben Van de Velde]

Looks like the difference is in the decidability instance; convert instead of exact works

[Kim Morrison]

What's going on under the hood here?

import Mathlib

theorem MvPolynomial.degreeOf_C_mul_le {R σ : Type} [CommSemiring R] [DecidableEq σ] (j : σ)
    (c : R) (f : MvPolynomial σ R) :
    MvPolynomial.degreeOf j (MvPolynomial.C c * f) ≤ MvPolynomial.degreeOf j f := by
  unfold degreeOf
  have := degrees_mul (C c) f
  simp [MvPolynomial.degrees_C] at this
  -- what `exact?` is actually doing is:
  apply (config := {allowSynthFailures := true}) Multiset.count_le_of_le
  solve_by_elim*

[Kim Morrison]

Curiously even though apply Multiset.count_le_of_le by itself fails with a typeclass synthesis error, with (config := {allowSynthFailures := true}) it doesn't actually return any additional goals!

[Kim Morrison]

That seems a bit mysterious.

[Kim Morrison]

One approach here would be to have exact? verify that its suggestion really works, and if it doesn't, try again with convert, and then report that if it works.

[Kim Morrison]

This could be done without touching the internals of exact?, but instead as a wrapper around Std.Tactic.TryThis.addExactSuggestion.

[Kim Morrison]

Anyone interested?