diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index a9b7fe9e68d1..9b06a789b75a 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -3231,7 +3231,7 @@ instance (σ : Type u) (m : Type u → Type v) [MonadStateOf σ m] : MonadState
 /--
 `modify (f : σ → σ)` applies the function `f` to the state.
 
-It is equivalent to `do put (f (← get))`, but `modify f` may be preferable
+It is equivalent to `do set (f (← get))`, but `modify f` may be preferable
 because the former does not use the state linearly (without sufficient inlining).
 -/
 @[always_inline, inline]
diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean
index 23f9721b6aa5..92eb53ae2d07 100644
--- a/src/Lean/Expr.lean
+++ b/src/Lean/Expr.lean
@@ -1198,10 +1198,9 @@ def hasLooseBVarInExplicitDomain : Expr → Nat → Bool → Bool
 
 /--
 Lower the loose bound variables `>= s` in `e` by `d`.
-That is, a loose bound variable `bvar i`.
-`i >= s` is mapped into `bvar (i-d)`.
+That is, a loose bound variable `bvar i` with `i >= s` is mapped to `bvar (i-d)`.
 
-Remark: if `s < d`, then result is `e`
+Remark: if `s < d`, then the result is `e`.
 -/
 @[extern "lean_expr_lower_loose_bvars"]
 opaque lowerLooseBVars (e : @& Expr) (s d : @& Nat) : Expr
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index c2c05f6cf357..87b992277fe4 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -1218,7 +1218,7 @@ def withLocalDeclD (name : Name) (type : Expr) (k : Expr → n α) : n α :=
   withLocalDecl name BinderInfo.default type k
 
 /-- Append an array of free variables `xs` to the local context and execute `k xs`.
-declInfos takes the form of an array consisting of:
+`declInfos` takes the form of an array consisting of:
 - the name of the variable
 - the binder info of the variable
 - a type constructor for the variable, where the array consists of all of the free variables
diff --git a/src/Lean/Meta/Eqns.lean b/src/Lean/Meta/Eqns.lean
index 3f07258d9ded..ae9fb789f24f 100644
--- a/src/Lean/Meta/Eqns.lean
+++ b/src/Lean/Meta/Eqns.lean
@@ -77,7 +77,7 @@ private def mkSimpleEqThm (declName : Name) : MetaM (Option Name) := do
 
 /--
   Return equation theorems for the given declaration.
-  By default, we not create equation theorems for nonrecursive definitions.
+  By default, we do not create equation theorems for nonrecursive definitions.
   You can use `nonRec := true` to override this behavior, a dummy `rfl` proof is created on the fly.
 -/
 def getEqnsFor? (declName : Name) (nonRec := false) : MetaM (Option (Array Name)) := withLCtx {} {} do