diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index af04faa2e1..8b0dcc06c0 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -864,7 +864,7 @@ instance : Inhabited UInt8 where
   default := UInt8.ofNatCore 0 (by decide)
 
 def UInt16.size : Nat := 65536
-/-- Unsigned, 16-bit integer. -/
+/-- Unsigned 16-bit integer. -/
 structure UInt16 where
   val : Fin UInt16.size
 
@@ -971,7 +971,7 @@ theorem usize_size_eq : Or (Eq USize.size 4294967296) (Eq USize.size 18446744073
   | _, Or.inr rfl => Or.inr (by decide)
 
 /-- A USize is an unsigned integer with the size of a word
-for the platform's arctitecture.
+for the platform's architecture.
 
 For example, if running on a 32-bit machine, USize is equivalent to UInt32.
 Or on a 64-bit machine, UInt64.
diff --git a/src/Lean/Meta/MatchUtil.lean b/src/Lean/Meta/MatchUtil.lean
index c9c98c7f96..06d1a924c4 100644
--- a/src/Lean/Meta/MatchUtil.lean
+++ b/src/Lean/Meta/MatchUtil.lean
@@ -19,7 +19,7 @@ namespace Lean.Meta
   | none => p? (← whnf e)
   | s    => return s
 
-/-- matches `e` with `lhs = rhs : α` and returns `(α, lhs, rhs)`. -/
+/-- Matches `e` with `lhs = (rhs : α)` and returns `(α, lhs, rhs)`. -/
 def matchEq? (e : Expr) : MetaM (Option (Expr × Expr × Expr)) :=
   matchHelper? e fun e => return Expr.eq? e
 
diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean
index bb6819ab0a..97da8f3c6d 100644
--- a/src/Lean/MetavarContext.lean
+++ b/src/Lean/MetavarContext.lean
@@ -421,10 +421,10 @@ def assignLevelMVar [MonadMCtx m] (mvarId : MVarId) (val : Level) : m Unit :=
   modifyMCtx fun m => { m with lAssignment := m.lAssignment.insert mvarId val, usedAssignment := true }
 
 /--
-  Add `mvarId := u` to the metavariable assignment.
-  This method does not check whether `mvarId` is already assigned, nor it checks whether
-  a cycle is being introduced.
-  This is a low-level API, and it is safer to use `isDefEq (mkLevelMVar mvarId) u`.
+Add `mvarId := u` to the metavariable assignment.
+This method does not check whether `mvarId` is already assigned, nor it checks whether
+a cycle is being introduced, or whether the expression has the right type.
+This is a low-level API, and it is safer to use `isDefEq (mkLevelMVar mvarId) u`.
 -/
 def assignExprMVar [MonadMCtx m] (mvarId : MVarId) (val : Expr) : m Unit :=
   modifyMCtx fun m => { m with eAssignment := m.eAssignment.insert mvarId val, usedAssignment := true }