Documentation

Mathlib.Tactic.ApplyWith

The applyWith tactic #

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

apply (config := cfg) e is like apply e but allows you to provide a configuration cfg : ApplyConfig to pass to the underlying apply operation.

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