doc(Tactics): fix file refs (leanprover-community#33273)

Fix some stale documentation file refs.

Author: harahu

Mathlib/Tactic/CategoryTheory/Coherence/Normalize.lean

@@ -13,7 +13,7 @@ public meta import Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
 
 This file provides a function that normalizes 2-morphisms in bicategories. The function also
 used to normalize morphisms in monoidal categories. This is used in the string diagram widget given
-in `Mathlib/Tactic/StringDiagram.lean`, as well as `monoidal` and `bicategory` tactics.
+in `Mathlib/Tactic/Widget/StringDiagram.lean`, as well as `monoidal` and `bicategory` tactics.
 
 We say that the 2-morphism `η` in a bicategory is in normal form if
 1. `η` is of the form `α₀ ≫ η₀ ≫ α₁ ≫ η₁ ≫ ... αₘ ≫ ηₘ ≫ αₘ₊₁` where each `αᵢ` is a

Mathlib/Tactic/NormNum/PowMod.lean

@@ -14,7 +14,8 @@ These expressions can often be evaluated efficiently in cases where first evalua
 then reducing mod `m` is not feasible. We provide a function `evalNatPowMod` which is used by the
 `reduce_mod_char` tactic to efficiently evaluate powers in rings with positive characteristic.
 
-The approach taken here is identical to (and copied from) the development in `NormNum/Pow.lean`.
+The approach taken here is identical to (and copied from) the development in
+`Mathlib/Tactic/NormNum/Pow.lean`.
 
 ## TODO
 

Mathlib/Tactic/TermCongr.lean

@@ -108,7 +108,7 @@ We need to decouple these to support letting the proof's elaboration be deferred
 we know whether we want an iff, eq, or heq, while also allowing it to choose
 to elaborate as an iff, eq, or heq.
 Later, the congruence generator handles any discrepancies.
-See `Mathlib/Tactic/TermCongr/CongrResult.lean`. -/
+See `CongrResult` below. -/
 @[reducible, nolint unusedArguments, expose]
 def cHole {α : Sort u} (val : α) {p : Prop} (_pf : p) : α := val