Create typeclass goals with apply?

Stream: mathlib4

[Joël Riou]

In mathlib, in order to prove epi g, one could use apply category_theory.epi_of_epi f g, which would create the goal epi (f ≫ g) if this class could not be infered automatically. Is there a way to do the same in mathlib4? (Apart from refine @epi_of_epi _ _ _ _ _ f g ?_.)

[Adam Topaz]

mathlib3 also had apply_with ... { instances := ff }. I suppose we have something similar in mathlib4?

[Adam Topaz]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/ApplyWith.html#Mathlib.Tactic.applyWith

[Adam Topaz]

So I think(hope) that apply (config := { synthAssignedInstances := false }) epi_of_epi f g should work?

[Joël Riou]

I had just tried this, but it does not seem to work on https://github.com/leanprover-community/mathlib4/pull/2467/files#diff-8fa3d373d90b7fa7d6c162fd2cd095aa9f8b9d8317ccd32b5d3e20e18d361196R105

[Adam Topaz]

hmmm... that's not great.

[Adam Topaz]

refine probably won't scale for this application. I don't know of any other tricks through.

[Reid Barton]

A "trick" that works well in this and similar situations is to use regular definitions rather than classes.