diff --git a/Mathlib/Algebra/Group/Defs.lean b/Mathlib/Algebra/Group/Defs.lean
index 21534c8fd115f..330098f8d05fa 100644
--- a/Mathlib/Algebra/Group/Defs.lean
+++ b/Mathlib/Algebra/Group/Defs.lean
@@ -113,7 +113,7 @@ variable [Ring R] [AddCommMonoid M] [Module R M] (r : R) (N : Submodule R M) (m
 ```
 Without the macro, the expression would elaborate as `m + ↑(r • n : ↑N) : M`.
 With the macro, the expression elaborates as `m + r • (↑n : M) : M`.
-To get the first intepretation, one can write `m + (r • n :)`.
+To get the first interpretation, one can write `m + (r • n :)`.
 
 Here is a quick review of the expression tree elaborator:
 1. It builds up an expression tree of all the immediately accessible operations
diff --git a/Mathlib/Algebra/Group/WithOne/Basic.lean b/Mathlib/Algebra/Group/WithOne/Basic.lean
index 3f7ae36f5602a..db9f3ac68d8f4 100644
--- a/Mathlib/Algebra/Group/WithOne/Basic.lean
+++ b/Mathlib/Algebra/Group/WithOne/Basic.lean
@@ -58,8 +58,8 @@ section lift
 
 variable [Mul α] [MulOneClass β]
 
-/-- Lift a semigroup homomorphism `f` to a bundled monoid homorphism. -/
-@[to_additive "Lift an add semigroup homomorphism `f` to a bundled add monoid homorphism."]
+/-- Lift a semigroup homomorphism `f` to a bundled monoid homomorphism. -/
+@[to_additive "Lift an add semigroup homomorphism `f` to a bundled add monoid homomorphism."]
 def lift : (α →ₙ* β) ≃ (WithOne α →* β) where
   toFun f :=
     { toFun := fun x => Option.casesOn x 1 f, map_one' := rfl,
diff --git a/Mathlib/Algebra/Star/StarAlgHom.lean b/Mathlib/Algebra/Star/StarAlgHom.lean
index 0c92c3b6c592f..c537cc18c0171 100644
--- a/Mathlib/Algebra/Star/StarAlgHom.lean
+++ b/Mathlib/Algebra/Star/StarAlgHom.lean
@@ -531,7 +531,7 @@ variable (R A B C : Type*) [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulA
   [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] [NonUnitalNonAssocSemiring C]
   [DistribMulAction R C] [Star C]
 
-/-- The first projection of a product is a non-unital ⋆-algebra homomoprhism. -/
+/-- The first projection of a product is a non-unital ⋆-algebra homomorphism. -/
 @[simps!]
 def fst : A × B →⋆ₙₐ[R] A :=
   { NonUnitalAlgHom.fst R A B with map_star' := fun _ => rfl }
@@ -629,7 +629,7 @@ namespace StarAlgHom
 variable (R A B C : Type*) [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B]
   [Algebra R B] [Star B] [Semiring C] [Algebra R C] [Star C]
 
-/-- The first projection of a product is a ⋆-algebra homomoprhism. -/
+/-- The first projection of a product is a ⋆-algebra homomorphism. -/
 @[simps!]
 def fst : A × B →⋆ₐ[R] A :=
   { AlgHom.fst R A B with map_star' := fun _ => rfl }
diff --git a/Mathlib/AlgebraicTopology/DoldKan/Homotopies.lean b/Mathlib/AlgebraicTopology/DoldKan/Homotopies.lean
index 028f650c93d58..d675da0cfa740 100644
--- a/Mathlib/AlgebraicTopology/DoldKan/Homotopies.lean
+++ b/Mathlib/AlgebraicTopology/DoldKan/Homotopies.lean
@@ -53,7 +53,7 @@ compatible the application of additive functors (see `map_Hσ`).
 
 ## References
 * [Albrecht Dold, *Homology of Symmetric Products and Other Functors of Complexes*][dold1958]
-* [Paul G. Goerss, John F. Jardine, *Simplical Homotopy Theory*][goerss-jardine-2009]
+* [Paul G. Goerss, John F. Jardine, *Simplicial Homotopy Theory*][goerss-jardine-2009]
 
 -/
 
diff --git a/Mathlib/AlgebraicTopology/ExtraDegeneracy.lean b/Mathlib/AlgebraicTopology/ExtraDegeneracy.lean
index d61c3bd48f37b..cd3bb8133a51d 100644
--- a/Mathlib/AlgebraicTopology/ExtraDegeneracy.lean
+++ b/Mathlib/AlgebraicTopology/ExtraDegeneracy.lean
@@ -40,7 +40,7 @@ the augmentation on the alternating face map complex of `X` is a homotopy
 equivalence.
 
 ## References
-* [Paul G. Goerss, John F. Jardine, *Simplical Homotopy Theory*][goerss-jardine-2009]
+* [Paul G. Goerss, John F. Jardine, *Simplicial Homotopy Theory*][goerss-jardine-2009]
 
 -/
 
@@ -78,7 +78,7 @@ attribute [reassoc (attr := simp)] s'_comp_ε s_comp_δ₀
 
 /-- If `ed` is an extra degeneracy for `X : SimplicialObject.Augmented C` and
 `F : C ⥤ D` is a functor, then `ed.map F` is an extra degeneracy for the
-augmented simplical object in `D` obtained by applying `F` to `X`. -/
+augmented simplicial object in `D` obtained by applying `F` to `X`. -/
 def map {D : Type*} [Category D] {X : SimplicialObject.Augmented C} (ed : ExtraDegeneracy X)
     (F : C ⥤ D) : ExtraDegeneracy (((whiskering _ _).obj F).obj X) where
   s' := F.map ed.s'
diff --git a/Mathlib/AlgebraicTopology/Nerve.lean b/Mathlib/AlgebraicTopology/Nerve.lean
index 537cb6c7e41ab..d284f58aab70b 100644
--- a/Mathlib/AlgebraicTopology/Nerve.lean
+++ b/Mathlib/AlgebraicTopology/Nerve.lean
@@ -18,7 +18,7 @@ By definition, the type of `n`-simplices of `nerve C` is `ComposableArrows C n`,
 which is the category `Fin (n + 1) ⥤ C`.
 
 ## References
-* [Paul G. Goerss, John F. Jardine, *Simplical Homotopy Theory*][goerss-jardine-2009]
+* [Paul G. Goerss, John F. Jardine, *Simplicial Homotopy Theory*][goerss-jardine-2009]
 
 -/
 
diff --git a/Mathlib/AlgebraicTopology/SimplexCategory.lean b/Mathlib/AlgebraicTopology/SimplexCategory.lean
index 1aef771a54ef3..76081e6d63044 100644
--- a/Mathlib/AlgebraicTopology/SimplexCategory.lean
+++ b/Mathlib/AlgebraicTopology/SimplexCategory.lean
@@ -97,7 +97,7 @@ protected def Hom (a b : SimplexCategory) :=
 
 namespace Hom
 
-/-- Make a moprhism in `SimplexCategory` from a monotone map of `Fin`'s. -/
+/-- Make a morphism in `SimplexCategory` from a monotone map of `Fin`'s. -/
 def mk {a b : SimplexCategory} (f : Fin (a.len + 1) →o Fin (b.len + 1)) : SimplexCategory.Hom a b :=
   f
 #align simplex_category.hom.mk SimplexCategory.Hom.mk
diff --git a/Mathlib/AlgebraicTopology/SplitSimplicialObject.lean b/Mathlib/AlgebraicTopology/SplitSimplicialObject.lean
index 3c37f676ffcb3..c00555412f750 100644
--- a/Mathlib/AlgebraicTopology/SplitSimplicialObject.lean
+++ b/Mathlib/AlgebraicTopology/SplitSimplicialObject.lean
@@ -14,7 +14,7 @@ import Mathlib.CategoryTheory.Limits.Shapes.Products
 
 In this file, we introduce the notion of split simplicial object.
 If `C` is a category that has finite coproducts, a splitting
-`s : Splitting X` of a simplical object `X` in `C` consists
+`s : Splitting X` of a simplicial object `X` in `C` consists
 of the datum of a sequence of objects `s.N : ℕ → C` (which
 we shall refer to as "nondegenerate simplices") and a
 sequence of morphisms `s.ι n : s.N n → X _[n]` that have
@@ -341,7 +341,7 @@ def mk' {X : SimplicialObject C} (s : Splitting X) : Split C :=
 /-- Morphisms in `SimplicialObject.Split C` are morphisms of simplicial objects that
 are compatible with the splittings. -/
 structure Hom (S₁ S₂ : Split C) where
-  /-- the morphism between the underlying simplical objects -/
+  /-- the morphism between the underlying simplicial objects -/
   F : S₁.X ⟶ S₂.X
   /-- the morphism between the "nondegenerate" `n`-simplices for all `n : ℕ` -/
   f : ∀ n : ℕ, S₁.s.N n ⟶ S₂.s.N n
diff --git a/Mathlib/Analysis/Convolution.lean b/Mathlib/Analysis/Convolution.lean
index 8dc0cece4f998..13ca46eaf22b2 100644
--- a/Mathlib/Analysis/Convolution.lean
+++ b/Mathlib/Analysis/Convolution.lean
@@ -27,7 +27,7 @@ For many applications we can take `L = ContinuousLinearMap.lsmul ℝ ℝ` or
 
 We also define `ConvolutionExists` and `ConvolutionExistsAt` to state that the convolution is
 well-defined (everywhere or at a single point). These conditions are needed for pointwise
-computations (e.g. `ConvolutionExistsAt.distrib_add`), but are generally not stong enough for any
+computations (e.g. `ConvolutionExistsAt.distrib_add`), but are generally not strong enough for any
 local (or global) properties of the convolution. For this we need stronger assumptions on `f`
 and/or `g`, and generally if we impose stronger conditions on one of the functions, we can impose
 weaker conditions on the other.
diff --git a/Mathlib/CategoryTheory/Abelian/Homology.lean b/Mathlib/CategoryTheory/Abelian/Homology.lean
index 7a24eae161591..7ed7b9483ec72 100644
--- a/Mathlib/CategoryTheory/Abelian/Homology.lean
+++ b/Mathlib/CategoryTheory/Abelian/Homology.lean
@@ -129,7 +129,7 @@ def desc' {W : A} (e : kernel g ⟶ W) (he : kernel.lift g f w ≫ e = 0) : homo
   (homology'IsoCokernelLift _ _ _).hom ≫ cokernel.desc _ e he
 #align homology.desc' homology'.desc'
 
-/-- Obtain a moprhism to the homology, given a morphism to the kernel. -/
+/-- Obtain a morphism to the homology, given a morphism to the kernel. -/
 def lift {W : A} (e : W ⟶ cokernel f) (he : e ≫ cokernel.desc f g w = 0) : W ⟶ homology' f g w :=
   kernel.lift _ e he ≫ (homology'IsoKernelDesc _ _ _).inv
 #align homology.lift homology'.lift
diff --git a/Mathlib/CategoryTheory/Sites/Grothendieck.lean b/Mathlib/CategoryTheory/Sites/Grothendieck.lean
index ad483f36f4d3d..515f5768223d9 100644
--- a/Mathlib/CategoryTheory/Sites/Grothendieck.lean
+++ b/Mathlib/CategoryTheory/Sites/Grothendieck.lean
@@ -606,7 +606,7 @@ def bind {X : C} (S : J.Cover X) (T : ∀ I : S.Arrow, J.Cover I.Y) : J.Cover X
     J.bind_covering S.condition fun _ _ _ => (T _).condition⟩
 #align category_theory.grothendieck_topology.cover.bind CategoryTheory.GrothendieckTopology.Cover.bind
 
-/-- The canonical moprhism from `S.bind T` to `T`. -/
+/-- The canonical morphism from `S.bind T` to `T`. -/
 def bindToBase {X : C} (S : J.Cover X) (T : ∀ I : S.Arrow, J.Cover I.Y) : S.bind T ⟶ S :=
   homOfLE <| by
     rintro Y f ⟨Z, e1, e2, h1, _, h3⟩
diff --git a/Mathlib/Data/Int/Cast/Defs.lean b/Mathlib/Data/Int/Cast/Defs.lean
index f5f84d3e6ce4e..5c4068ccca3f2 100644
--- a/Mathlib/Data/Int/Cast/Defs.lean
+++ b/Mathlib/Data/Int/Cast/Defs.lean
@@ -40,11 +40,11 @@ protected def Int.castDef {R : Type u} [NatCast R] [Neg R] : ℤ → R
 /-- An `AddGroupWithOne` is an `AddGroup` with a 1. It also contains data for the unique
 homomorphisms `ℕ → R` and `ℤ → R`. -/
 class AddGroupWithOne (R : Type u) extends IntCast R, AddMonoidWithOne R, AddGroup R where
-  /-- The canonical homorphism `ℤ → R`. -/
+  /-- The canonical homomorphism `ℤ → R`. -/
   intCast := Int.castDef
-  /-- The canonical homorphism `ℤ → R` agrees with the one from `ℕ → R` on `ℕ`. -/
+  /-- The canonical homomorphism `ℤ → R` agrees with the one from `ℕ → R` on `ℕ`. -/
   intCast_ofNat : ∀ n : ℕ, intCast (n : ℕ) = Nat.cast n := by intros; rfl
-  /-- The canonical homorphism `ℤ → R` for negative values is just the negation of the values
+  /-- The canonical homomorphism `ℤ → R` for negative values is just the negation of the values
   of the canonical homomorphism `ℕ → R`. -/
   intCast_negSucc : ∀ n : ℕ, intCast (Int.negSucc n) = - Nat.cast (n + 1) := by intros; rfl
 #align add_group_with_one AddGroupWithOne
diff --git a/Mathlib/GroupTheory/GroupAction/Opposite.lean b/Mathlib/GroupTheory/GroupAction/Opposite.lean
index 57fb6de5fc37f..45376cc60d9b2 100644
--- a/Mathlib/GroupTheory/GroupAction/Opposite.lean
+++ b/Mathlib/GroupTheory/GroupAction/Opposite.lean
@@ -83,7 +83,7 @@ end MulOpposite
 /-! ### Right actions
 
 In this section we establish `SMul αᵐᵒᵖ β` as the canonical spelling of right scalar multiplication
-of `β` by `α`, and provide convienient notations.
+of `β` by `α`, and provide convenient notations.
 -/
 
 namespace RightActions
diff --git a/Mathlib/Init/Control/Lawful.lean b/Mathlib/Init/Control/Lawful.lean
index 4d5140830be1c..0648f90d15b50 100644
--- a/Mathlib/Init/Control/Lawful.lean
+++ b/Mathlib/Init/Control/Lawful.lean
@@ -67,7 +67,7 @@ following theorem as a simp theorem.
 theorem run_fun (f : σ → m (α × σ)) (st : σ) : StateT.run (fun s => f s) st = f st :=
   rfl
 ```
-If we decleare this theorem as a simp theorem, `StateT.run f st` is simplified to `f st` by eta
+If we declare this theorem as a simp theorem, `StateT.run f st` is simplified to `f st` by eta
 reduction. This breaks the structure of `StateT`.
 So, we declare a constructor-like definition `StateT.mk` and a simp theorem for it.
 -/
@@ -155,7 +155,7 @@ following theorem as a simp theorem.
 theorem run_fun (f : σ → m α) (r : σ) : ReaderT.run (fun r' => f r') r = f r :=
   rfl
 ```
-If we decleare this theorem as a simp theorem, `ReaderT.run f st` is simplified to `f st` by eta
+If we declare this theorem as a simp theorem, `ReaderT.run f st` is simplified to `f st` by eta
 reduction. This breaks the structure of `ReaderT`.
 So, we declare a constructor-like definition `ReaderT.mk` and a simp theorem for it.
 -/
diff --git a/Mathlib/LinearAlgebra/Dimension/Basic.lean b/Mathlib/LinearAlgebra/Dimension/Basic.lean
index 45cda19b20e6d..847e4db176181 100644
--- a/Mathlib/LinearAlgebra/Dimension/Basic.lean
+++ b/Mathlib/LinearAlgebra/Dimension/Basic.lean
@@ -179,7 +179,7 @@ variable {R : Type w} {S : Type v} [CommRing R] [Ring S] [Algebra R S]
   {R' : Type w'} {S' : Type v'} [CommRing R'] [Ring S'] [Algebra R' S']
 
 /-- If `S / R` and `S' / R'` are algebras, `i : R' →+* R` and `j : S →+* S'` are injective ring
-homorphisms, such that `R' → R → S → S'` and `R' → S'` commute, then the rank of `S / R` is
+homomorphisms, such that `R' → R → S → S'` and `R' → S'` commute, then the rank of `S / R` is
 smaller than or equal to the rank of `S' / R'`. -/
 theorem lift_rank_le_of_injective_injective
     (i : R' →+* R) (j : S →+* S') (hi : Injective i) (hj : Injective j)
@@ -192,7 +192,7 @@ theorem lift_rank_le_of_injective_injective
   simp_rw [smul_def, AddMonoidHom.coe_coe, map_mul, this]
 
 /-- If `S / R` and `S' / R'` are algebras, `i : R →+* R'` is a surjective ring homomorphism,
-`j : S →+* S'` is an injective ring homorphism, such that `R → R' → S'` and `R → S → S'` commute,
+`j : S →+* S'` is an injective ring homomorphism, such that `R → R' → S'` and `R → S → S'` commute,
 then the rank of `S / R` is smaller than or equal to the rank of `S' / R'`. -/
 theorem lift_rank_le_of_surjective_injective
     (i : R →+* R') (j : S →+* S') (hi : Surjective i) (hj : Injective j)
diff --git a/Mathlib/ModelTheory/ElementarySubstructures.lean b/Mathlib/ModelTheory/ElementarySubstructures.lean
index 463cba9173e7d..0fb97f07ad355 100644
--- a/Mathlib/ModelTheory/ElementarySubstructures.lean
+++ b/Mathlib/ModelTheory/ElementarySubstructures.lean
@@ -31,7 +31,7 @@ variable {L : Language} {M : Type*} {N : Type*} {P : Type*} {Q : Type*}
 
 variable [L.Structure M] [L.Structure N] [L.Structure P] [L.Structure Q]
 
-/-- A substructure is elementary when every formula applied to a tuple in the subtructure
+/-- A substructure is elementary when every formula applied to a tuple in the substructure
   agrees with its value in the overall structure. -/
 def Substructure.IsElementary (S : L.Substructure M) : Prop :=
   ∀ ⦃n⦄ (φ : L.Formula (Fin n)) (x : Fin n → S), φ.Realize (((↑) : _ → M) ∘ x) ↔ φ.Realize x
@@ -39,7 +39,7 @@ def Substructure.IsElementary (S : L.Substructure M) : Prop :=
 
 variable (L M)
 
-/-- An elementary substructure is one in which every formula applied to a tuple in the subtructure
+/-- An elementary substructure is one in which every formula applied to a tuple in the substructure
   agrees with its value in the overall structure. -/
 structure ElementarySubstructure where
   toSubstructure : L.Substructure M
diff --git a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean
index d6a73b652fb79..9dc54d24fd202 100644
--- a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean
+++ b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean
@@ -22,7 +22,7 @@ into the type `(K →+* ℂ) → ℂ` of `ℂ`-vectors indexed by the complex em
 
 ## Main definitions and results
 
-* `NumberField.canonicalEmbedding`: the ring homorphism `K →+* ((K →+* ℂ) → ℂ)` defined by
+* `NumberField.canonicalEmbedding`: the ring homomorphism `K →+* ((K →+* ℂ) → ℂ)` defined by
 sending `x : K` to the vector `(φ x)` indexed by `φ : K →+* ℂ`.
 
 * `NumberField.canonicalEmbedding.integerLattice.inter_ball_finite`: the intersection of the
diff --git a/Mathlib/RingTheory/IsTensorProduct.lean b/Mathlib/RingTheory/IsTensorProduct.lean
index d6b28c61ffa26..393ea32410ced 100644
--- a/Mathlib/RingTheory/IsTensorProduct.lean
+++ b/Mathlib/RingTheory/IsTensorProduct.lean
@@ -429,7 +429,7 @@ instance TensorProduct.isPushout' {R S T : Type*} [CommRing R] [CommRing S] [Com
 #align tensor_product.is_pushout' TensorProduct.isPushout'
 
 /-- If `S' = S ⊗[R] R'`, then any pair of `R`-algebra homomorphisms `f : S → A` and `g : R' → A`
-such that `f x` and `g y` commutes for all `x, y` descends to a (unique) homomoprhism `S' → A`.
+such that `f x` and `g y` commutes for all `x, y` descends to a (unique) homomorphism `S' → A`.
 -/
 --@[simps (config := .lemmasOnly) apply] --Porting note: removed and added by hand
 noncomputable def Algebra.pushoutDesc [H : Algebra.IsPushout R S R' S'] {A : Type*} [Semiring A]