doc(misc): fix file refs (leanprover-community#33258)

Fix or clarify some dead documentation file refs.

Author: harahu

Cache/IO.lean

@@ -459,10 +459,10 @@ Return tuples of the form ("module name", "path to .lean file").
 
 The input string `arg` takes one of the following forms:
 
-1. `Mathlib.Algebra.Fields.Basic`: there exists such a Lean file
-2. `Mathlib.Algebra.Fields`: no Lean file exists but a folder (TODO)
-3. `Mathlib/Algebra/Fields/Basic.lean`: the file exists (note potentially `\` on Windows)
-4. `Mathlib/Algebra/Fields/`: the folder exists (TODO)
+1. `Mathlib.Algebra.Field.Basic`: there exists such a Lean file
+2. `Mathlib.Algebra.Field`: no Lean file exists but a folder (TODO)
+3. `Mathlib/Algebra/Field/Basic.lean`: the file exists (note potentially `\` on Windows)
+4. `Mathlib/Algebra/Field/`: the folder exists (TODO)
 
 Not supported yet:
 

Mathlib/Deprecated/RingHom.lean

@@ -12,7 +12,7 @@ public import Mathlib.Data.Set.Insert
 /-!
 # Additional lemmas about homomorphisms of semirings and rings
 
-These lemmas were in `Mathlib/Algebra/Hom/Ring/Defs.lean` and have now been deprecated.
+These lemmas were in `Mathlib/Algebra/Ring/Hom/Defs.lean` and have now been deprecated.
 -/
 
 @[expose] public section

Mathlib/Geometry/Manifold/VectorBundle/LocalFrame.lean

@@ -27,10 +27,10 @@ Any section `s` of `e` can be uniquely written as `s = ∑ i, f^i sᵢ` near `x`
 and `s` is smooth at `x` iff the functions `f^i` are.
 
 In this file, we prove the latter statement for finite-rank bundles (with coefficients in a
-complete field). In `Mathlib/Geometry/Manifold/VectorBundle/OrthonormalFrame.lean` (#26221),
-we will prove the same for real vector bundles of any rank which admit a `C^n` bundle metric.
-This includes bundles of finite rank, modelled on a Hilbert space or on a Banach space which has
-smooth partitions of unity.
+complete field). In the planned file `Mathlib/Geometry/Manifold/VectorBundle/OrthonormalFrame.lean`
+(#26221), we will prove the same for real vector bundles of any rank which admit a `C^n` bundle
+metric. This includes bundles of finite rank, modelled on a Hilbert space or on a Banach space which
+has smooth partitions of unity.
 
 We will use this to construct local extensions of a vector to a section which is smooth on the
 trivialisation domain.

Mathlib/Init.lean

@@ -53,7 +53,7 @@ as early as possible.
 
 All linters imported here have no bulk imports;
 **Not** imported in this file are
-- the text-based linters in `Linters/TextBased.lean`, as they can be imported later
+- the text-based linters in `Mathlib/Tactic/Linter/TextBased.lean`, as they can be imported later
 - the `haveLet` linter, as it is currently disabled by default due to crashes
 - the `ppRoundTrip` linter, which is currently disabled (as this is not mature enough)
 - the `minImports` linter, as that linter is disabled by default (and has an informational function;

Mathlib/Probability/ProbabilityMassFunction/Basic.lean

@@ -14,8 +14,9 @@ public import Mathlib.MeasureTheory.Measure.Dirac
 This file is about probability mass functions or discrete probability measures:
 a function `α → ℝ≥0∞` such that the values have (infinite) sum `1`.
 
-Construction of monadic `pure` and `bind` is found in `ProbabilityMassFunction/Monad.lean`,
-other constructions of `PMF`s are found in `ProbabilityMassFunction/Constructions.lean`.
+Construction of monadic `pure` and `bind` is found in
+`Mathlib/Probability/ProbabilityMassFunction/Monad.lean`, other constructions of `PMF`s are found in
+`Mathlib/Probability/ProbabilityMassFunction/Constructions.lean`.
 
 Given `p : PMF α`, `PMF.toOuterMeasure` constructs an `OuterMeasure` on `α`,
 by assigning each set the sum of the probabilities of each of its elements.

Mathlib/Topology/UniformSpace/Ultra/Basic.lean

@@ -26,7 +26,7 @@ In this file we define `IsUltraUniformity`, a Prop mixin typeclass.
 
 ## Implementation notes
 
-As in the `Mathlib/Topology/UniformSpace/Defs.lean` file, we do not reuse `Mathlib/Data/SetRel.lean`
+As in the `Mathlib/Topology/UniformSpace/Defs.lean` file, we do not reuse `Mathlib/Data/Rel.lean`
 but rather extend the relation properties as needed.
 
 ## TODOs