Instances in refine (for port/RingTheory.Jacobson)

Stream: mathlib4

[Antoine Chambert-Loir]

I am trying to finish to port that file written in Lean 3 by @Devon Tuma
I have one question about instances as arguments.

Some statements have arguments of the form (P : Ideal R) [hP : IsMaximal P], but it seems that Lean 3 and Lean 4 behave differently, in so that Lean 4 blocks if the instance hP cannot be found, while Lean 3, if it finds P seems to be capable of creating the goal IsMaximal P.

Am I right ? If yes, how to circumvent this issue ?

One option would be to change the arguments formats to {P : Ideal R} (hP : IsMaximal P).

[Riccardo Brasca]

Doing refine' @foo _ _ _ should still work.

[Riccardo Brasca]

But I agree it would be nice if refine asks for instances that is not able to find, at least if they're Prop valued.

[Kyle Miller]

You might need to put (_) in place of _ for the instance argument

[Scott Morrison]

You can also use apply (config := {allowSynthFailures := true}).