diff --git a/docs/1000.yaml b/docs/1000.yaml
index 3b964c85b25017..d1f98c60ad5cfe 100644
--- a/docs/1000.yaml
+++ b/docs/1000.yaml
@@ -3506,7 +3506,7 @@ Q6799039:
 
 Q6813106:
   title: Mellin inversion theorem
-  decl: mellin_inversion
+  decl: mellinInv_mellin_eq
 
 Q6859627:
   title: Milliken's tree theorem
@@ -3623,7 +3623,6 @@ Q7208500:
   title: Poisson limit theorem
   decls:
     - ProbabilityTheory.tendsto_choose_mul_pow_of_tendsto_mul_atTop
-    - ProbabilityTheory.binomial_tendsto_poissonPMFReal_atTop
   authors: Yi Yuan
   date: 2026
 
diff --git a/docs/overview.yaml b/docs/overview.yaml
index 8418077fbae180..03223f0a7ed66c 100644
--- a/docs/overview.yaml
+++ b/docs/overview.yaml
@@ -12,7 +12,7 @@ General algebra:
     presheafed space: 'AlgebraicGeometry.PresheafedSpace'
     sheafed space: 'AlgebraicGeometry.SheafedSpace'
     monoidal category: 'CategoryTheory.MonoidalCategory'
-    Cartesian closed: 'CategoryTheory.CartesianClosed'
+    Cartesian closed: 'CategoryTheory.MonoidalClosed'
     abelian category: 'CategoryTheory.Abelian'
 
   Numbers:
@@ -129,7 +129,7 @@ General algebra:
     splitting field: 'Polynomial.SplittingField'
     perfect closure: 'PerfectClosure'
     Galois correspondence: 'IsGalois.intermediateFieldEquivSubgroup'
-    Abel-Ruffini theorem (one direction): 'solvableByRad.isSolvable'
+    Abel-Ruffini theorem (one direction): 'isSolvable_gal_minpoly'
 
   Homological algebra:
     chain complex: 'ChainComplex'
@@ -146,7 +146,7 @@ General algebra:
     Chevalley-Warning theorem: 'char_dvd_card_solutions'
     "Hensel's lemma (for $\\mathbb{Z}_p$)": 'hensels_lemma'
     ring of Witt vectors: 'WittVector'
-    perfection of a ring: 'Ring.Perfection'
+    perfection of a ring: 'Perfection'
   Transcendental numbers:
     Liouville's theorem on existence of transcendental numbers: 'transcendental_liouvilleNumber'
 
@@ -200,7 +200,7 @@ Linear algebra:
     bilinear form: 'LinearMap.BilinForm'
     alternating bilinear form: 'LinearMap.BilinForm.IsAlt'
     symmetric bilinear form: 'LinearMap.BilinForm.IsSymm'
-    matrix representation: 'BilinForm.toMatrix'
+    matrix representation: 'LinearMap.BilinForm.toMatrix'
     quadratic form: 'QuadraticForm'
     polar form of a quadratic: 'QuadraticMap.polar'
   Finite-dimensional inner product spaces (see also Hilbert spaces, below):
@@ -366,7 +366,7 @@ Analysis:
     principle of isolated zeros: 'AnalyticAt.eventually_eq_zero_or_eventually_ne_zero'
     principle of analytic continuation: 'AnalyticOnNhd.eqOn_of_preconnected_of_frequently_eq'
     analyticity of holomorphic functions: 'DifferentiableOn.analyticAt'
-    Schwarz lemma: 'Complex.norm_le_norm_of_mapsTo_ball_self'
+    Schwarz lemma: 'Complex.norm_le_norm_of_mapsTo_ball'
     removable singularity: 'Complex.differentiableOn_update_limUnder_insert_of_isLittleO'
     Phragmen-Lindelöf principle: 'PhragmenLindelof.horizontal_strip'
     fundamental theorem of algebra: 'Complex.isAlgClosed'
@@ -420,7 +420,7 @@ Probability Theory:
     martingale: 'MeasureTheory.Martingale'
     optional stopping theorem: 'MeasureTheory.submartingale_iff_expected_stoppedValue_mono'
     stopping time: 'MeasureTheory.IsStoppingTime'
-    hitting time: 'MeasureTheory.hitting'
+    hitting time: 'MeasureTheory.hittingBtwn'
     Gaussian processes: 'ProbabilityTheory.IsGaussianProcess'
 
 Geometry:
diff --git a/docs/undergrad.yaml b/docs/undergrad.yaml
index c3c04b3926497d..7003d5a056e239 100644
--- a/docs/undergrad.yaml
+++ b/docs/undergrad.yaml
@@ -197,8 +197,8 @@ Bilinear and Quadratic Forms Over a Vector Space:
     alternating bilinear forms: 'LinearMap.BilinForm.IsAlt'
     symmetric bilinear forms: 'LinearMap.BilinForm.IsSymm'
     nondegenerate forms: 'LinearMap.BilinForm.Nondegenerate'
-    matrix representation: 'BilinForm.toMatrix'
-    change of coordinates: 'BilinForm.toMatrix_comp'
+    matrix representation: 'LinearMap.BilinForm.toMatrix'
+    change of coordinates: 'LinearMap.BilinForm.toMatrix_comp'
     rank of a bilinear form: ''
   Quadratic forms:
     quadratic form: 'QuadraticForm'
@@ -618,8 +618,8 @@ Distribution calculus:
     $L^p$ functions: 'MeasureTheory.Lp.toTemperedDistributionCLM'
     periodic functions: ''
     Dirac comb: ''
-    Fourier transforms: 'TemperedDistribution.fourierTransformCLM'
-    inverse Fourier transform: 'TemperedDistribution.fourierTransformInvCLM'
+    Fourier transforms: 'FourierTransform.fourierCLM'
+    inverse Fourier transform: 'FourierTransform.fourierInvCLM'
     Fourier transform and derivation: ''
     Fourier transform and convolution product: ''
   Applications: