apply (config := { instances := false })

Stream: mathlib4

[Kevin Buzzard]

mathlib3port is turning apply_with foo { instances := ff }, into apply (config := { instances := false }) foo, which is barfing with a syntax error (expected ')', ',' or ':'). Is apply configurable? I'm assuming not and will work around accordingly.

[Kyle Miller]

It looks like you have to import Mathlib.Tactic.ApplyWith

[Adam Topaz]

But note that docs4#Lean.Meta.ApplyConfig doesn't have an instances field.