diff --git a/HepLean/AnomalyCancellation/PureU1/Basic.lean b/HepLean/AnomalyCancellation/PureU1/Basic.lean
index d506c0a..6b17491 100644
--- a/HepLean/AnomalyCancellation/PureU1/Basic.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Basic.lean
@@ -124,7 +124,7 @@ lemma pureU1_last {n : ℕ} (S : (PureU1 n.succ).LinSols) :
   rw [Fin.sum_univ_castSucc] at hS
   linear_combination hS
 
-/-- Two solutions to the Linear ACCs for `n.succ` areq equal if their first `n` charges are
+/-- Two solutions to the Linear ACCs for `n.succ` are equal if their first `n` charges are
   equal. -/
 lemma pureU1_anomalyFree_ext {n : ℕ} {S T : (PureU1 n.succ).LinSols}
     (h : ∀ (i : Fin n), S.val i.castSucc = T.val i.castSucc) : S = T := by
diff --git a/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean b/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
index 86594c4..83b5f03 100644
--- a/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
+++ b/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
@@ -61,7 +61,7 @@ lemma speciesVal (S : linearParameters) :
   | 3 => rfl
   | 4 => rfl
 
-/-- The map from the linear paramaters to elements of `(SMNoGrav 1).LinSols`. -/
+/-- The map from the linear parameters to elements of `(SMNoGrav 1).LinSols`. -/
 def asLinear (S : linearParameters) : (SMNoGrav 1).LinSols :=
   chargeToLinear S.asCharges (by
     simp only [accSU2, SMSpecies_numberCharges, Finset.univ_unique, Fin.default_eq_zero,
diff --git a/HepLean/BeyondTheStandardModel/TwoHDM/GaugeOrbits.lean b/HepLean/BeyondTheStandardModel/TwoHDM/GaugeOrbits.lean
index aff69e8..23ed567 100644
--- a/HepLean/BeyondTheStandardModel/TwoHDM/GaugeOrbits.lean
+++ b/HepLean/BeyondTheStandardModel/TwoHDM/GaugeOrbits.lean
@@ -84,8 +84,8 @@ lemma prodMatrix_smooth (Φ1 Φ2 : HiggsField) :
     simpa only [prodMatrix, Fin.zero_eta, Fin.isValue, of_apply, cons_val', cons_val_zero,
       empty_val', cons_val_fin_one] using smooth_innerProd _ _
 
-/-- The map `prodMatrix` is invariant under the simultanous action of `gaugeAction` on the two Higgs
-fields. -/
+/-- The map `prodMatrix` is invariant under the simultaneous action of `gaugeAction` on the two
+Higgs fields. -/
 informal_lemma prodMatrix_invariant where
   deps := [``prodMatrix, ``gaugeAction]
 
diff --git a/HepLean/FlavorPhysics/CKMMatrix/Basic.lean b/HepLean/FlavorPhysics/CKMMatrix/Basic.lean
index a3c1901..23df8bc 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/Basic.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/Basic.lean
@@ -422,7 +422,7 @@ def Rcscb (V : CKMMatrix) : ℂ := [V]cs / [V]cb
 /-- The ratio of the `cs` and `cb` elements of a CKM matrix. -/
 scoped[CKMMatrix] notation (name := cs_cb_ratio) "[" V "]cs|cb" => Rcscb V
 
-/-- Multiplicying the ratio of the `cs` by `cb` element of a CKM matrix by the `cb` element
+/-- Multiplying the ratio of the `cs` by `cb` element of a CKM matrix by the `cb` element
   returns the `cs` element, as long as the `cb` element is non-zero. -/
 lemma Rcscb_mul_cb {V : CKMMatrix} (h : [V]cb ≠ 0) : [V]cs = Rcscb V * [V]cb := by
   rw [Rcscb]
diff --git a/HepLean/FlavorPhysics/CKMMatrix/Invariants.lean b/HepLean/FlavorPhysics/CKMMatrix/Invariants.lean
index b106c5f..a590645 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/Invariants.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/Invariants.lean
@@ -50,8 +50,8 @@ lemma jarlskogℂCKM_equiv (V U : CKMMatrix) (h : V ≈ U) :
 def jarlskogℂ : Quotient CKMMatrixSetoid → ℂ :=
   Quotient.lift jarlskogℂCKM jarlskogℂCKM_equiv
 
-/-- An invariant for CKM mtrices corresponding to the square of the absolute values
-  of the `us`, `ub` and `cb` elements multipled together divided by `(VudAbs V ^ 2 + VusAbs V ^2)`.
+/-- An invariant for CKM matrices corresponding to the square of the absolute values
+  of the `us`, `ub` and `cb` elements multiplied together divided by `(VudAbs V ^ 2 + VusAbs V ^2)`.
 -/
 def VusVubVcdSq (V : Quotient CKMMatrixSetoid) : ℝ :=
     VusAbs V ^ 2 * VubAbs V ^ 2 * VcbAbs V ^2 / (VudAbs V ^ 2 + VusAbs V ^2)
diff --git a/HepLean/FlavorPhysics/CKMMatrix/Relations.lean b/HepLean/FlavorPhysics/CKMMatrix/Relations.lean
index b254b56..480dae4 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/Relations.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/Relations.lean
@@ -44,7 +44,7 @@ lemma fst_row_normalized_abs (V : CKMMatrix) : abs [V]ud ^ 2 + abs [V]us ^ 2 + a
 lemma snd_row_normalized_abs (V : CKMMatrix) : abs [V]cd ^ 2 + abs [V]cs ^ 2 + abs [V]cb ^ 2 = 1 :=
   VAbs_sum_sq_row_eq_one ⟦V⟧ 1
 
-/-- The absolute value squared of the thid rwo of a CKM matrix is `1`, in terms of `abs`. -/
+/-- The absolute value squared of the third rwo of a CKM matrix is `1`, in terms of `abs`. -/
 lemma thd_row_normalized_abs (V : CKMMatrix) : abs [V]td ^ 2 + abs [V]ts ^ 2 + abs [V]tb ^ 2 = 1 :=
   VAbs_sum_sq_row_eq_one ⟦V⟧ 2
 
diff --git a/HepLean/Lorentz/ComplexTensor/PauliMatrices/Basic.lean b/HepLean/Lorentz/ComplexTensor/PauliMatrices/Basic.lean
index 089169a..be90483 100644
--- a/HepLean/Lorentz/ComplexTensor/PauliMatrices/Basic.lean
+++ b/HepLean/Lorentz/ComplexTensor/PauliMatrices/Basic.lean
@@ -79,7 +79,7 @@ lemma tensorNode_pauliContrDown : {pauliContrDown | μ α β}ᵀ.tensor =
 -/
 
 set_option maxRecDepth 5000 in
-/-- A rearanging of `pauliCoDown` to place the pauli matrices on the right. -/
+/-- A rearranging of `pauliCoDown` to place the pauli matrices on the right. -/
 lemma pauliCoDown_eq_metric_mul_pauliCo :
     {pauliCoDown | μ α' β' = εL' | α α' ⊗ εR' | β β' ⊗ pauliCo | μ α β}ᵀ := by
   conv =>
@@ -128,7 +128,7 @@ lemma pauliCoDown_eq_metric_mul_pauliCo :
   decide
 
 set_option maxRecDepth 5000 in
-/-- A rearanging of `pauliContrDown` to place the pauli matrices on the right. -/
+/-- A rearranging of `pauliContrDown` to place the pauli matrices on the right. -/
 lemma pauliContrDown_eq_metric_mul_pauliContr :
     {pauliContrDown | μ α' β' = εL' | α α' ⊗
     εR' | β β' ⊗ pauliContr | μ α β}ᵀ := by
diff --git a/HepLean/Lorentz/ComplexVector/Unit.lean b/HepLean/Lorentz/ComplexVector/Unit.lean
index c0bec8c..6b22e57 100644
--- a/HepLean/Lorentz/ComplexVector/Unit.lean
+++ b/HepLean/Lorentz/ComplexVector/Unit.lean
@@ -38,7 +38,7 @@ lemma contrCoUnitVal_expand_tmul : contrCoUnitVal =
   rfl
 
 /-- The contra-co unit for complex lorentz vectors as a morphism
-  `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ complexCo`, manifesting the invaraince under
+  `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ complexCo`, manifesting the invariance under
   the `SL(2, ℂ)` action. -/
 def contrCoUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ complexCo where
   hom := ModuleCat.ofHom {
@@ -88,7 +88,7 @@ lemma coContrUnitVal_expand_tmul : coContrUnitVal =
   rfl
 
 /-- The co-contra unit for complex lorentz vectors as a morphism
-  `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexCo ⊗ complexContr`, manifesting the invaraince under
+  `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexCo ⊗ complexContr`, manifesting the invariance under
   the `SL(2, ℂ)` action. -/
 def coContrUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexCo ⊗ complexContr where
   hom := ModuleCat.ofHom {
diff --git a/HepLean/Lorentz/Group/Orthochronous.lean b/HepLean/Lorentz/Group/Orthochronous.lean
index 5a725fe..82dcf50 100644
--- a/HepLean/Lorentz/Group/Orthochronous.lean
+++ b/HepLean/Lorentz/Group/Orthochronous.lean
@@ -29,7 +29,7 @@ open Lorentz.Contr
 /-- A Lorentz transformation is `orthochronous` if its `0 0` element is non-negative. -/
 def IsOrthochronous : Prop := 0 ≤ Λ.1 (Sum.inl 0) (Sum.inl 0)
 
-/-- A Lorentz transformation is `orthochronous` if and only if its fist column is
+/-- A Lorentz transformation is `orthochronous` if and only if its first column is
   future pointing. -/
 lemma IsOrthochronous_iff_futurePointing :
     IsOrthochronous Λ ↔ toNormOne Λ ∈ NormOne.FuturePointing d := by
@@ -66,7 +66,7 @@ def timeCompCont : C(LorentzGroup d, ℝ) := ⟨fun Λ => Λ.1 (Sum.inl 0) (Sum.
 
 /-- An auxiliary function used in the definition of `orthchroMapReal`.
   This function takes all elements of `ℝ` less then `-1` to `-1`,
-  all elements of `R` geater then `1` to `1` and peserves all other elements. -/
+  all elements of `R` greater then `1` to `1` and preserves all other elements. -/
 def stepFunction : ℝ → ℝ := fun t =>
   if t ≤ -1 then -1 else
     if 1 ≤ t then 1 else t
@@ -152,7 +152,7 @@ lemma mul_othchron_of_not_othchron_not_othchron {Λ Λ' : LorentzGroup d} (h : 
   exact NormOne.FuturePointing.metric_reflect_not_mem_not_mem h h'
 
 /-- The product of an orthochronous Lorentz transformations with a
-  non-orthochronous Loentz transformation is not orthochronous. -/
+  non-orthochronous Lorentz transformation is not orthochronous. -/
 lemma mul_not_othchron_of_othchron_not_othchron {Λ Λ' : LorentzGroup d} (h : IsOrthochronous Λ)
     (h' : ¬ IsOrthochronous Λ') : ¬ IsOrthochronous (Λ * Λ') := by
   rw [not_orthochronous_iff_le_zero, LorentzGroup.inl_inl_mul]
@@ -161,7 +161,7 @@ lemma mul_not_othchron_of_othchron_not_othchron {Λ Λ' : LorentzGroup d} (h : I
   exact NormOne.FuturePointing.metric_reflect_mem_not_mem h h'
 
 /-- The product of a non-orthochronous Lorentz transformations with an
-  orthochronous Loentz transformation is not orthochronous. -/
+  orthochronous Lorentz transformation is not orthochronous. -/
 lemma mul_not_othchron_of_not_othchron_othchron {Λ Λ' : LorentzGroup d} (h : ¬ IsOrthochronous Λ)
     (h' : IsOrthochronous Λ') : ¬ IsOrthochronous (Λ * Λ') := by
   rw [not_orthochronous_iff_le_zero, LorentzGroup.inl_inl_mul]
diff --git a/HepLean/Lorentz/MinkowskiMatrix.lean b/HepLean/Lorentz/MinkowskiMatrix.lean
index 149d040..14f015d 100644
--- a/HepLean/Lorentz/MinkowskiMatrix.lean
+++ b/HepLean/Lorentz/MinkowskiMatrix.lean
@@ -29,7 +29,7 @@ variable {d : ℕ}
 /-- Notation for `minkowskiMatrix`. -/
 scoped[minkowskiMatrix] notation "η" => minkowskiMatrix
 
-/-- The Minkowski matrix is self-inveting. -/
+/-- The Minkowski matrix is self-inverting. -/
 @[simp]
 lemma sq : @minkowskiMatrix d * minkowskiMatrix = 1 := by
   simp only [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, diagonal_mul_diagonal]
@@ -55,8 +55,8 @@ lemma sq : @minkowskiMatrix d * minkowskiMatrix = 1 := by
 lemma eq_transpose : minkowskiMatrixᵀ = @minkowskiMatrix d := by
   simp only [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, diagonal_transpose]
 
-/-- The deteminant of the Minkowski matrix is equal to `-1` to the power
-  of the number of spactial dimensions. -/
+/-- The determinant of the Minkowski matrix is equal to `-1` to the power
+  of the number of spatial dimensions. -/
 @[simp]
 lemma det_eq_neg_one_pow_d : (@minkowskiMatrix d).det = (- 1) ^ d := by
   simp [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal]
@@ -68,7 +68,7 @@ lemma η_apply_mul_η_apply_diag (μ : Fin 1 ⊕ Fin d) : η μ μ * η μ μ =
   | Sum.inl _ => simp [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal]
   | Sum.inr _ => simp [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal]
 
-/-- The Minkowski matix as a block matrix. -/
+/-- The Minkowski matrix as a block matrix. -/
 lemma as_block : @minkowskiMatrix d =
     Matrix.fromBlocks (1 : Matrix (Fin 1) (Fin 1) ℝ) 0 0 (-1 : Matrix (Fin d) (Fin d) ℝ) := by
   rw [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, ← fromBlocks_diagonal]
diff --git a/HepLean/Lorentz/PauliMatrices/SelfAdjoint.lean b/HepLean/Lorentz/PauliMatrices/SelfAdjoint.lean
index 3fabdbd..8bb7651 100644
--- a/HepLean/Lorentz/PauliMatrices/SelfAdjoint.lean
+++ b/HepLean/Lorentz/PauliMatrices/SelfAdjoint.lean
@@ -301,7 +301,7 @@ lemma σSAL_span : ⊤ ≤ Submodule.span ℝ (Set.range σSAL') := by
 def σSAL : Basis (Fin 1 ⊕ Fin 3) ℝ (selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :=
   Basis.mk σSAL_linearly_independent σSAL_span
 
-/-- The decomposition of a self-adjint matrix into the Pauli matrices (where `σi` are negated). -/
+/-- The decomposition of a self-adjoint matrix into the Pauli matrices (where `σi` are negated). -/
 lemma σSAL_decomp (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
     M = (1/2 * (Matrix.trace (σ0 * M.1)).re) • σSAL (Sum.inl 0)
     + (-1/2 * (Matrix.trace (σ1 * M.1)).re) • σSAL (Sum.inr 0)
diff --git a/HepLean/Lorentz/SL2C/SelfAdjoint.lean b/HepLean/Lorentz/SL2C/SelfAdjoint.lean
index e843638..c4864da 100644
--- a/HepLean/Lorentz/SL2C/SelfAdjoint.lean
+++ b/HepLean/Lorentz/SL2C/SelfAdjoint.lean
@@ -175,7 +175,7 @@ lemma toSelfAdjointMap_det_one' {M : ℂ²ˣ²} (hM : M.IsUpperTriangular) (detM
     _ = 1 := by rw [hE]; simp [detD_one, detA_one]
 
 /-- This promotes `Lorentz.SL2C.toSelfAdjointMap M` and its definitional equivalence,
-`Lorentz.SL2C.toSelfAdjointMap' M`, to a linear equivalence by recognising the linear inverse to be
+`Lorentz.SL2C.toSelfAdjointMap' M`, to a linear equivalence by recognizing the linear inverse to be
 `Lorentz.SL2C.toSelfAdjointMap M⁻¹`, i.e., `Lorentz.SL2C.toSelfAdjointMap' M⁻¹`. -/
 noncomputable def toSelfAdjointEquiv (M : ℂ²ˣ²) [Invertible M] : ℍ₂ ≃ₗ[ℝ] ℍ₂ where
   toLinearMap := toSelfAdjointMap' M
diff --git a/HepLean/Lorentz/Weyl/Contraction.lean b/HepLean/Lorentz/Weyl/Contraction.lean
index 0805deb..a5c31c4 100644
--- a/HepLean/Lorentz/Weyl/Contraction.lean
+++ b/HepLean/Lorentz/Weyl/Contraction.lean
@@ -174,11 +174,11 @@ lemma altLeftContraction_basis (i j : Fin 2) :
   exact Eq.propIntro (fun a => id (Eq.symm a)) fun a => id (Eq.symm a)
 
 /--
-The linear map from rightHandedWeyl ⊗ altRightHandedWeyl to ℂ given by
-  summing over components of rightHandedWeyl and altRightHandedWeyl in the
+The linear map from `rightHandedWeyl ⊗ altRightHandedWeyl` to `ℂ` given by
+  summing over components of `rightHandedWeyl` and `altRightHandedWeyl` in the
   standard basis (i.e. the dot product).
   The contraction of a right-handed Weyl fermion with a left-handed Weyl fermion.
-  In index notation this is ψ^{dot a} φ_{dot a}.
+  In index notation this is `ψ^{dot a} φ_{dot a}`.
 -/
 def rightAltContraction : rightHanded ⊗ altRightHanded ⟶ 𝟙_ (Rep ℂ SL(2,ℂ)) where
   hom := ModuleCat.ofHom <| TensorProduct.lift rightAltBi
diff --git a/HepLean/Meta/Remark/Properties.lean b/HepLean/Meta/Remark/Properties.lean
index 374d24f..820843a 100644
--- a/HepLean/Meta/Remark/Properties.lean
+++ b/HepLean/Meta/Remark/Properties.lean
@@ -13,7 +13,7 @@ namespace HepLean
 open Lean
 variable {m} [Monad m] [MonadEnv m] [MonadError m]
 
-/-- All remarks in the enviroment. -/
+/-- All remarks in the environment. -/
 def allRemarkInfo : m (Array RemarkInfo) := do
   let env ← getEnv
   return remarkExtension.getState env
diff --git a/HepLean/PerturbationTheory/FeynmanDiagrams/Momentum.lean b/HepLean/PerturbationTheory/FeynmanDiagrams/Momentum.lean
index 662ff88..9c908fc 100644
--- a/HepLean/PerturbationTheory/FeynmanDiagrams/Momentum.lean
+++ b/HepLean/PerturbationTheory/FeynmanDiagrams/Momentum.lean
@@ -44,7 +44,7 @@ We define the direct sum of the edge and vertex momentum spaces.
 
 -/
 
-/-- The type which assocaites to each half-edge a `1`-dimensional vector space.
+/-- The type which associates to each half-edge a `1`-dimensional vector space.
   Corresponding to that spanned by its momentum. -/
 def HalfEdgeMomenta : Type := F.𝓱𝓔 → ℝ
 
@@ -89,7 +89,7 @@ instance : AddCommGroup F.EdgeMomenta := Pi.addCommGroup
 /-- The edge momenta form a module over `ℝ`. -/
 instance : Module ℝ F.EdgeMomenta := Pi.module _ _ _
 
-/-- The type which assocaites to each ege a `1`-dimensional vector space.
+/-- The type which associates to each ege a `1`-dimensional vector space.
   Corresponding to that spanned by its total inflowing momentum. -/
 def VertexMomenta : Type := F.𝓥 → ℝ
 
diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean
index 3e723bf..9e3bbd8 100644
--- a/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean
+++ b/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean
@@ -224,7 +224,7 @@ For a field specification `𝓕`, an element `φ` of `𝓕.CrAnFieldOp`, a list
 
 `[φ, 𝓝(φ₀…φₙ)]ₛ = ∑ i, 𝓢(φ, φ₀…φᵢ₋₁) • [φ, φᵢ]ₛ * 𝓝(φ₀…φᵢ₋₁φᵢ₊₁…φₙ)`.
 
-The proof of this result ultimetly goes as follows
+The proof of this result ultimately goes as follows
 - The definition of `normalOrder` is used to rewrite `𝓝(φ₀…φₙ)` as a scalar multiple of
   a `ofCrAnList φsn` where `φsn` is the normal ordering of `φ₀…φₙ`.
 - `superCommuteF_ofCrAnListF_ofCrAnListF_eq_sum` is used to rewrite the super commutator of `φ`
@@ -348,7 +348,7 @@ For a field specification `𝓕`, a `φ` in `𝓕.FieldOp` and a list `φs` of `
 the following relation holds in the algebra `𝓕.FieldOpAlgebra`,
 `φ * 𝓝(φ₀φ₁…φₙ) = 𝓝(φφ₀φ₁…φₙ) + ∑ i, (𝓢(φ,φ₀φ₁…φᵢ₋₁) • [anPart φ, φᵢ]ₛ) * 𝓝(φ₀φ₁…φᵢ₋₁φᵢ₊₁…φₙ)`.
 
-The proof of ultimetly goes as follows:
+The proof of ultimately goes as follows:
 - `ofFieldOp_eq_crPart_add_anPart` is used to split `φ` into its creation and annihilation parts.
 - The fact that `crPart φ * 𝓝(φ₀φ₁…φₙ) = 𝓝(crPart φ * φ₀φ₁…φₙ)` is used.
 - The fact that `anPart φ * 𝓝(φ₀φ₁…φₙ)` is
diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/TimeOrder.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/TimeOrder.lean
index 250c2ca..f28070d 100644
--- a/HepLean/PerturbationTheory/FieldOpAlgebra/TimeOrder.lean
+++ b/HepLean/PerturbationTheory/FieldOpAlgebra/TimeOrder.lean
@@ -434,7 +434,7 @@ lemma timeOrder_ofFieldOpList_singleton (φ : 𝓕.FieldOp) :
   list of `𝓕.FieldOp`, `𝓣(φ₀…φₙ)`, is equal to
   `𝓢(φᵢ,φ₀…φᵢ₋₁) • φᵢ * 𝓣(φ₀…φᵢ₋₁φᵢ₊₁φₙ)` where `φᵢ` is the maximal time field in `φ₀…φₙ`.
 
-  The proof of this result ultimitley relies on basic properties of ordering and signs. -/
+  The proof of this result ultimately relies on basic properties of ordering and signs. -/
 lemma timeOrder_eq_maxTimeField_mul_finset (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) :
     𝓣(ofFieldOpList (φ :: φs)) = 𝓢(𝓕 |>ₛ maxTimeField φ φs, 𝓕 |>ₛ ⟨(eraseMaxTimeField φ φs).get,
       (Finset.univ.filter (fun x =>
diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/Universality.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/Universality.lean
index a2ca332..ca5eb42 100644
--- a/HepLean/PerturbationTheory/FieldOpAlgebra/Universality.lean
+++ b/HepLean/PerturbationTheory/FieldOpAlgebra/Universality.lean
@@ -75,7 +75,7 @@ lemma universalLift_ι {A : Type} [Semiring A] [Algebra ℂ A] (f : 𝓕.CrAnFie
     universalLift f h1 (ι a) = FreeAlgebra.lift ℂ f a := by rfl
 
 /--
-For a field specification, `𝓕`, the algebra `𝓕.FieldOpAlgebra` satifies the following universal
+For a field specification, `𝓕`, the algebra `𝓕.FieldOpAlgebra` satisfies the following universal
 property. Let `f : 𝓕.CrAnFieldOp → A` be a function and `g : 𝓕.FieldOpFreeAlgebra →ₐ[ℂ] A`
 the universal lift of that function associated with the free algebra `𝓕.FieldOpFreeAlgebra`.
 If `g` is zero on the ideal defining `𝓕.FieldOpAlgebra`, then there is a unique
diff --git a/HepLean/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean
index 94550d0..ff292f8 100644
--- a/HepLean/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean
+++ b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean
@@ -55,7 +55,7 @@ def ofCrAnOpF (φ : 𝓕.CrAnFieldOp) : FieldOpFreeAlgebra 𝓕 :=
 The algebra `𝓕.FieldOpFreeAlgebra` satisfies the universal property that for any other algebra
   `A` (e.g. the operator algebra of the theory) with a map `f : 𝓕.CrAnFieldOp → A` (e.g.
   the inclusion of the creation and annihilation parts of field operators into the
-  operator algebra) there is a unqiue algebra map `g : 𝓕.FieldOpFreeAlgebra → A`
+  operator algebra) there is a unique algebra map `g : 𝓕.FieldOpFreeAlgebra → A`
   such that `g ∘ ofCrAnOpF = f`.
 
   The unique `g` is given by `FreeAlgebra.lift ℂ f`.
@@ -141,7 +141,7 @@ lemma ofFieldOpListF_sum (φs : List 𝓕.FieldOp) :
 
 -/
 
-/-- The algebra map taking an element of the free-state algbra to
+/-- The algebra map taking an element of the free-state algebra to
   the part of it in the creation and annihilation free algebra
   spanned by creation operators. -/
 def crPartF : 𝓕.FieldOp → 𝓕.FieldOpFreeAlgebra := fun φ =>
@@ -166,7 +166,7 @@ lemma crPartF_posAsymp (φ : (Σ f, 𝓕.AsymptoticLabel f) × (Fin 3 → ℝ))
     crPartF (FieldOp.outAsymp φ) = 0 := by
   simp [crPartF]
 
-/-- The algebra map taking an element of the free-state algbra to
+/-- The algebra map taking an element of the free-state algebra to
   the part of it in the creation and annihilation free algebra
   spanned by annihilation operators. -/
 def anPartF : 𝓕.FieldOp → 𝓕.FieldOpFreeAlgebra := fun φ =>
diff --git a/HepLean/PerturbationTheory/FieldSpecification/CrAnFieldOp.lean b/HepLean/PerturbationTheory/FieldSpecification/CrAnFieldOp.lean
index ef3c3b1..2d56cf3 100644
--- a/HepLean/PerturbationTheory/FieldSpecification/CrAnFieldOp.lean
+++ b/HepLean/PerturbationTheory/FieldSpecification/CrAnFieldOp.lean
@@ -34,7 +34,7 @@ In this module in addition to defining `CrAnFieldOp` we also define some maps:
 namespace FieldSpecification
 variable (𝓕 : FieldSpecification)
 
-/-- To each field operator the specificaition of the type of creation and annihilation parts.
+/-- To each field operator the specification of the type of creation and annihilation parts.
   For asymptotic states there is only one allowed part, whilst for position
   field operator there is two. -/
 def fieldOpToCrAnType : 𝓕.FieldOp → Type
@@ -92,7 +92,7 @@ def crAnFieldOpToCreateAnnihilate : 𝓕.CrAnFieldOp → CreateAnnihilate
 
 /-- For a field specification `𝓕`, and an element `φ` in `𝓕.CrAnFieldOp`, the field
   statistic `crAnStatistics φ` is defined to be the statistic associated with the field `𝓕.Field`
-  (or equivalently `𝓕.FieldOp`) underlying `φ`.
+  (or `𝓕.FieldOp`) underlying `φ`.
 
   The following notation is used in relation to `crAnStatistics`:
   - For `φ` an element of `𝓕.CrAnFieldOp`, `𝓕 |>ₛ φ` is `crAnStatistics φ`.
diff --git a/HepLean/PerturbationTheory/FieldStatistics/Basic.lean b/HepLean/PerturbationTheory/FieldStatistics/Basic.lean
index e9e7e5c..9639ade 100644
--- a/HepLean/PerturbationTheory/FieldStatistics/Basic.lean
+++ b/HepLean/PerturbationTheory/FieldStatistics/Basic.lean
@@ -291,7 +291,7 @@ lemma ofList_take_insertIdx_le (n m : ℕ) (φ1 : 𝓕) (φs : List 𝓕) (hn :
   · exact hn
   · exact hm
 
-/-- The instance of an addative monoid on `FieldStatistic`. -/
+/-- The instance of an additive monoid on `FieldStatistic`. -/
 instance : AddMonoid FieldStatistic where
   zero := bosonic
   add a b := a * b
diff --git a/HepLean/PerturbationTheory/WickContraction/InsertAndContract.lean b/HepLean/PerturbationTheory/WickContraction/InsertAndContract.lean
index 167f74e..93d67b9 100644
--- a/HepLean/PerturbationTheory/WickContraction/InsertAndContract.lean
+++ b/HepLean/PerturbationTheory/WickContraction/InsertAndContract.lean
@@ -34,7 +34,7 @@ open HepLean.Fin
   of `φ` (at position `i`) with the new position of `j` after `φ` is added.
 
   In other words, `φsΛ.insertAndContract φ i j` is formed by adding `φ` to `φs` at position `i`,
-  and contracting `φ` with the field orginally at position `j` if `j` is not none.
+  and contracting `φ` with the field originally at position `j` if `j` is not none.
 
   The notation `φsΛ ↩Λ φ i j` is used to denote `φsΛ.insertAndContract φ i j`. -/
 def insertAndContract {φs : List 𝓕.FieldOp} (φ : 𝓕.FieldOp) (φsΛ : WickContraction φs.length)
diff --git a/HepLean/PerturbationTheory/WickContraction/Sign/InsertSome.lean b/HepLean/PerturbationTheory/WickContraction/Sign/InsertSome.lean
index 52699a8..caa16fc 100644
--- a/HepLean/PerturbationTheory/WickContraction/Sign/InsertSome.lean
+++ b/HepLean/PerturbationTheory/WickContraction/Sign/InsertSome.lean
@@ -201,7 +201,7 @@ lemma signFinset_insertAndContract_some (φ : 𝓕.FieldOp) (φs : List 𝓕.Fie
         rw [Fin.succAbove_lt_succAbove_iff]
 
 /--
-Given a Wick contraction `φsΛ` the sign defined in the followin way,
+Given a Wick contraction `φsΛ` the sign defined in the following way,
 related to inserting a field `φ` at position `i` and contracting it with `j : φsΛ.uncontracted`.
 - For each contracted pair `{a1, a2}` in `φsΛ` with `a1 < a2` the sign
   `𝓢(φ, φₐ₂)` if `a₁ < i ≤ a₂` and `a₁ < j`.
@@ -220,7 +220,7 @@ def signInsertSomeProd (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : Wi
     else
       1
 
-/-- Given a Wick contraction `φsΛ` the sign defined in the followin way,
+/-- Given a Wick contraction `φsΛ` the sign defined in the following way,
 related to inserting a field `φ` at position `i` and contracting it with `j : φsΛ.uncontracted`.
 - If `j < i`, for each field `φₐ` in `φⱼ₊₁…φᵢ₋₁` without a dual at position `< j`
   the sign `𝓢(φₐ, φᵢ)`.
diff --git a/HepLean/PerturbationTheory/WickContraction/SubContraction.lean b/HepLean/PerturbationTheory/WickContraction/SubContraction.lean
index 6378c7e..3342c14 100644
--- a/HepLean/PerturbationTheory/WickContraction/SubContraction.lean
+++ b/HepLean/PerturbationTheory/WickContraction/SubContraction.lean
@@ -21,7 +21,7 @@ open HepLean.List
 open FieldOpAlgebra
 
 /-- Given a Wick contraction `φsΛ`, and a subset of `φsΛ.1`, the Wick contraction
-  conisting of contracted pairs within that subset. -/
+  consisting of contracted pairs within that subset. -/
 def subContraction (S : Finset (Finset (Fin φs.length))) (ha : S ⊆ φsΛ.1) :
     WickContraction φs.length :=
   ⟨S, by
diff --git a/HepLean/PerturbationTheory/WickContraction/TimeCond.lean b/HepLean/PerturbationTheory/WickContraction/TimeCond.lean
index 2480677..4cc6e70 100644
--- a/HepLean/PerturbationTheory/WickContraction/TimeCond.lean
+++ b/HepLean/PerturbationTheory/WickContraction/TimeCond.lean
@@ -314,7 +314,7 @@ lemma empty_not_haveEqTime {φs : List 𝓕.FieldOp} :
   rw [haveEqTime_iff_finset]
   simp [empty]
 
-/-- Given a Wick contraction the subset of contracted pairs between eqaul time fields. -/
+/-- Given a Wick contraction the subset of contracted pairs between equal time fields. -/
 def eqTimeContractSet {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) :
     Finset (Finset (Fin φs.length)) :=
   Finset.univ.filter (fun a =>
diff --git a/HepLean/StandardModel/Basic.lean b/HepLean/StandardModel/Basic.lean
index 8951e88..1e09493 100644
--- a/HepLean/StandardModel/Basic.lean
+++ b/HepLean/StandardModel/Basic.lean
@@ -52,7 +52,7 @@ See https://math.ucr.edu/home/baez/guts.pdf
 informal_definition gaugeGroupℤ₂SubGroup where
   deps := [``GaugeGroupI, ``StandardModel.gaugeGroupℤ₆SubGroup]
 
-/-- The guage group of the Standard Model with a ℤ₂ quotient, i.e., the quotient of `GaugeGroupI` by
+/-- The gauge group of the Standard Model with a ℤ₂ quotient, i.e., the quotient of `GaugeGroupI` by
 the ℤ₂-subgroup `gaugeGroupℤ₂SubGroup`.
 
 See https://math.ucr.edu/home/baez/guts.pdf
@@ -69,7 +69,7 @@ See https://math.ucr.edu/home/baez/guts.pdf
 informal_definition gaugeGroupℤ₃SubGroup where
   deps := [``GaugeGroupI, ``StandardModel.gaugeGroupℤ₆SubGroup]
 
-/-- The guage group of the Standard Model with a ℤ₃-quotient, i.e., the quotient of `GaugeGroupI` by
+/-- The gauge group of the Standard Model with a ℤ₃-quotient, i.e., the quotient of `GaugeGroupI` by
 the ℤ₃-subgroup `gaugeGroupℤ₃SubGroup`.
 
 See https://math.ucr.edu/home/baez/guts.pdf
diff --git a/HepLean/StandardModel/HiggsBoson/GaugeAction.lean b/HepLean/StandardModel/HiggsBoson/GaugeAction.lean
index 9fab2b4..0c2a714 100644
--- a/HepLean/StandardModel/HiggsBoson/GaugeAction.lean
+++ b/HepLean/StandardModel/HiggsBoson/GaugeAction.lean
@@ -118,7 +118,7 @@ lemma rotateMatrix_det {φ : HiggsVec} (hφ : φ ≠ 0) : (rotateMatrix φ).det
   simp [PiLp.inner_apply, Complex.inner, neg_mul, sub_neg_eq_add,
     Fin.sum_univ_two, ofReal_add, ofReal_mul, mul_conj, mul_comm, add_comm]
 
-/-- The `rotateMatrix` for a non-zero Higgs vector is untitary. -/
+/-- The `rotateMatrix` for a non-zero Higgs vector is unitary. -/
 lemma rotateMatrix_unitary {φ : HiggsVec} (hφ : φ ≠ 0) :
     (rotateMatrix φ) ∈ unitaryGroup (Fin 2) ℂ := by
   rw [mem_unitaryGroup_iff', rotateMatrix_star, rotateMatrix]
@@ -148,15 +148,15 @@ lemma rotateMatrix_specialUnitary {φ : HiggsVec} (hφ : φ ≠ 0) :
 
 /-- Given a Higgs vector, an element of the gauge group which puts the first component of the
 vector to zero, and the second component to a real number. -/
-def rotateGuageGroup {φ : HiggsVec} (hφ : φ ≠ 0) : GaugeGroupI :=
+def rotateGaugeGroup {φ : HiggsVec} (hφ : φ ≠ 0) : GaugeGroupI :=
     ⟨1, ⟨(rotateMatrix φ), rotateMatrix_specialUnitary hφ⟩, 1⟩
 
 /-- Acting on a non-zero Higgs vector with its rotation matrix gives a vector which is
   zero in the first component and a positive real in the second component. -/
-lemma rotateGuageGroup_apply {φ : HiggsVec} (hφ : φ ≠ 0) :
-    rep (rotateGuageGroup hφ) φ = ![0, Complex.ofRealHom ‖φ‖] := by
+lemma rotateGaugeGroup_apply {φ : HiggsVec} (hφ : φ ≠ 0) :
+    rep (rotateGaugeGroup hφ) φ = ![0, Complex.ofRealHom ‖φ‖] := by
   rw [rep_apply]
-  simp only [rotateGuageGroup, rotateMatrix, one_pow, one_smul,
+  simp only [rotateGaugeGroup, rotateMatrix, one_pow, one_smul,
     Nat.succ_eq_add_one, Nat.reduceAdd, ofRealHom_eq_coe]
   ext i
   fin_cases i
@@ -184,8 +184,8 @@ theorem rotate_fst_zero_snd_real (φ : HiggsVec) :
       norm_zero]
     ext i
     fin_cases i <;> rfl
-  · use rotateGuageGroup h
-    exact rotateGuageGroup_apply h
+  · use rotateGaugeGroup h
+    exact rotateGaugeGroup_apply h
 
 /-- For every Higgs vector there exists an element of the gauge group which rotates that
   Higgs vector to have `0` in the second component and be a non-negative real in the first
diff --git a/HepLean/StandardModel/HiggsBoson/Potential.lean b/HepLean/StandardModel/HiggsBoson/Potential.lean
index 775b8e3..504165e 100644
--- a/HepLean/StandardModel/HiggsBoson/Potential.lean
+++ b/HepLean/StandardModel/HiggsBoson/Potential.lean
@@ -120,7 +120,7 @@ lemma toFun_eq_zero_iff (h : P.𝓵 ≠ 0) (φ : HiggsField) (x : SpaceTime) :
 
 -/
 
-/-- The discrimiant of the quadratic equation formed by the Higgs potential. -/
+/-- The discriminant of the quadratic equation formed by the Higgs potential. -/
 def quadDiscrim (φ : HiggsField) (x : SpaceTime) : ℝ := discrim P.𝓵 (- P.μ2) (- P.toFun φ x)
 
 /-- The discriminant of the quadratic formed by the potential is non-negative. -/
@@ -325,7 +325,7 @@ lemma isBounded_of_𝓵_pos (h : 0 < P.𝓵) : P.IsBounded := by
 
 /-- When there is no quartic coupling, the potential is bounded iff the mass squared is
 non-positive, i.e., for `P : Potential` then `P.IsBounded` iff `P.μ2 ≤ 0`. That is to say
-`- P.μ2 * ‖φ‖_H^2 x` is bounded below ifff `P.μ2 ≤ 0`. -/
+`- P.μ2 * ‖φ‖_H^2 x` is bounded below iff `P.μ2 ≤ 0`. -/
 informal_lemma isBounded_iff_of_𝓵_zero where
   deps := [`StandardModel.HiggsField.Potential.IsBounded, `StandardModel.HiggsField.Potential]
 
diff --git a/HepLean/Tensors/OverColor/Iso.lean b/HepLean/Tensors/OverColor/Iso.lean
index 4ad7b45..d2cbbf2 100644
--- a/HepLean/Tensors/OverColor/Iso.lean
+++ b/HepLean/Tensors/OverColor/Iso.lean
@@ -90,7 +90,7 @@ lemma equivToIso_mkIso_inv {c1 c2 : X → C} (h : c1 = c2) :
     Hom.toEquiv (mkIso h).inv = Equiv.refl _ := by
   rfl
 
-/-- The homorophism from `mk c` to `mk c1` obtaied by an equivalence and
+/-- The morphism from `mk c` to `mk c1` obtained by an equivalence and
   an equality lemma. -/
 def equivToHomEq {c : X → C} {c1 : Y → C} (e : X ≃ Y)
     (h : ∀ x, c1 x = (c ∘ e.symm) x := by decide) : mk c ⟶ mk c1 :=
diff --git a/HepLean/Tensors/TensorSpecies/Basic.lean b/HepLean/Tensors/TensorSpecies/Basic.lean
index 8bbbada..2054c58 100644
--- a/HepLean/Tensors/TensorSpecies/Basic.lean
+++ b/HepLean/Tensors/TensorSpecies/Basic.lean
@@ -93,13 +93,13 @@ open OverColor
 
 variable (S : TensorSpecies)
 
-/-- The field `k` of a TensorSpecies has the instance of a commutative ring. -/
+/-- The field `k` of a `TensorSpecies` has the instance of a commutative ring. -/
 instance : CommRing S.k := S.k_commRing
 
-/-- The field `G` of a TensorSpecies has the instance of a group. -/
+/-- The field `G` of a `TensorSpecies` has the instance of a group. -/
 instance : Group S.G := S.G_group
 
-/-- The field `repDim` of a TensorSpecies is non-zero for all colors. -/
+/-- The field `repDim` of a `TensorSpecies` is non-zero for all colors. -/
 instance (c : S.C) : NeZero (S.repDim c) := S.repDim_neZero c
 
 /-- The lift of the functor `S.F` to functor. -/
diff --git a/HepLean/Tensors/TensorSpecies/UnitTensor.lean b/HepLean/Tensors/TensorSpecies/UnitTensor.lean
index 4160f18..d6496ba 100644
--- a/HepLean/Tensors/TensorSpecies/UnitTensor.lean
+++ b/HepLean/Tensors/TensorSpecies/UnitTensor.lean
@@ -97,7 +97,7 @@ lemma unitTensor_eq_dual_perm (c : S.C) : {S.unitTensor c | μ ν}ᵀ.tensor =
   exact congrFun (congrArg (fun f => f.toFun) hg) _
 
 /-- The unit tensor of the dual of a color `c` is equal to the unit tensor of `c`
-  with indicees permuted. -/
+  with indices permuted. -/
 lemma dual_unitTensor_eq_perm (c : S.C) :
     {S.unitTensor (S.τ c) | ν μ}ᵀ.tensor = ({S.unitTensor c | μ ν}ᵀ |>
     perm (OverColor.equivToHomEq (finMapToEquiv ![1, 0] ![1, 0])
diff --git a/HepLean/Tensors/Tree/NodeIdentities/Basic.lean b/HepLean/Tensors/Tree/NodeIdentities/Basic.lean
index ce9dc19..e4f6fd3 100644
--- a/HepLean/Tensors/Tree/NodeIdentities/Basic.lean
+++ b/HepLean/Tensors/Tree/NodeIdentities/Basic.lean
@@ -125,7 +125,7 @@ lemma perm_eq_id {n : ℕ} {c : Fin n → S.C} (σ : (OverColor.mk c) ⟶ (OverC
   simp [perm_tensor, h]
 
 /-- Given an equality of tensors corresponding to tensor trees where the tensor tree on the
-  left finishes with a premotion node, this permutation node can be moved to the
+  left finishes with a permutation node, this permutation node can be moved to the
   tensor tree on the right. This lemma holds here for isomorphisms only, but holds in practice
   more generally. -/
 lemma perm_eq_of_eq_perm {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
diff --git a/scripts/README.md b/scripts/README.md
index 6a49ffb..0f9bf94 100644
--- a/scripts/README.md
+++ b/scripts/README.md
@@ -1,91 +1,91 @@
 
-# Scripts associated with HepLean 
+# Scripts associated with HepLean
 
 ## lint-style.py and lint-style.sh
 
-Taken from Mathlib's linters. These perform text-based linting of the code. 
+Taken from Mathlib's linters. These perform text-based linting of the code.
 
 These are to be slowly replaced with code written in Lean.
 
 ## hepLean_style_lint
 
-Checks the following in HepLean 
-- There are no double empty lines. 
-- There are no non-initial double spaces.  
+Checks the following in HepLean
+- There are no double empty lines.
+- There are no non-initial double spaces.
 Passing this linter is currently not required to pass CI on github.
 
-Run using 
+Run using
 ```
 lake exe hepLean_style_lint
 ```
 
-## check_file_imports.lean 
+## check_file_imports.lean
 
-Checks all files are correctly imported into `HepLean.lean`. 
+Checks all files are correctly imported into `HepLean.lean`.
 
-Run using 
+Run using
 ```
 lake exe check_file_imports
 ```
 
 ## type_former_lint.lean
 
-Checks whether the name of definitions which form a type or prop starts with a capital letter. 
+Checks whether the name of definitions which form a type or prop starts with a capital letter.
 
-Run using 
+Run using
 ```
 lake exe type_former_lint
 ```
 
-## stats.sh 
+## stats.sh
 
-Outputs statistics for HepLean. 
+Outputs statistics for HepLean.
 
-Run using 
+Run using
 ```
 lake exe stats
 ```
 
-## openAI_doc_check.lean 
+## openAI_doc_check.lean
 
-Uses openAI's API to check for spelling mistakes etc. in doc strings. 
+Uses openAI's API to check for spelling mistakes etc. in doc strings.
 
-This code needs `https://github.com/jstoobysmith/Lean_llm_fork` to be installed. 
+This code needs `https://github.com/jstoobysmith/Lean_llm_fork` to be installed.
 
-It also needs the enviroment variable `OPENAI_API_KEY` defined using e.g. 
+It also needs the environment variable `OPENAI_API_KEY` defined using e.g.
 ```
 export OPENAI_API_KEY=<Your-openAI-key>
 ```
 
-Run on a specific file using 
+Run on a specific file using
 ```
 lake exe openAI_doc_check <module_name>
 ```
-where `<module_name>` is e.g. `HepLean.SpaceTime.Basic`. 
+where `<module_name>` is e.g. `HepLean.SpaceTime.Basic`.
 
-Run on a random file using 
+Run on a random file using
 ```
 lake exe openAI_doc_check random
 ```
 
-## lint-all.sh 
+## lint-all.sh
 
-Performs all linting checks on HepLean. 
+Performs all linting checks on HepLean.
 
-Run using 
+Run using
 ```
 ./scripts/lint-all.sh
 ```
 
 ## Other useful commands
 
-- To build HepLean use 
+- To build HepLean use
 ```
-lake exe cache get 
+lake exe cache get
 lake build
 ```
 
-- To update HepLean's dependencies use 
+- To update HepLean's dependencies use
 ```
 lake update
-```
\ No newline at end of file
+```