def Mathlib.Tactic.variables : Lean.ParserDescr

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

def Mathlib.Tactic.lemma : Lean.ParserDescr

lemma means the same as theorem. It is used to denote "less important" theorems

def Mathlib.Tactic.expandLemma : Lean.Macro

Implementation of the lemma command, by macro expansion to theorem.

def Mathlib.Tactic.«termSort*» : Lean.ParserDescr

The syntax variable (X Y ... Z : Sort*) creates a new distinct implicit universe variable for each variable in the sequence.

def Mathlib.Tactic.«termType*» : Lean.ParserDescr

The syntax variable (X Y ... Z : Type*) creates a new distinct implicit universe variable > 0 for each variable in the sequence.

def Mathlib.Tactic.pushFVarAliasInfo {m : Type → Type} [Monad m] [Lean.Elab.MonadInfoTree m] (oldFVars : Array Lean.FVarId) (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.

def Lean.MVarId.withReverted {α : Type} (mvarId : Lean.MVarId) (fvarIds : Array Lean.FVarId) (k : Lean.MVarId → Array Lean.FVarId → Lean.MetaM (α × Array (Option Lean.FVarId) × Lean.MVarId)) (clearAuxDeclsInsteadOfRevert : optParam Bool false) : Lean.MetaM (α × Lean.MVarId)

Function to help do the revert/intro pattern, running some code inside a context where certain variables have been reverted before re-introing them. It will push FVarId alias information into info trees for you according to a simple protocol.

• fvarIds is an array of fvarIds to revert. These are passed to Lean.MVarId.revert with preserveOrder := true, hence the function raises an error if they cannot be reverted in the provided order.
• k is given the goal with all the variables reverted and the array of reverted FVarIds, with the requested FVarIds at the beginning. It must return a tuple of a value, an array describing which FVarIds to link, and a mutated MVarId.

The a : Array (Option FVarId) array returned by k is interpreted in the following way. The function will intro a.size variables, and then for each non-none entry we create an FVar alias between it and the corresponding introed variable. For example, having k return fvars.map .some causes all reverted variables to be introed and linked.

Returns the value returned by k along with the resulting goal.

def Lean.MVarId.changeLocalDecl' (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (typeNew : Lean.Expr) (checkDefEq : optParam Bool true) : Lean.MetaM Lean.MVarId

Replace the type of the free variable fvarId with typeNew.

If checkDefEq = true then throws an error if typeNew is not definitionally equal to the type of fvarId. Otherwise this function assumes typeNew and the type of fvarId are definitionally equal.

This function is the same as Lean.MVarId.changeLocalDecl but makes sure to push substitution information into the infotree.

def Mathlib.Tactic.tacticBy_cases_ : Lean.ParserDescr

by_cases p makes a case distinction on p, resulting in two subgoals h : p ⊢ and h : ¬ p ⊢.

def Mathlib.Tactic.tacticTransitivity___ : Lean.ParserDescr

def Mathlib.Tactic.introv : Lean.ParserDescr

The tactic introv allows the user to automatically introduce the variables of a theorem and explicitly name the non-dependent hypotheses. Any dependent hypotheses are assigned their default names.

Examples:

example : ∀ a b : Nat, a = b → b = a := by
  introv h,
  exact h.symm

The state after introv h is

a b : ℕ,
h : a = b
⊢ b = a

example : ∀ a b : Nat, a = b → ∀ c, b = c → a = c := by
  introv h₁ h₂,
  exact h₁.trans h₂

The state after introv h₁ h₂ is

a b : ℕ,
h₁ : a = b,
c : ℕ,
h₂ : b = c
⊢ a = c

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

partial def Mathlib.Tactic.evalIntrov.introsDep : Lean.Elab.Tactic.TacticM Unit

def Mathlib.Tactic.evalIntrov.intro1PStep : Lean.Elab.Tactic.TacticM Unit

def Mathlib.Tactic.tacticAssumption' : Lean.ParserDescr

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

def Mathlib.Tactic.tacticMatch_target_ : Lean.ParserDescr

def Mathlib.Tactic.clearAuxDecl : Lean.ParserDescr

This tactic clears all auxiliary declarations from the context.

def Lean.MVarId.clearValue (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) : Lean.MetaM Lean.MVarId

Clears the value of the local definition fvarId. Ensures that the resulting goal state is still type correct. Throws an error if it is a local hypothesis without a value.

def Mathlib.Tactic.clearValue : Lean.ParserDescr

clear_value n₁ n₂ ... clears the bodies of the local definitions n₁, n₂ ..., changing them into regular hypotheses. A hypothesis n : α := t is changed to n : α.

The order of n₁ n₂ ... does not matter, and values will be cleared in reverse order of where they appear in the context.