apply without autoParams

Stream: mathlib4

[Brendan Seamas Murphy]

Is there a config option for the apply tactic that makes it so a new goal is created for each autoParam argument instead of their corresponding tactic being run?

[Kyle Miller]

That's the default (and only) option already. The apply tactic implementation has a todo in the source code for handling auto params and default arguments at some point.

[Brendan Seamas Murphy]

hm, it seems like I get this behavior if I use apply with just the function name, eg apply Functor.mk, but not if I try to partially apply the function, e.g.

example (F : C ⥤q D) : C ⥤ D := by
  apply Functor.mk F

errors out

[Kyle Miller]

If you partially apply the function, that causes the tactic to run. That's due to the function application getting elaborated.

[Brendan Seamas Murphy]

Yeah, that makes sense

[Kyle Miller]

Maybe you can do apply @Functor.mk ... F with the right number of underscores in place of ...

[Brendan Seamas Murphy]

I think that would work, but at that point I think I'd just use refine with ?_'s for the remaining arguments