Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+โ†‘Ctrl+โ†“to navigate, Ctrl+๐Ÿ–ฑ๏ธto focus. On Mac, use Cmdinstead of Ctrl. 
import Lean
import Std.Util.TermUnsafe

namespace Mathlib.Tactic
open Lean Meta Elab Tactic Term

/--
`apply (config := cfg) e` is like `apply e` but allows you to provide a configuration
`cfg : ApplyConfig` to pass to the underlying apply operation.
-/
elab (name := 
applyWith: ParserDescr
applyWith) "apply" " (" 
&: String โ†’ Bool โ†’ ParserDescr
&"config" " := " 
cfg: ?m.156
cfg:
term: Parser.Category
term ") " 
e: ?m.144
e:
term: Parser.Category
term : 
tactic: Parser.Category
tactic => do
  let 
cfg: ?m.852
cfg โ† unsafe 
evalTerm: (ฮฑ : Type) โ†’ Expr โ†’ Syntax โ†’ optParam DefinitionSafety DefinitionSafety.safe โ†’ TermElabM ฮฑ
evalTerm 
ApplyConfig: Type
ApplyConfig (
mkConst: Name โ†’ optParam (List Level) [] โ†’ Expr
mkConst ``
ApplyConfig: Type
ApplyConfig) 
cfg: ?m.156
cfg
  
evalApplyLikeTactic: (MVarId โ†’ Expr โ†’ MetaM (List MVarId)) โ†’ Syntax โ†’ TacticM Unit
evalApplyLikeTactic (ยท.
apply: MVarId โ†’
  Expr โ†’
    optParam ApplyConfig
        { newGoals := ApplyNewGoals.nonDependentFirst, synthAssignedInstances := true, approx := true } โ†’
      MetaM (List MVarId)
apply ยท 
cfg: ?m.852
cfg) 
e: ?m.144
e