# Documentation

Mathlib.Lean.Meta

## Additional utilities in Lean.MVarId#

def Lean.MVarId.replace (g : Lean.MVarId) (hyp : Lean.FVarId) (proof : Lean.Expr) (typeNew : optParam () none) :

Replace hypothesis hyp in goal g with proof : typeNew. The new hypothesis is given the same user name as the original, it attempts to avoid reordering hypotheses, and the original is cleared if possible.

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

Finds the LocalDecl for the FVar in e with the highest index.

Equations
• One or more equations did not get rendered due to their size.
def Lean.MVarId.note (g : Lean.MVarId) (h : Lean.Name) (v : Lean.Expr) (t : optParam () none) :

Add the hypothesis h : t, given v : t, and return the new FVarId.

Equations
def Lean.MVarId.existsi (mvar : Lean.MVarId) (es : ) :

Has the effect of refine ⟨e₁,e₂,⋯, ?_⟩.

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

Applies intro repeatedly until it fails. We use this instead of Lean.MVarId.intros to allowing unfolding. For example, if we want to do introductions for propositions like ¬p, the ¬ needs to be unfolded into → False, and intros does not do such unfolding.

Equations
partial def Lean.MVarId.intros!.run (mvarId : Lean.MVarId) (acc : ) (g : Lean.MVarId) :

Implementation of intros!.

Return local hypotheses which are not "implementation detail", as Exprs.

Equations
• One or more equations did not get rendered due to their size.
def Lean.Meta.mapForallTelescope' (F : ) (forallTerm : Lean.Expr) :

Given a monadic function F that takes a type and a term of that type and produces a new term, lifts this to the monadic function that opens a ∀ telescope, applies F to the body, and then builds the lambda telescope term for the new term.

Equations
• One or more equations did not get rendered due to their size.
def Lean.Meta.mapForallTelescope (F : ) (forallTerm : Lean.Expr) :

Given a monadic function F that takes a term and produces a new term, lifts this to the monadic function that opens a ∀ telescope, applies F to the body, and then builds the lambda telescope term for the new term.

Equations

Analogue of liftMetaTactic for tactics that return a single goal.

Equations

Analogue of liftMetaTactic for tactics that do not return any goals.

Equations
def Lean.Elab.Tactic.run_for {α : Type} (mvarId : Lean.MVarId) (x : ) :

Copy of Lean.Elab.Tactic.run that can return a value.

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