apply_with ... { instances := false }

Stream: mathlib4

[Adam Topaz]

What's the current state of the art for using apply foo while introducing goals for the missing instances?

[Adam Topaz]

In mathlib3, I would usually use apply_with foo { instances := false }

[Eric Wieser]

refine' @foo _ _ _ (_) where (_) is the instance argument

[Adam Topaz]

my foo has about 15 _'s

[Eric Wieser]

refine @foo _ _ _ ?_ might work too, I haven't tried

[Eric Wieser]

Sounds like you're doomed to write a lot of _s

[Adam Topaz]

I ended up using suffices : A ; apply ... for one instance and suffices : A x B; cases this ; apply ... ; refine' <_,_> for 2 isntances

[Adam Topaz]

This can't be ideal. And using refine' foo _ _ _ _ _ _ can't be ideal either.

[Adam Topaz]

Is there a way to get refine to work approximately as follows: refine foo ((?_ : ClassName) := _) _ _?

[Eric Wieser]

I requested this in another thread

[Eric Wieser]

There's some progress here and onwards

[Adam Topaz]

Great!

[Eric Wieser]

Eric Wieser said:

I requested this in another thread

Here

[Thomas Murrills]

Btw, I’m not sure how it deals with instance arguments, but note that refine' foo .. is shorthand for refine' foo _ _ _ _ _ _ (etc.)