The applyWith tactic

The applyWith tactic is like apply, but allows passing a custom configuration to the underlying apply operation.

def Mathlib.Tactic.elabApplyConfig : Lean.Syntax → Lean.Elab.Tactic.TacticM Lean.Meta.ApplyConfig

Elaborator for the configuration in apply (config := cfg) syntax.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.applyWith : Lean.ParserDescr

apply e tries to match the current goal against the conclusion of e's type. If it succeeds, then the tactic returns as many subgoals as the number of premises that have not been fixed by type inference or type class resolution. Non-dependent premises are added before dependent ones.

The apply tactic uses higher-order pattern matching, type class resolution, and first-order unification with dependent types.

Extensions:

• • apply (config := cfg) e allows for additional configuration (see Lean.Meta.ApplyConfig):
    • newGoals controls which new goals are added by apply, in which order.
    • -synthAssignedInstances will not synthesize instance implicit arguments if they have been assigned by isDefEq.
    • +allowSynthFailures will create new goals when instance synthesis fails, rather than erroring.
    • +approx enables isDefEq approximations (see Lean.Meta.approxDefEq).

Equations

• One or more equations did not get rendered due to their size.