diff --git a/docs/overview.yaml b/docs/overview.yaml
index 771307bcabe793..eb74a4f96c3769 100644
--- a/docs/overview.yaml
+++ b/docs/overview.yaml
@@ -244,7 +244,7 @@ Topology:
     order topology: 'OrderTopology'
     intermediate value theorem: 'intermediate_value_Icc'
     extreme value theorem: 'IsCompact.exists_isMinOn'
-    limit infimum and supremum: 'order/liminf_limsup.html'
+    limit infimum and supremum: 'Mathlib/Order/LiminfLimsup.html'
     topological group: 'IsTopologicalGroup'
     completion of an abelian topological group: 'UniformSpace.Completion.instAddCommGroup'
     infinite sum: 'HasSum'
@@ -306,7 +306,7 @@ Analysis:
     derivative of the inverse of a function: 'HasFDerivAt.of_local_left_inverse'
     Rolle's theorem: 'exists_deriv_eq_zero'
     mean value theorem: 'exists_ratio_deriv_eq_ratio_slope'
-    Taylor's theorem: 'analysis/calculus/taylor.html'
+    Taylor's theorem: 'Mathlib/Analysis/Calculus/Taylor.html'
     $C^k$ function: 'ContDiff'
     Leibniz formula: 'fderiv_mul'
     local extrema: 'IsLocalMin.fderiv_eq_zero'
@@ -319,7 +319,7 @@ Analysis:
     characterization of convexity: 'convexOn_of_deriv2_nonneg'
     Jensen's inequality (finite sum version): 'ConvexOn.map_sum_le'
     Jensen's inequality (integral version): 'ConvexOn.map_integral_le'
-    convexity inequalities: 'analysis/mean_inequalities.html'
+    convexity inequalities: 'Mathlib/Analysis/MeanInequalities.html'
     Carathéodory's theorem: 'convexHull_eq_union'
 
   Special functions:
diff --git a/docs/undergrad.yaml b/docs/undergrad.yaml
index d826cac30a1997..6295168a54236f 100644
--- a/docs/undergrad.yaml
+++ b/docs/undergrad.yaml
@@ -172,7 +172,7 @@ Ring Theory:
     characteristic of a ring: 'ringChar'
     characteristic zero: 'CharZero'
     characteristic p: 'CharP'
-    Subfields: 'field_theory/subfield.html'
+    Subfields: 'Subfield'
     Frobenius morphisms: 'frobenius'
     field $\Q$ of rational numbers: 'Rat.instField'
     field $\R$ of real numbers: 'Real.instField'
@@ -185,7 +185,7 @@ Ring Theory:
     algebraically closed fields: 'IsAlgClosed'
     rupture fields: 'AdjoinRoot'
     splitting fields: 'Polynomial.SplittingField'
-    finite fields: 'field_theory/finite.html'
+    finite fields: 'Mathlib/FieldTheory/Finite/Basic.html'
     rational fraction fields with one indeterminate over a field: 'RatFunc'
     $\R(X)$-partial fraction decomposition: 'https://en.wikipedia.org/wiki/Partial_fraction_decomposition#General_result'
     $\C(X)$-partial fraction decomposition: 'https://en.wikipedia.org/wiki/Partial_fraction_decomposition#Statement'
@@ -283,7 +283,7 @@ Single Variable Real Analysis:
     convergence: 'Filter.Tendsto'
     limit point: 'MapClusterPt'
     recurrent sequences: 'Nat'
-    limit infimum and supremum: 'order/liminf_limsup.html'
+    limit infimum and supremum: 'Mathlib/Order/LiminfLimsup.html'
     Cauchy sequences: 'CauchySeq'
   Topology of R:
     metric structure: 'Real.metricSpace'
@@ -360,7 +360,7 @@ Single Variable Real Analysis:
       continuity: 'ConvexOn.continuousOn'
       differentiability: 'https://en.wikipedia.org/wiki/Convex_function#Functions_of_one_variable'
     characterizations of convexity: 'convexOn_of_deriv2_nonneg'
-    convexity inequalities: 'analysis/mean_inequalities.html'
+    convexity inequalities: 'Mathlib/Analysis/MeanInequalities.html'
 
 # 7.
 Single Variable Complex Analysis: