diff --git a/src/Init/Control/Basic.lean b/src/Init/Control/Basic.lean
index 39d158933a..b0b780622d 100644
--- a/src/Init/Control/Basic.lean
+++ b/src/Init/Control/Basic.lean
@@ -135,6 +135,13 @@ instance : ToBool Bool where
   | true  => t
   | false => f
 
+/--
+Converts the result of the monadic action `x` to a `Bool`. If it is `true`, returns it and ignores
+`y`; otherwise, runs `y` and returns its result.
+
+This a monadic counterpart to the short-circuiting `||` operator, usually accessed via the `<||>`
+operator.
+-/
 @[macro_inline] def orM {m : Type u → Type v} {β : Type u} [Monad m] [ToBool β] (x y : m β) : m β := do
   let b ← x
   match toBool b with
@@ -145,6 +152,13 @@ infixr:30 " <||> " => orM
 
 recommended_spelling "orM" for "<||>" in [orM, «term_<||>_»]
 
+/--
+Converts the result of the monadic action `x` to a `Bool`. If it is `true`, returns `y`; otherwise,
+returns the original result of `x`.
+
+This a monadic counterpart to the short-circuiting `&&` operator, usually accessed via the `<&&>`
+operator.
+-/
 @[macro_inline] def andM {m : Type u → Type v} {β : Type u} [Monad m] [ToBool β] (x y : m β) : m β := do
   let b ← x
   match toBool b with
@@ -155,6 +169,9 @@ infixr:35 " <&&> " => andM
 
 recommended_spelling "andM" for "<&&>" in [andM, «term_<&&>_»]
 
+/--
+Runs a monadic action and returns the negation of its result.
+-/
 @[macro_inline] def notM {m : Type → Type v} [Applicative m] (x : m Bool) : m Bool :=
   not <$> x
 
