Basic tactics and utilities for tactic writing

This file defines some basic utilities for tactic writing, and also

• a dummy variables macro (which warns that the Lean 4 name is variable)
• the introv tactic, which allows the user to automatically introduce the variables of a theorem and explicitly name the non-dependent hypotheses,
• an assumption macro, calling the assumption tactic on all goals
• the tactics match_target and clear_aux_decl (clearing all auxiliary declarations from the context).

def Mathlib.Tactic.variables : Lean.ParserDescr

Syntax for the variables command: this command is just a stub, and merely warns that it has been renamed to variable in Lean 4.

Equations

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

def Mathlib.Tactic.elabVariables : Lean.Elab.Command.CommandElab

The variables command: this is just a stub, and merely warns that it has been renamed to variable in Lean 4.

Equations

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

def Mathlib.Tactic.pushFVarAliasInfo {m : Type → Type} [Monad m] [Lean.Elab.MonadInfoTree m] (oldFVars newFVars : Array Lean.FVarId) (newLCtx : Lean.LocalContext) : m Unit

Given two arrays of FVarIds, one from an old local context and the other from a new local context, pushes FVarAliasInfos into the info tree for corresponding pairs of FVarIds. Recall that variables linked this way should be considered to be semantically identical.

The effect of this is, for example, the unused variable linter will see that variables from the first array are used if corresponding variables in the second array are used.

Equations

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

def Mathlib.Tactic.introv : Lean.ParserDescr

introv introduces the parameters to a dependent function according to their parameter name. If the first parameter is not depended on by the rest of the function type, introv with no (remaining) arguments does nothing.

• introv h₁ h₂ ... introduces non-depended-on parameters in between sequences of depended-on parameters, using the names h₁, h₂, ... in turn. Use _ to anonymize a specific hypothesis.

Examples:

example : ∀ a b : Nat, a = b → b = a := by
  introv h
  /-
  The goal state is:
  a b : ℕ,
  h : a = b
  ⊢ b = a
  -/
  exact h.symm

example : ∀ a b : Nat, a = b → ∀ c, b = c → a = c := by
  introv h₁ h₂
  /-
  The goal state is:
  a b : ℕ,
  h₁ : a = b,
  c : ℕ,
  h₂ : b = c
  ⊢ a = c
  -/
  exact h₁.trans h₂

Equations

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

def Mathlib.Tactic.evalIntrov : Lean.Elab.Tactic.Tactic

Equations

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

def Mathlib.Tactic.tacticAssumption' : Lean.ParserDescr

Try calling assumption on all goals; succeeds if it closes at least one goal.

Equations

• Mathlib.Tactic.tacticAssumption' = Lean.ParserDescr.node `Mathlib.Tactic.tacticAssumption' 1024 (Lean.ParserDescr.nonReservedSymbol "assumption'" false)

@[deprecated "Use `guard_target =~` instead." (since := "2025-12-11")]

def Mathlib.Tactic.tacticMatch_target_ : Lean.ParserDescr

Deprecated: use guard_target =~ t instead.

Equations

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

def Mathlib.Tactic.clearAuxDecl : Lean.ParserDescr

This tactic clears all auxiliary declarations from the context.

Equations

• Mathlib.Tactic.clearAuxDecl = Lean.ParserDescr.node `Mathlib.Tactic.clearAuxDecl 1024 (Lean.ParserDescr.nonReservedSymbol "clear_aux_decl" false)

structure Mathlib.Tactic.withResetServerInfo.Result (α : Type) : Type

Result of withResetServerInfo.

• result? : Option α

  Return value of the executed tactic.

• msgs : Lean.MessageLog

  Messages produced by the executed tactic.

• trees : Lean.PersistentArray Lean.Elab.InfoTree

  Info trees produced by the executed tactic, wrapped in CommandContextInfo.save.

def Mathlib.Tactic.withResetServerInfo {α : Type} (t : Lean.Elab.Tactic.TacticM α) : Lean.Elab.Tactic.TacticM (withResetServerInfo.Result α)

Runs a tactic, returning any new messages and info trees rather than adding them to the state.

Equations

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