def Lean.Elab.Tactic.Do.ProofMode.mIntro {m : Type → Type u_1} [Monad m] [MonadControlT MetaM m] [MonadLiftT MetaM m] (goal : MGoal) (ident : TSyntax `Lean.binderIdent) (k : MGoal → m Expr) : m Expr

Equations

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

def Lean.Elab.Tactic.Do.ProofMode.mIntroForall {m : Type → Type u_1} [Monad m] [MonadControlT MetaM m] [MonadLiftT MetaM m] (goal : MGoal) (ident : TSyntax `Lean.binderIdent) (k : MGoal → m Expr) : m Expr

Equations

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

def Lean.Elab.Tactic.Do.ProofMode.mIntroForallN {m : Type → Type u_1} [Monad m] [MonadControlT MetaM m] [MonadLiftT MetaM m] (goal : MGoal) (n : Nat) (k : MGoal → m Expr) : m Expr

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.Tactic.Do.ProofMode.mIntroForallN goal 0 k = k goal

def Lean.Elab.Tactic.Do.ProofMode.elabMIntro : Tactic

Equations

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