diff --git a/HepLean/AnomalyCancellation/Basic.lean b/HepLean/AnomalyCancellation/Basic.lean
index 382bcb73..651118c2 100644
--- a/HepLean/AnomalyCancellation/Basic.lean
+++ b/HepLean/AnomalyCancellation/Basic.lean
@@ -77,7 +77,7 @@ namespace ACCSystemLinear
 structure LinSols (χ : ACCSystemLinear) where
   /-- The underlying charge. -/
   val : χ.1.charges
-  /-- The condition that the charge satifies the linear ACCs. -/
+  /-- The condition that the charge satisfies the linear ACCs. -/
   linearSol : ∀ i : Fin χ.numberLinear, χ.linearACCs i val = 0
 
 /-- Two solutions are equal if the underlying charges are equal. -/
@@ -172,7 +172,7 @@ namespace ACCSystemQuad
 
 /-- The type of solutions to the linear and quadratic ACCs. -/
 structure QuadSols (χ : ACCSystemQuad) extends χ.LinSols where
-  /-- The condition that the charge satifies the quadratic ACCs. -/
+  /-- The condition that the charge satisfies the quadratic ACCs. -/
   quadSol : ∀ i : Fin χ.numberQuadratic, (χ.quadraticACCs i) val = 0
 
 /-- Two `QuadSols` are equal if the underlying charges are equal. -/
@@ -225,7 +225,7 @@ namespace ACCSystem
 
 /-- The type of solutions to the anomaly cancellation conditions. -/
 structure Sols (χ : ACCSystem) extends χ.QuadSols where
-  /-- The condition that the charge satifies the cubic ACC. -/
+  /-- The condition that the charge satisfies the cubic ACC. -/
   cubicSol : χ.cubicACC val = 0
 
 /-- Two solutions are equal if the underlying charges are equal. -/
diff --git a/HepLean/AnomalyCancellation/MSSMNu/Basic.lean b/HepLean/AnomalyCancellation/MSSMNu/Basic.lean
index 839e1d9e..1b8ce7ce 100644
--- a/HepLean/AnomalyCancellation/MSSMNu/Basic.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/Basic.lean
@@ -206,7 +206,7 @@ lemma accSU2_ext {S T : MSSMCharges.charges}
   rw [hd, hu]
   rfl
 
-/-- The anomaly cancelation condition for SU(3) anomaly. -/
+/-- The anomaly cancellation condition for SU(3) anomaly. -/
 @[simp]
 def accSU3 : MSSMCharges.charges →ₗ[ℚ] ℚ where
   toFun S := ∑ i, (2 * (Q S i) + (U S i) + (D S i))
diff --git a/HepLean/AnomalyCancellation/MSSMNu/HyperCharge.lean b/HepLean/AnomalyCancellation/MSSMNu/HyperCharge.lean
index 8af33deb..23268af1 100644
--- a/HepLean/AnomalyCancellation/MSSMNu/HyperCharge.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/HyperCharge.lean
@@ -8,7 +8,7 @@ import Mathlib.Tactic.Polyrith
 /-!
 # Hypercharge in MSSM.
 
-Relavent definitions for the MSSM hypercharge.
+Relevant definitions for the MSSM hypercharge.
 
 -/
 
