# Documentation

Mathlib.Lean.Meta

## Additional utilities in Lean.MVarId#

Solve a goal by synthesizing an instance.

Instances For
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.

Instances For

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

Instances For
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.

Instances For
def Lean.MVarId.let (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.

Instances For
def Lean.MVarId.applyConst (mvar : Lean.MVarId) (c : Lean.Name) (cfg : optParam Lean.Meta.ApplyConfig { newGoals := Lean.Meta.ApplyNewGoals.nonDependentFirst, synthAssignedInstances := true, allowSynthFailures := false, approx := true }) :

Short-hand for applying a constant to the goal.

Instances For
def Lean.MVarId.existsi (mvar : Lean.MVarId) (es : ) :

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

Instances For

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.

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

Implementation of intros!.

Check if a goal is of a subsingleton type.

Instances For

Check if a goal is "independent" of a list of other goals. We say a goal is independent of other goals if assigning a value to it can not change the solvability of the other goals.

This function only calculates a conservative approximation of this condition.

Instances For

Try to convert an Iff into an Eq by applying iff_of_eq. If successful, returns the new goal, and otherwise returns the original MVarId.

This may be regarded as being a special case of Lean.MVarId.liftReflToEq, specifically for Iff.

Instances For

Try to convert an Eq into an Iff by applying propext. If successful, then returns then new goal, otherwise returns the original MVarId.

Instances For

Try to close the goal with using proof_irrel_heq. Returns whether or not it succeeds.

We need to be somewhat careful not to assign metavariables while doing this, otherwise we might specialize Sort _ to Prop.

Instances For

Try to close the goal using Subsingleton.elim. Returns whether or not it succeeds.

We are careful to apply Subsingleton.elim in a way that does not assign any metavariables. This is to prevent the Subsingleton Prop instance from being used as justification to specialize Sort _ to Prop.

Instances For
def Lean.Meta.getLocalHyps {m : } [] [] :
m ()

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

Instances For
def Lean.Meta.countLocalHypsUsed {m : } [] [] [] (e : Lean.Expr) :
m Nat

Count how many local hypotheses appear in an expression.

Instances For
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.

Instances For
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.

Instances For

Get the type the given metavariable after instantiating metavariables and cleaning up annotations.

Instances For

Analogue of liftMetaTactic for tactics that return a single goal.

Instances For

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

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

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

Instances For