diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index df814e4aa1..b50a927016 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -290,9 +290,12 @@ def adaptExpander (exp : Syntax → TacticM Syntax) : Tactic := fun stx => do
   let stx' ← exp stx
   withMacroExpansion stx stx' $ evalTactic stx'
 
+/-- Add the given goals at the end of the current goals collection. -/
 def appendGoals (mvarIds : List MVarId) : TacticM Unit :=
   modify fun s => { s with goals := s.goals ++ mvarIds }
 
+/-- Discard the first goal and replace it by the given list of goals, 
+keeping the other goals. -/
 def replaceMainGoal (mvarIds : List MVarId) : TacticM Unit := do
   let (_ :: mvarIds') ← getGoals | throwNoGoalsToBeSolved
   modify fun _ => { goals := mvarIds ++ mvarIds' }
diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean
index ef131dadd8..75cba225b1 100644
--- a/src/Lean/Elab/Tactic/ElabTerm.lean
+++ b/src/Lean/Elab/Tactic/ElabTerm.lean
@@ -16,6 +16,8 @@ open Meta
 
 /-! # `elabTerm` for Tactics and basic tactics that use it. -/
 
+/-- Elaborate `stx` in the current `MVarContext`. If given, the `expectedType` will be used to help
+elaboration but not enforced (use `elabTermEnsuringType` to enforce an expected type). -/
 def elabTerm (stx : Syntax) (expectedType? : Option Expr) (mayPostpone := false) : TacticM Expr := do
   /- If error recovery is disabled, we disable `Term.withoutErrToSorry` -/
   if (← read).recover then
@@ -29,6 +31,8 @@ where
       Term.synthesizeSyntheticMVars mayPostpone
       instantiateMVars e
 
+/-- Elaborate `stx` in the current `MVarContext`. If given, the `expectedType` will be used to help
+elaboration and then a `TypeMismatchError` will be thrown if the elaborated type doesn't match.  -/
 def elabTermEnsuringType (stx : Syntax) (expectedType? : Option Expr) (mayPostpone := false) : TacticM Expr := do
   let e ← elabTerm stx expectedType? mayPostpone
   -- We do use `Term.ensureExpectedType` because we don't want coercions being inserted here.
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index 2adf577b84..21e2384441 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -697,6 +697,8 @@ def _root_.Lean.FVarId.getUserName (fvarId : FVarId) : MetaM Name :=
 def _root_.Lean.FVarId.isLetVar (fvarId : FVarId) : MetaM Bool :=
   return (← fvarId.getDecl).isLet
 
+/-- Get the local declaration associated to the given `Expr` in the current local
+context. Fails if the given expression is not a fvar or if no such declaration exists. -/
 def getFVarLocalDecl (fvar : Expr) : MetaM LocalDecl :=
   fvar.fvarId!.getDecl
 
diff --git a/src/Lean/Meta/Tactic/Intro.lean b/src/Lean/Meta/Tactic/Intro.lean
index 058fd3f392..ae3d2b88cc 100644
--- a/src/Lean/Meta/Tactic/Intro.lean
+++ b/src/Lean/Meta/Tactic/Intro.lean
@@ -136,9 +136,10 @@ def intro1Core (mvarId : MVarId) (preserveBinderNames : Bool) : MetaM (FVarId ×
   let (fvarIds, mvarId) ← introNCore mvarId 1 [] (useNamesForExplicitOnly := false) preserveBinderNames
   return (fvarIds[0]!, mvarId)
 
-/--
-Introduce one binder.
--/
+/-- Introduce one object from the goal `mvarid`, without preserving the name used in the binder.
+Returns a pair made of the newly introduced variable (which will have an inaccessible name)
+and the new goal. This will fail if there is nothing to introduce, ie when the goal
+does not start with a forall, lambda or let. -/
 abbrev _root_.Lean.MVarId.intro1 (mvarId : MVarId) : MetaM (FVarId × MVarId) :=
   intro1Core mvarId false
 
@@ -146,9 +147,10 @@ abbrev _root_.Lean.MVarId.intro1 (mvarId : MVarId) : MetaM (FVarId × MVarId) :=
 abbrev intro1 (mvarId : MVarId) : MetaM (FVarId × MVarId) :=
   mvarId.intro1
 
-/--
-Introduce one binder. The new hypothesis is named using the binder name.
--/
+/-- Introduce one object from the goal `mvarid`, preserving the name used in the binder.
+Returns a pair made of the newly introduced variable and the new goal.
+This will fail if there is nothing to introduce, ie when the goal
+does not start with a forall, lambda or let. -/
 abbrev _root_.Lean.MVarId.intro1P (mvarId : MVarId) : MetaM (FVarId × MVarId) :=
   intro1Core mvarId true
 
diff --git a/src/Lean/Meta/Tactic/Util.lean b/src/Lean/Meta/Tactic/Util.lean
index 5ad403bef1..69038bac00 100644
--- a/src/Lean/Meta/Tactic/Util.lean
+++ b/src/Lean/Meta/Tactic/Util.lean
@@ -10,7 +10,7 @@ import Lean.Meta.PPGoal
 
 namespace Lean.Meta
 
-/-- Aka user name -/
+/-- Get the user name of the given metavariable. -/
 def _root_.Lean.MVarId.getTag (mvarId : MVarId) : MetaM Name :=
   return (← mvarId.getDecl).userName
 
@@ -45,9 +45,7 @@ def throwTacticEx (tacticName : Name) (mvarId : MVarId) (msg : MessageData) : Me
 def throwNestedTacticEx {α} (tacticName : Name) (ex : Exception) : MetaM α := do
   throwError "tactic '{tacticName}' failed, nested error:\n{ex.toMessageData}"
 
-/--
-Throw error message if `mvarId` is already assigned.
--/
+/-- Throw a tactic exception with given tactic name if the given metavariable is assigned. -/
 def _root_.Lean.MVarId.checkNotAssigned (mvarId : MVarId) (tacticName : Name) : MetaM Unit := do
   if (← mvarId.isAssigned) then
     throwTacticEx tacticName mvarId "metavariable has already been assigned"
@@ -56,6 +54,7 @@ def _root_.Lean.MVarId.checkNotAssigned (mvarId : MVarId) (tacticName : Name) :
 def checkNotAssigned (mvarId : MVarId) (tacticName : Name) : MetaM Unit := do
   mvarId.checkNotAssigned tacticName
 
+/-- Get the type the given metavariable. -/
 def _root_.Lean.MVarId.getType (mvarId : MVarId) : MetaM Expr :=
   return (← mvarId.getDecl).type
 
@@ -63,6 +62,8 @@ def _root_.Lean.MVarId.getType (mvarId : MVarId) : MetaM Expr :=
 def getMVarType (mvarId : MVarId) : MetaM Expr :=
   mvarId.getType
 
+/-- Get the type the given metavariable after instantiating metavariables and reducing to
+weak head normal form. -/
 def _root_.Lean.MVarId.getType' (mvarId : MVarId) : MetaM Expr := do
   whnf (← instantiateMVars (← mvarId.getType))