diff --git a/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean b/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean
index 834dc5b0..db47ec05 100644
--- a/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean
@@ -67,7 +67,7 @@ lemma line_in_cubic_P_P_P! {S : (PureU1 (2 * n.succ)).LinSols} (h : lineInCubic
   linear_combination 2 / 3 * (lineInCubic_expand h g f hS 1 1) -
    (lineInCubic_expand h g f hS 1 2) / 6
 
-/-- We say a `LinSol` satifies  `lineInCubicPerm` if all its permutations satsify `lineInCubic`. -/
+/-- We say a `LinSol` satisfies  `lineInCubicPerm` if all its permutations satisfy `lineInCubic`. -/
 def lineInCubicPerm (S : (PureU1 (2 * n.succ)).LinSols) : Prop :=
   ∀ (M : (FamilyPermutations (2 * n.succ)).group ),
   lineInCubic ((FamilyPermutations (2 * n.succ)).linSolRep M S)
diff --git a/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean b/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean
index 3d878778..8ea80f4f 100644
--- a/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean
+++ b/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean
@@ -12,7 +12,7 @@ import Mathlib.RepresentationTheory.Basic
 /-!
 # Line in plane condition
 
-We say a `LinSol` satifies the `line in plane` condition if for all distinct `i1`, `i2`, `i3` in
+We say a `LinSol` satisfies the `line in plane` condition if for all distinct `i1`, `i2`, `i3` in
 `Fin n`, we have
 `S i1 = S i2`  or  `S i1 = - S i2` or  `2 S i3 + S i1 + S i2 = 0`.
 
@@ -21,7 +21,7 @@ The main reference for this material is
 
 - https://arxiv.org/pdf/1912.04804.pdf
 
-We will show that `n ≥ 4` the `line in plane` condition on solutions inplies the
+We will show that `n ≥ 4` the `line in plane` condition on solutions implies the
 `constAbs` condition.
 
 -/
diff --git a/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean b/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean
index ef0361d2..30c7570d 100644
--- a/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean
@@ -10,7 +10,7 @@ import Mathlib.Logic.Equiv.Fin
 /-!
 # Basis of `LinSols` in the odd case
 
-We give a basis of `LinSols` in the odd case. This basis has the special propoerty
+We give a basis of `LinSols` in the odd case. This basis has the special property
 that splits into two planes on which every point is a solution to the ACCs.
 -/
 universe v u
diff --git a/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean b/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean
index d7a90005..d5153b5a 100644
--- a/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean
@@ -16,10 +16,10 @@ import Mathlib.RepresentationTheory.Basic
 # Line In Cubic Odd case
 
 We say that a linear solution satisfies the `lineInCubic` property
-if the line through that point and through the two different planes formed by the baisis of
+if the line through that point and through the two different planes formed by the basis of
 `LinSols` lies in the cubic.
 
-We show that for a solution all its permutations satsfiy this property,
+We show that for a solution all its permutations satisfy this property,
 then the charge must be zero.
 
 The main reference for this file is:
@@ -34,7 +34,7 @@ open BigOperators
 variable {n : ℕ}
 open VectorLikeOddPlane
 
-/-- A  property on `LinSols`, statified if every point on the line between the two planes
+/-- A  property on `LinSols`, satisfied if every point on the line between the two planes
 in the basis through that point is in the cubic. -/
 def lineInCubic (S : (PureU1 (2 * n + 1)).LinSols) : Prop :=
   ∀ (g f : Fin n → ℚ)  (_ : S.val = Pa g f) (a b : ℚ) ,
@@ -64,7 +64,7 @@ lemma line_in_cubic_P_P_P! {S : (PureU1 (2 * n + 1)).LinSols} (h : lineInCubic S
 
 
 
-/-- We say a `LinSol` satifies  `lineInCubicPerm` if all its permutations satsify `lineInCubic`. -/
+/-- We say a `LinSol` satisfies  `lineInCubicPerm` if all its permutations satisfy `lineInCubic`. -/
 def lineInCubicPerm (S : (PureU1 (2 * n + 1)).LinSols) : Prop :=
   ∀ (M : (FamilyPermutations (2 * n + 1)).group ),
     lineInCubic ((FamilyPermutations (2 * n + 1)).linSolRep M S)
diff --git a/HepLean/AnomalyCancellation/SM/Basic.lean b/HepLean/AnomalyCancellation/SM/Basic.lean
index cd712307..5f68cc64 100644
--- a/HepLean/AnomalyCancellation/SM/Basic.lean
+++ b/HepLean/AnomalyCancellation/SM/Basic.lean
@@ -13,7 +13,7 @@ import Mathlib.Logic.Equiv.Fin
 /-!
 # Anomaly cancellation conditions for n family SM.
 
-We define the ACC system for the Standard Model with`n`-famlies and no RHN.
+We define the ACC system for the Standard Model with`n`-families and no RHN.
 
 -/
 
@@ -21,7 +21,7 @@ universe v u
 open Nat
 open BigOperators
 
-/-- Aassociate to each (including RHN) SM fermion a set of charges-/
+/-- Associate to each (including RHN) SM fermion a set of charges-/
 @[simps!]
 def SMCharges (n : ℕ) : ACCSystemCharges := ACCSystemChargesMk (5 * n)
 
diff --git a/HepLean/AnomalyCancellation/SM/FamilyMaps.lean b/HepLean/AnomalyCancellation/SM/FamilyMaps.lean
index 2dc75d68..37c5bae0 100644
--- a/HepLean/AnomalyCancellation/SM/FamilyMaps.lean
+++ b/HepLean/AnomalyCancellation/SM/FamilyMaps.lean
@@ -7,7 +7,7 @@ import HepLean.AnomalyCancellation.SM.Basic
 /-!
 # Family maps for the Standard Model ACCs
 
-We define the a series of maps between the charges for different numbers of famlies.
+We define the a series of maps between the charges for different numbers of families.
 
 -/
 
@@ -84,7 +84,7 @@ other charges zero.  -/
 def familyEmbedding (m n : ℕ) : (SMCharges m).charges →ₗ[ℚ] (SMCharges n).charges :=
   chargesMapOfSpeciesMap (speciesEmbed m n)
 
-/-- For species, the embeddding of the `1`-family charges into the `n`-family charges in
+/-- For species, the embedding of the `1`-family charges into the `n`-family charges in
 a universal manor. -/
 @[simps!]
 def speciesFamilyUniversial (n : ℕ) :
@@ -98,7 +98,7 @@ def speciesFamilyUniversial (n : ℕ) :
     simp [HSMul.hSMul]
     --rw [show Rat.cast a = a from rfl]
 
-/-- The embeddding of the `1`-family charges into the `n`-family charges in
+/-- The embedding of the `1`-family charges into the `n`-family charges in
 a universal manor. -/
 def familyUniversal ( n : ℕ) : (SMCharges 1).charges →ₗ[ℚ] (SMCharges n).charges :=
   chargesMapOfSpeciesMap (speciesFamilyUniversial n)
diff --git a/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean b/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean
index e24ce3a1..6288867a 100644
--- a/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean
+++ b/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean
@@ -12,7 +12,7 @@ import HepLean.AnomalyCancellation.SM.NoGrav.One.LinearParameterization
 The main result of this file is the conclusion of this paper:
 https://arxiv.org/abs/1907.00514
 
-That eveery solution to the ACCs without gravity satifies for free the gravitational anomaly.
+That eveery solution to the ACCs without gravity satisfies for free the gravitational anomaly.
 -/
 
 universe v u
@@ -67,7 +67,7 @@ lemma accGrav_Q_neq_zero {S : (SMNoGrav 1).Sols} (hQ : Q S.val (0 : Fin 1) ≠ 0
   rw [← hS']
   exact S'.grav_of_cubic hC FLTThree
 
-/-- Any solution to the ACCs without gravity satifies the gravitational ACC.  -/
+/-- Any solution to the ACCs without gravity satisfies the gravitational ACC.  -/
 theorem accGravSatisfied {S : (SMNoGrav 1).Sols} (FLTThree : FermatLastTheoremWith ℚ 3) :
     accGrav S.val = 0 := by
   by_cases hQ : Q S.val (0 : Fin 1)= 0
diff --git a/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean b/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean
index 8ffd5e85..1c11dcaa 100644
--- a/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean
+++ b/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean
@@ -7,7 +7,7 @@ import HepLean.AnomalyCancellation.SMNu.Basic
 /-!
 # Family maps for the Standard Model  for RHN ACCs
 
-We define the a series of maps between the charges for different numbers of famlies.
+We define the a series of maps between the charges for different numbers of families.
 
 -/
 
@@ -89,7 +89,7 @@ other charges zero.  -/
 def familyEmbedding (m n : ℕ) : (SMνCharges m).charges →ₗ[ℚ] (SMνCharges n).charges :=
   chargesMapOfSpeciesMap (speciesEmbed m n)
 
-/-- For species, the embeddding of the `1`-family charges into the `n`-family charges in
+/-- For species, the embedding of the `1`-family charges into the `n`-family charges in
 a universal manor. -/
 @[simps!]
 def speciesFamilyUniversial (n : ℕ) :
@@ -103,7 +103,7 @@ def speciesFamilyUniversial (n : ℕ) :
     simp [HSMul.hSMul]
     -- rw [show Rat.cast a = a from rfl]
 
-/-- The embeddding of the `1`-family charges into the `n`-family charges in
+/-- The embedding of the `1`-family charges into the `n`-family charges in
 a universal manor. -/
 def familyUniversal (n : ℕ) : (SMνCharges 1).charges →ₗ[ℚ] (SMνCharges n).charges :=
   chargesMapOfSpeciesMap (speciesFamilyUniversial n)
diff --git a/HepLean/FlavorPhysics/CKMMatrix/Basic.lean b/HepLean/FlavorPhysics/CKMMatrix/Basic.lean
index 36cba929..611612e9 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/Basic.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/Basic.lean
@@ -9,7 +9,7 @@ import Mathlib.Tactic.Polyrith
 /-!
 # The CKM Matrix
 
-The definition of the type of CKM matries as unitary $3×3$-matries.
+The definition of the type of CKM matrices as unitary $3×3$-matrices.
 
 An equivalence relation on CKM matrices is defined, where two matrices are equivalent if they are
 related by phase shifts.