diff --git a/src/Init/Control/Except.lean b/src/Init/Control/Except.lean
index 48604b6326..1ee7ec24ec 100644
--- a/src/Init/Control/Except.lean
+++ b/src/Init/Control/Except.lean
@@ -265,13 +265,24 @@ instance (ε : Type u) (m : Type u → Type v) [Monad m] : MonadControl m (Excep
   liftWith f := liftM <| f fun x => x.run
   restoreM x := x
 
+/--
+Monads that provide the ability to ensure an action happens, regardless of exceptions or other
+failures.
+
+`MonadFinally.tryFinally'` is used to desugar `try ... finally ...` syntax.
+-/
 class MonadFinally (m : Type u → Type v) where
-  /-- `tryFinally' x f` runs `x` and then the "finally" computation `f`.
-  When `x` succeeds with `a : α`, `f (some a)` is returned. If `x` fails
-  for `m`'s definition of failure, `f none` is returned. Hence `tryFinally'`
-  can be thought of as performing the same role as a `finally` block in
-  an imperative programming language. -/
-  tryFinally' {α β} : m α → (Option α → m β) → m (α × β)
+  /--
+  Runs an action, ensuring that some other action always happens afterward.
+
+  More specifically, `tryFinally' x f` runs `x` and then the “finally” computation `f`. If `x`
+  succeeds with some value `a : α`, `f (some a)` is returned. If `x` fails for `m`'s definition of
+  failure, `f none` is returned.
+
+  `tryFinally'` can be thought of as performing the same role as a `finally` block in an imperative
+  programming language.
+  -/
+  tryFinally' {α β} : (x : m α) → (f : Option α → m β) → m (α × β)
 
 export MonadFinally (tryFinally')
 
diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 2bf1b13fb3..c4272025bb 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -865,37 +865,55 @@ noncomputable def HEq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : {β : S
 noncomputable def HEq.elim {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : HEq a b) (h₂ : p a) : p b :=
   eq_of_heq h₁ ▸ h₂
 
+/-- Substitution with heterogeneous equality. -/
 theorem HEq.subst {p : (T : Sort u) → T → Prop} (h₁ : HEq a b) (h₂ : p α a) : p β b :=
   HEq.ndrecOn h₁ h₂
 
+/-- Heterogeneous equality is symmetric. -/
 @[symm] theorem HEq.symm (h : HEq a b) : HEq b a :=
   h.rec (HEq.refl a)
 
+/-- Propositionally equal terms are also heterogeneously equal. -/
 theorem heq_of_eq (h : a = a') : HEq a a' :=
   Eq.subst h (HEq.refl a)
 
+/-- Heterogeneous equality is transitive. -/
 theorem HEq.trans (h₁ : HEq a b) (h₂ : HEq b c) : HEq a c :=
   HEq.subst h₂ h₁
 
+/-- Heterogeneous equality precomposes with propositional equality. -/
 theorem heq_of_heq_of_eq (h₁ : HEq a b) (h₂ : b = b') : HEq a b' :=
   HEq.trans h₁ (heq_of_eq h₂)
 
+/-- Heterogeneous equality postcomposes with propositional equality. -/
 theorem heq_of_eq_of_heq (h₁ : a = a') (h₂ : HEq a' b) : HEq a b :=
   HEq.trans (heq_of_eq h₁) h₂
 
+/-- If two terms are heterogeneously equal then their types are propositionally equal. -/
 theorem type_eq_of_heq (h : HEq a b) : α = β :=
   h.rec (Eq.refl α)
 
 end
 
+/--
+Rewriting inside `φ` using `Eq.recOn` yields a term that's heterogeneously equal to the original
+term.
+-/
 theorem eqRec_heq {α : Sort u} {φ : α → Sort v} {a a' : α} : (h : a = a') → (p : φ a) → HEq (Eq.recOn (motive := fun x _ => φ x) h p) p
   | rfl, p => HEq.refl p
 
+/--
+If casting a term with `Eq.rec` to another type makes it equal to some other term, then the two
+terms are heterogeneously equal.
+-/
 theorem heq_of_eqRec_eq {α β : Sort u} {a : α} {b : β} (h₁ : α = β) (h₂ : Eq.rec (motive := fun α _ => α) a h₁ = b) : HEq a b := by
   subst h₁
   apply heq_of_eq
   exact h₂
 
+/--
+The result of casting a term with `cast` is heterogeneously equal to the original term.
+-/
 theorem cast_heq {α β : Sort u} : (h : α = β) → (a : α) → HEq (cast h a) a
   | rfl, a => HEq.refl a
 
diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index 5ea3c79feb..171716041b 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -748,7 +748,10 @@ def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α 
 
 @[deprecated mapM (since := "2024-11-11")] abbrev sequenceMap := @mapM
 
-/-- Variant of `mapIdxM` which receives the index `i` along with the bound `i < as.size`. -/
+/--
+Applies the monadic action `f` to every element in the array, along with the element's index and a
+proof that the index is in bounds, from left to right. Returns the array of results.
+-/
 @[inline]
 def mapFinIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m]
     (as : Array α) (f : (i : Nat) → α → (h : i < as.size) → m β) : m (Array β) :=
@@ -763,6 +766,10 @@ def mapFinIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m]
       map i (j+1) this (bs.push (← f j as[j] j_lt))
   map as.size 0 rfl (emptyWithCapacity as.size)
 
+/--
+Applies the monadic action `f` to every element in the array, along with the element's index, from
+left to right. Returns the array of results.
+-/
 @[inline]
 def mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : Nat → α → m β) (as : Array α) : m (Array β) :=
   as.mapFinIdxM fun i a _ => f i a
diff --git a/src/Init/Data/Array/Subarray.lean b/src/Init/Data/Array/Subarray.lean
index dc912e46d5..57cf7eb5cb 100644
--- a/src/Init/Data/Array/Subarray.lean
+++ b/src/Init/Data/Array/Subarray.lean
@@ -7,6 +7,7 @@ prelude
 import Init.Data.Array.Basic
 
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.missingDocs true
 
 universe u v w
 
@@ -25,7 +26,18 @@ structure Subarray (α : Type u) where
   start : Nat
   /-- The ending index of the region of interest (exclusive). -/
   stop : Nat
+  /--
+  The starting index is no later than the ending index.
+
+  The ending index is exclusive. If the starting and ending indices are equal, then the subarray is
+  empty.
+  -/
   start_le_stop : start ≤ stop
+  /-- The stopping index is no later than the end of the array.
+
+  The ending index is exclusive. If it is equal to the size of the array, then the last element of
+  the array is in the subarray.
+  -/
   stop_le_array_size : stop ≤ array.size
 
 namespace Subarray
@@ -110,6 +122,12 @@ instance : EmptyCollection (Subarray α) :=
 instance : Inhabited (Subarray α) :=
   ⟨{}⟩
 
+/--
+The run-time implementation of `ForIn.forIn` for `Subarray`, which allows it to be used with `for`
+loops in `do`-notation.
+
+This definition replaces `Subarray.forIn`.
+-/
 @[inline] unsafe def forInUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (s : Subarray α) (b : β) (f : α → β → m (ForInStep β)) : m β :=
   let sz := USize.ofNat s.stop
   let rec @[specialize] loop (i : USize) (b : β) : m β := do
@@ -122,6 +140,10 @@ instance : Inhabited (Subarray α) :=
       pure b
   loop (USize.ofNat s.start) b
 
+/--
+The implementation of `ForIn.forIn` for `Subarray`, which allows it to be used with `for` loops in
+`do`-notation.
+-/
 -- TODO: provide reference implementation
 @[implemented_by Subarray.forInUnsafe]
 protected opaque forIn {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (s : Subarray α) (b : β) (f : α → β → m (ForInStep β)) : m β :=
diff --git a/src/Init/Data/OfScientific.lean b/src/Init/Data/OfScientific.lean
index 01b7b51c26..21d232f036 100644
--- a/src/Init/Data/OfScientific.lean
+++ b/src/Init/Data/OfScientific.lean
@@ -17,6 +17,16 @@ import Init.Data.Nat.Log2
    Note the use of `nat_lit`; there is no wrapping `OfNat.ofNat` in the resulting term.
 -/
 class OfScientific (α : Type u) where
+  /--
+  Produces a value from the given mantissa, exponent sign, and decimal exponent. For the exponent
+  sign, `true` indicates a negative exponent.
+
+   Examples:
+   - `1.23` is syntax for `OfScientific.ofScientific (nat_lit 123) true (nat_lit 2)`
+   - `121e100` is syntax for `OfScientific.ofScientific (nat_lit 121) false (nat_lit 100)`
+
+   Note the use of `nat_lit`; there is no wrapping `OfNat.ofNat` in the resulting term.
+  -/
   ofScientific (mantissa : Nat) (exponentSign : Bool) (decimalExponent : Nat) : α
 
 /-- Computes `m * 2^e`. -/
diff --git a/src/Init/Data/Random.lean b/src/Init/Data/Random.lean
index 086816af77..2bdacf84d9 100644
--- a/src/Init/Data/Random.lean
+++ b/src/Init/Data/Random.lean
@@ -34,11 +34,15 @@ structure StdGen where
 
 instance : Inhabited StdGen := ⟨{ s1 := 0, s2 := 0 }⟩
 
+/-- The range of values returned by `StdGen` -/
 def stdRange := (1, 2147483562)
 
 instance : Repr StdGen where
   reprPrec | ⟨s1, s2⟩, _ => Std.Format.bracket "⟨" (repr s1 ++ ", " ++ repr s2) "⟩"
 
+/--
+The next value from a `StdGen`, paired with an updated generator state.
+-/
 def stdNext : StdGen → Nat × StdGen
   | ⟨s1, s2⟩ =>
     let k    : Int := Int.ofNat (s1 / 53668)
@@ -51,6 +55,9 @@ def stdNext : StdGen → Nat × StdGen
     let z'   : Nat := if z < 1 then (z + 2147483562).toNat else z.toNat % 2147483562
     (z', ⟨s1'', s2''⟩)
 
+/--
+Splits a `StdGen` into two separate states.
+-/
 def stdSplit : StdGen → StdGen × StdGen
   | g@⟨s1, s2⟩ =>
     let newS1  := if s1 = 2147483562 then 1 else s1 + 1
diff --git a/src/Init/GetElem.lean b/src/Init/GetElem.lean
index 482d7c0d13..b093120136 100644
--- a/src/Init/GetElem.lean
+++ b/src/Init/GetElem.lean
@@ -135,13 +135,21 @@ theorem getElem_congr_idx [GetElem coll idx elem valid] {c : coll} {i j : idx} {
     (h' : i = j) : c[i] = c[j]'(h' ▸ w) := by
   cases h'; rfl
 
+/--
+Lawful `GetElem?` instances (which extend `GetElem`) are those for which the potentially-failing
+`GetElem?.getElem?` and `GetElem?.getElem!` operators succeed when the validity predicate is
+satisfied, and fail when it is not.
+-/
 class LawfulGetElem (cont : Type u) (idx : Type v) (elem : outParam (Type w))
    (dom : outParam (cont → idx → Prop)) [ge : GetElem? cont idx elem dom] : Prop where
 
+  /-- `GetElem?.getElem?` succeeds when the validity predicate is satisfied and fails otherwise. -/
   getElem?_def (c : cont) (i : idx) [Decidable (dom c i)] :
       c[i]? = if h : dom c i then some (c[i]'h) else none := by
     intros
     try simp only [getElem?] <;> congr
+
+  /-- `GetElem?.getElem!` succeeds and fails when `GetElem.getElem?` succeeds and fails. -/
   getElem!_def [Inhabited elem] (c : cont) (i : idx) :
       c[i]! = match c[i]? with | some e => e | none => default := by
     intros
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 0bf0b18e49..13dcc0e5c0 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -483,6 +483,7 @@ inductive HEq : {α : Sort u} → α → {β : Sort u} → β → Prop where
 @[match_pattern] protected def HEq.rfl {α : Sort u} {a : α} : HEq a a :=
   HEq.refl a
 
+/-- If two heterogeneously equal terms have the same type, then they are propositionally equal. -/
 theorem eq_of_heq {α : Sort u} {a a' : α} (h : HEq a a') : Eq a a' :=
   have : (α β : Sort u) → (a : α) → (b : β) → HEq a b → (h : Eq α β) → Eq (cast h a) b :=
     fun _ _ _ _ h₁ =>
diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean
index d9079377c1..c222e2fe8a 100644
--- a/src/Init/System/IO.lean
+++ b/src/Init/System/IO.lean
@@ -1573,6 +1573,10 @@ end CancelToken
 namespace FS
 namespace Stream
 
+/--
+Creates a Lean stream from a file handle. Each stream operation is implemented by the corresponding
+file handle operation.
+-/
 @[export lean_stream_of_handle]
 def ofHandle (h : Handle) : Stream where
   flush   := Handle.flush h
diff --git a/src/Init/System/ST.lean b/src/Init/System/ST.lean
index a93a2e92f8..a8aba27643 100644
--- a/src/Init/System/ST.lean
+++ b/src/Init/System/ST.lean
@@ -122,6 +122,9 @@ end Prim
 section
 variable {σ : Type} {m : Type → Type} [Monad m] [MonadLiftT (ST σ) m]
 
+/--
+Creates a new mutable reference that contains the provided value `a`.
+-/
 @[inline] def mkRef {α : Type} (a : α) : m (Ref σ α) :=  liftM <| Prim.mkRef a
 /--
 Reads the value of a mutable reference.
diff --git a/src/Init/WF.lean b/src/Init/WF.lean
index 10c0f52ea8..665d9c09b1 100644
--- a/src/Init/WF.lean
+++ b/src/Init/WF.lean
@@ -52,10 +52,22 @@ a well founded relation, then the function terminates.
 Well-founded relations are sometimes called _Artinian_ or said to satisfy the “descending chain condition”.
 -/
 inductive WellFounded {α : Sort u} (r : α → α → Prop) : Prop where
+  /--
+  If all elements are accessible via `r`, then `r` is well-founded.
+  -/
   | intro (h : ∀ a, Acc r a) : WellFounded r
 
+/--
+A type that has a standard well-founded relation.
+
+Instances are used to prove that functions terminate using well-founded recursion by showing that
+recursive calls reduce some measure according to a well-founded relation. This relation can combine
+well-founded relations on the recursive function's parameters.
+-/
 class WellFoundedRelation (α : Sort u) where
+  /-- A well-founded relation on `α`. -/
   rel : α → α → Prop
+  /-- A proof that `rel` is, in fact, well-founded. -/
   wf  : WellFounded rel
 
 namespace WellFounded
@@ -88,6 +100,13 @@ end
 
 variable {α : Sort u} {C : α → Sort v} {r : α → α → Prop}
 
+/--
+A well-founded fixpoint. If satisfying the motive `C` for all values that are smaller according to a
+well-founded relation allows it to be satisfied for the current value, then it is satisfied for all
+values.
+
+This function is used as part of the elaboration of well-founded recursion.
+-/
 -- Well-founded fixpoint
 noncomputable def fix (hwf : WellFounded r) (F : ∀ x, (∀ y, r y x → C y) → C x) (x : α) : C x :=
   fixF F x (apply hwf x)
@@ -145,6 +164,9 @@ theorem wf (f : α → β) (h : WellFounded r) : WellFounded (InvImage r f) :=
   ⟨fun a => accessible f (apply h (f a))⟩
 end InvImage
 
+/--
+The inverse image of a well-founded relation is well-founded.
+-/
 @[reducible] def invImage (f : α → β) (h : WellFoundedRelation β) : WellFoundedRelation α where
   rel := InvImage h.rel f
   wf  := InvImage.wf f h.wf
diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index 3278b73235..10c40c9558 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -35,7 +35,19 @@ structure Context where
   -/
   recover    : Bool := true
 
+/--
+The tactic monad, which extends the term elaboration monad `TermElabM` with state that contains the
+current goals (`Lean.Elab.Tactic.State`, accessible via `MonadStateOf`) and local information about
+the current tactic's name and whether error recovery is enabled (`Lean.Elab.Tactic.Context`,
+accessible via `MonadReaderOf`).
+-/
 abbrev TacticM := ReaderT Context $ StateRefT State TermElabM
+/--
+A tactic is a function from syntax to an action in the tactic monad.
+
+A given tactic syntax kind may have multiple `Tactic`s associated with it, all of which will be
+attempted until one succeeds.
+-/
 abbrev Tactic  := Syntax → TacticM Unit
 
 /-
diff --git a/src/Lean/Meta/Tactic/Simp/Attr.lean b/src/Lean/Meta/Tactic/Simp/Attr.lean
index 6df5b95680..7ac1fe261a 100644
--- a/src/Lean/Meta/Tactic/Simp/Attr.lean
+++ b/src/Lean/Meta/Tactic/Simp/Attr.lean
@@ -56,6 +56,16 @@ def mkSimpAttr (attrName : Name) (attrDescr : String) (ext : SimpExtension)
         modifyEnv fun env => ext.modifyState env fun _ => s
   }
 
+/--
+Registers the given name as a custom simp set. Applying the name as an attribute to a name adds it
+to the simp set, and using the name as a parameter to the `simp` tactic causes `simp` to use the
+included lemmas.
+
+Custom simp sets must be registered during [initialization](lean-manual://section/initialization).
+
+The description should be a short, singular noun phrase that describes the contents of the custom
+simp set.
+-/
 def registerSimpAttr (attrName : Name) (attrDescr : String)
     (ref : Name := by exact decl_name%) : IO SimpExtension := do
   let ext ← mkSimpExt ref
diff --git a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
index dd30ed75dd..8a4667764d 100644
--- a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
+++ b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
@@ -192,6 +192,9 @@ instance : BEq SimpTheorem where
 
 abbrev SimpTheoremTree := DiscrTree SimpTheorem
 
+/--
+The theorems in a simp set.
+-/
 structure SimpTheorems where
   pre          : SimpTheoremTree := DiscrTree.empty
   post         : SimpTheoremTree := DiscrTree.empty
@@ -423,6 +426,12 @@ inductive SimpEntry where
   | toUnfoldThms : Name → Array Name → SimpEntry
   deriving Inhabited
 
+/--
+The environment extension that contains a simp set, returned by `Lean.Meta.registerSimpAttr`.
+
+Use the simp set's attribute or `Lean.Meta.addSimpTheorem` to add theorems to the simp set. Use
+`Lean.Meta.SimpExtension.getTheorems` to get the contents.
+-/
 abbrev SimpExtension := SimpleScopedEnvExtension SimpEntry SimpTheorems
 
 def SimpExtension.getTheorems (ext : SimpExtension) : CoreM SimpTheorems :=
diff --git a/src/lake/Lake/Config/Monad.lean b/src/lake/Lake/Config/Monad.lean
index 8f426c846e..923586f07a 100644
--- a/src/lake/Lake/Config/Monad.lean
+++ b/src/lake/Lake/Config/Monad.lean
@@ -28,6 +28,7 @@ abbrev LakeEnvT := ReaderT Lake.Env
 
 /-- A monad equipped with a (read-only) Lake `Workspace`. -/
 class MonadWorkspace (m : Type → Type u) where
+  /-- Gets the current Lake workspace. -/
   getWorkspace : m Workspace
 
 export MonadWorkspace (getWorkspace)
@@ -128,6 +129,9 @@ variable [MonadLakeEnv m]
 
 /-! ## Environment Helpers -/
 
+/--
+Gets the current Lake environment.
+-/
 @[inline] def getLakeEnv : m Lake.Env :=
   read