# Documentation

Lean.Meta.Tactic.Generalize

The generalize tactic takes arguments of the form h : e = x

Instances For
Equations
def Lean.MVarId.generalize (mvarId : Lean.MVarId) (args : ) :

Telescopic generalize tactic. It can simultaneously generalize many terms. It uses kabstract to occurrences of the terms that need to be generalized.

Equations
def Lean.Meta.generalize (mvarId : Lean.MVarId) (args : ) :

Telescopic generalize tactic. It can simultaneously generalize many terms. It uses kabstract to occurrences of the terms that need to be generalized.

Equations
def Lean.MVarId.generalizeHyp (mvarId : Lean.MVarId) (args : ) (hyps : optParam () #[]) (fvarSubst : optParam Lean.Meta.FVarSubst { map := }) :

Extension of generalize to support generalizing within specified hypotheses. The hyps array contains the list of hypotheses within which to look for occurrences of the generalizing expressions.

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