chore: fix spelling mistakes (#17364)

Cache/Hashing.lean

@@ -73,9 +73,9 @@ def getRootHash : CacheM UInt64 := do
       pure id
     else
       pure ((← mathlibDepPath) / ·)
-  let hashs ← rootFiles.mapM fun path =>
+  let hashes ← rootFiles.mapM fun path =>
     hashFileContents <$> IO.FS.readFile (qualifyPath path)
-  return hash (hash Lean.githash :: hashs)
+  return hash (hash Lean.githash :: hashes)
 
 /--
 Computes the hash of a file, which mixes:

Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean

@@ -18,7 +18,7 @@ arbitrary choice in the definition.
 
 We also define a predicate `HasFTaylorSeriesUpTo` (and its localized version
 `HasFTaylorSeriesUpToOn`), saying that a sequence of multilinear maps is *a* sequence of
-derivatives of `f`. Contrary to `iteratedFDerivWithin`, it accomodates well the
+derivatives of `f`. Contrary to `iteratedFDerivWithin`, it accommodates well the
 non-uniqueness of derivatives.
 
 ## Main definitions and results

Mathlib/Analysis/Calculus/Deriv/Abs.lean

@@ -10,7 +10,7 @@ import Mathlib.Analysis.InnerProductSpace.Calculus
 # Derivative of the absolute value
 
 This file compiles basic derivability properties of the absolute value, and is largely inspired
-from `Mathlib.Analysis.InnerProductSpace.Calculus`, which is the analoguous file for norms derived
+from `Mathlib.Analysis.InnerProductSpace.Calculus`, which is the analogous file for norms derived
 from an inner product space.
 
 ## Tags

Mathlib/Analysis/Normed/Ring/IsPowMulFaithful.lean

@@ -58,7 +58,7 @@ theorem contraction_of_isPowMul {α β : Type*} [SeminormedRing α] [SeminormedR
   contraction_of_isPowMul_of_boundedWrt (SeminormedRing.toRingSeminorm α) hβ hf x
 
 /-- Given two power-multiplicative ring seminorms `f, g` on `α`, if `f` is bounded by a positive
-  multiple of `g` and viceversa, then `f = g`. -/
+  multiple of `g` and vice versa, then `f = g`. -/
 theorem eq_seminorms {F : Type*} {α : outParam (Type*)} [Ring α] [FunLike F α ℝ]
     [RingSeminormClass F α ℝ] {f g : F} (hfpm : IsPowMul f) (hgpm : IsPowMul g)
     (hfg : ∃ (r : ℝ) (_ : 0 < r), ∀ a : α, f a ≤ r * g a)

Mathlib/CategoryTheory/Comma/Over.lean

@@ -675,7 +675,7 @@ def ofStructuredArrowProjEquivalence (F : D ⥤ T) (Y : T) (X : D) :
   counitIso := NatIso.ofComponents (fun _ => Iso.refl _) (by aesop_cat)
 
 /-- The canonical functor from the structured arrow category on the diagonal functor
-`T ⥤ T × T` to the the structured arrow category on `Under.forget`. -/
+`T ⥤ T × T` to the structured arrow category on `Under.forget`. -/
 @[simps!]
 def ofDiagEquivalence.functor (X : T × T) :
     StructuredArrow X (Functor.diag _) ⥤ StructuredArrow X.2 (Under.forget X.1) :=
@@ -741,7 +741,7 @@ def ofCostructuredArrowProjEquivalence (F : T ⥤ D) (Y : D) (X : T) :
   counitIso := NatIso.ofComponents (fun _ => Iso.refl _) (by aesop_cat)
 
 /-- The canonical functor from the costructured arrow category on the diagonal functor
-`T ⥤ T × T` to the the costructured arrow category on `Under.forget`. -/
+`T ⥤ T × T` to the costructured arrow category on `Under.forget`. -/
 @[simps!]
 def ofDiagEquivalence.functor (X : T × T) :
     CostructuredArrow (Functor.diag _) X ⥤ CostructuredArrow (Over.forget X.1) X.2 :=

Mathlib/CategoryTheory/Galois/IsFundamentalgroup.lean

@@ -219,7 +219,7 @@ variable (G : Type*) [Group G] [∀ (X : C), MulAction G (F.obj X)]
 
 /-- A compact, topological group `G` with a natural action on `F.obj X` for each `X : C`
 is a fundamental group of `F`, if `G` acts transitively on the fibers of Galois objects,
-the action on `F.obj X` is continuous for all `X : C` and the only trivally acting element of `G`
+the action on `F.obj X` is continuous for all `X : C` and the only trivially acting element of `G`
 is the identity. -/
 class IsFundamentalGroup [TopologicalSpace G] [TopologicalGroup G] [CompactSpace G]
     extends IsNaturalSMul F G : Prop where

Mathlib/MeasureTheory/Measure/SeparableMeasure.lean

@@ -425,7 +425,7 @@ instance Lp.SecondCountableTopology [IsSeparable μ] [TopologicalSpace.Separable
   refine ⟨D, ?_, ?_⟩
   · -- Countability directly follows from countability of `u` and `𝒜₀`. The function `f` below
     -- is the uncurryfied version of `key`, which is easier to manipulate as countability of the
-    -- domain is automatically infered.
+    -- domain is automatically inferred.
     let f (nds : Σ n : ℕ, (Fin n → u) × (Fin n → 𝒜₀)) : Lp E p μ := key nds.1 nds.2.1 nds.2.2
     have := count_𝒜₀.to_subtype
     have := countable_u.to_subtype

Mathlib/NumberTheory/JacobiSum/Basic.lean

@@ -269,7 +269,7 @@ lemma MulChar.exists_apply_sub_one_mul_apply_sub_one {n : ℕ} (hn : n ≠ 0) {
 /-- If `χ` and `ψ` are multiplicative characters of order dividing `n` on a finite field `F`
 with values in an integral domain `R` and `μ` is a primitive `n`th root of unity in `R`,
 then `J(χ,ψ) = -1 + z*(μ - 1)^2` for some `z ∈ ℤ[μ] ⊆ R`. (We assume that `#F ≡ 1 mod n`.)
-Note that we do not state this as a divisbility in `R`, as this would give a weaker statement. -/
+Note that we do not state this as a divisibility in `R`, as this would give a weaker statement. -/
 lemma exists_jacobiSum_eq_neg_one_add [DecidableEq F] {n : ℕ} (hn : 2 < n) {χ ψ : MulChar F R}
     {μ : R} (hχ : χ ^ n = 1) (hψ : ψ ^ n = 1) (hn' : n ∣ Fintype.card F - 1)
     (hμ : IsPrimitiveRoot μ n) :

Mathlib/RingTheory/Valuation/ValExtension.lean

@@ -53,7 +53,7 @@ variable {R A ΓR ΓA : Type*} [CommRing R] [Ring A]
 
 /--
 The class `IsValExtension R A` states that the valuation of `A` is an extension of the valuation
-on `R`. More precisely, the valuation on `R` is equivlent to the comap of the valuation on `A`.
+on `R`. More precisely, the valuation on `R` is equivalent to the comap of the valuation on `A`.
 -/
 class IsValExtension : Prop where
   /-- The valuation on `R` is equivalent to the comap of the valuation on `A` -/

Mathlib/Tactic/Module.lean

@@ -483,7 +483,7 @@ partial def reduceCoefficientwise {R : Q(Type u)} {_ : Q(AddCommMonoid $M)} {_ :
     let pf : Q(NF.eval $(l₁.toNF) = NF.eval $(l₁.toNF)) := q(rfl)
     pure ([], pf)
   /- if one of the lists is empty and the other one is not, recurse down the nonempty one,
-    forming goals that each of the listed coefficents is equal to zero -/
+    forming goals that each of the listed coefficients is equal to zero -/
   | [], ((a, x), _) ::ᵣ L =>
     let mvar : Q((0:$R) = $a) ← mkFreshExprMVar q((0:$R) = $a)
     let (mvars, pf) ← reduceCoefficientwise iRM [] L
@@ -562,7 +562,7 @@ def algebraMapThms : Array Name := #[``eq_natCast, ``eq_intCast, ``eq_ratCast]
 /-- Postprocessing for the scalar goals constructed in the `match_scalars` and `module` tactics.
 These goals feature a proliferation of `algebraMap` operations (because the scalars start in `ℕ` and
 get successively bumped up by `algebraMap`s as new semirings are encountered), so we reinterpret the
-most commonly occuring `algebraMap`s (those out of `ℕ`, `ℤ` and `ℚ`) into their standard forms (`ℕ`,
+most commonly occurring `algebraMap`s (those out of `ℕ`, `ℤ` and `ℚ`) into their standard forms (`ℕ`,
 `ℤ` and `ℚ` casts) and then try to disperse the casts using the various `push_cast` lemmas. -/
 def postprocess (mvarId : MVarId) : MetaM MVarId := do
   -- collect the available `push_cast` lemmas

scripts/autolabel.lean

@@ -24,7 +24,7 @@ needs to be updated here if necessary:
 ## lake exe autolabel
 
 `lake exe autolabel` uses `git diff --name-only origin/master...HEAD` to determine which
-files have been modifed and then finds all labels which should be added based on these changes.
+files have been modified and then finds all labels which should be added based on these changes.
 These are printed for testing purposes.
 
 `lake exe autolabel [NUMBER]` will further try to add the applicable labels

scripts/create-adaptation-pr.sh

@@ -292,7 +292,7 @@ if git diff --name-only --diff-filter=U | grep -q . || ! git diff-index --quiet
   if [ "$AUTO" = "yes" ]; then
     echo "Auto mode enabled. Bailing out due to unresolved conflicts or uncommitted changes."
     echo "PR has been created, and message posted to Zulip."
-    echo "Error occured while merging the new branch into 'nightly-testing'."
+    echo "Error occurred while merging the new branch into 'nightly-testing'."
     exit 2
   fi
 fi