diff --git a/HepLean/Tensors/OverColor/Basic.lean b/HepLean/Tensors/OverColor/Basic.lean
index b32fcef..9695a52 100644
--- a/HepLean/Tensors/OverColor/Basic.lean
+++ b/HepLean/Tensors/OverColor/Basic.lean
@@ -17,7 +17,7 @@ The way to describe color is through examples.
 Indices of real Lorentz tensors can either be up-colored or down-colored.
 On the other hand, indices of Einstein tensors can just down-colored.
 In the case of complex Lorentz tensors, indices can take one of six different colors,
-corresponding to up and down, dotted and undotted weyl fermion indcies and up and down
+corresponding to up and down, dotted and undotted weyl fermion indices and up and down
 Lorentz indices.
 
 -/
diff --git a/HepLean/Tensors/OverColor/Discrete.lean b/HepLean/Tensors/OverColor/Discrete.lean
index b7863b8..834e8ba 100644
--- a/HepLean/Tensors/OverColor/Discrete.lean
+++ b/HepLean/Tensors/OverColor/Discrete.lean
@@ -46,7 +46,7 @@ def pairIso (c : C) : (pair F).obj (Discrete.mk c) ≅ (lift.obj F).obj (OverCol
     rfl
 
 /-- The isomorphism between `F.obj (Discrete.mk c1) ⊗ F.obj (Discrete.mk c2)` and
-  `(lift.obj F).obj (OverColor.mk ![c1,c2])` formed by the tensorate. -/
+  `(lift.obj F).obj (OverColor.mk ![c1,c2])` formed by the tensor. -/
 def pairIsoSep {c1 c2 : C} : F.obj (Discrete.mk c1) ⊗ F.obj (Discrete.mk c2) ≅
     (lift.obj F).obj (OverColor.mk ![c1,c2]) := by
   symm
@@ -200,7 +200,7 @@ lemma pairIsoSep_β {c1 c2 : C} (x : ↑(F.obj { as := c1 } ⊗ F.obj { as := c2
 
 /-- The isomorphism between
   `F.obj (Discrete.mk c1) ⊗ F.obj (Discrete.mk c2) ⊗ F.obj (Discrete.mk c3)` and
-  `(lift.obj F).obj (OverColor.mk ![c1,c2])` formed by the tensorate. -/
+  `(lift.obj F).obj (OverColor.mk ![c1,c2])` formed by the tensor. -/
 def tripleIsoSep {c1 c2 c3 : C} :
     F.obj (Discrete.mk c1) ⊗ F.obj (Discrete.mk c2) ⊗ F.obj (Discrete.mk c3) ≅
     (lift.obj F).obj (OverColor.mk ![c1,c2,c3]) :=
diff --git a/HepLean/Tensors/OverColor/Lift.lean b/HepLean/Tensors/OverColor/Lift.lean
index dd3fc41..af723d1 100644
--- a/HepLean/Tensors/OverColor/Lift.lean
+++ b/HepLean/Tensors/OverColor/Lift.lean
@@ -16,7 +16,7 @@ sense that it is a section of the forgetful functor
 
 Functors in `Discrete C ⥤ Rep k G` form the basic building blocks of tensor structures.
 The fact that they extend to monoidal functors `OverColor C ⥤ Rep k G` allows us to
-interfact more generally with tensors.
+interact more generally with tensors.
 
 -/
 
@@ -30,7 +30,7 @@ variable {C k : Type} [CommRing k] {G : Type} [Group G]
 
 namespace Discrete
 
-/-- Takes a homorphism in `Discrete C` to an isomorphism built on the same objects. -/
+/-- Takes a homomorphism in `Discrete C` to an isomorphism built on the same objects. -/
 def homToIso {c1 c2 : Discrete C} (h : c1 ⟶ c2) : c1 ≅ c2 :=
   Discrete.eqToIso (Discrete.eq_of_hom h)
 
@@ -40,7 +40,7 @@ namespace lift
 noncomputable section
 variable (F F' : Discrete C ⥤ Rep k G) (η : F ⟶ F')
 
-/-- Takes a homorphisms of `Discrete C` to an isomorphism `F.obj c1 ≅ F.obj c2`. -/
+/-- Takes a homomorphism of `Discrete C` to an isomorphism `F.obj c1 ≅ F.obj c2`. -/
 def discreteFunctorMapIso {c1 c2 : Discrete C} (h : c1 ⟶ c2) :
     F.obj c1 ≅ F.obj c2 := F.mapIso (Discrete.homToIso h)
 
@@ -83,7 +83,7 @@ lemma discreteFunctorMapEqIso_comm_ρ {c1 c2 : Discrete C} (h : c1.as = c2.as) (
     Action.id_hom, Iso.refl_inv, LinearEquiv.ofLinear_apply]
   rfl
 
-/-- Given a object in `OverColor Color` the correpsonding tensor product of representations. -/
+/-- Given a object in `OverColor Color` the corresponding tensor product of representations. -/
 def objObj' (f : OverColor C) : Rep k G := Rep.of {
   toFun := fun M => PiTensorProduct.map (fun x =>
     (F.obj (Discrete.mk (f.hom x))).ρ M),
@@ -127,7 +127,7 @@ open TensorProduct in
 lemma objObj'_V_carrier (f : OverColor C) :
     (objObj' F f).V = ⨂[k] (i : f.left), F.obj (Discrete.mk (f.hom i)) := rfl
 
-/-- Given a morphism in `OverColor C` the corresopnding linear equivalence between `obj' _`
+/-- Given a morphism in `OverColor C` the corresponding linear equivalence between `obj' _`
   induced by reindexing. -/
 def mapToLinearEquiv' {f g : OverColor C} (m : f ⟶ g) : (objObj' F f).V ≃ₗ[k] (objObj' F g).V :=
   (PiTensorProduct.reindex k (fun x => (F.obj (Discrete.mk (f.hom x))))
@@ -148,7 +148,7 @@ lemma mapToLinearEquiv'_tprod {f g : OverColor C} (m : f ⟶ g)
   rw [PiTensorProduct.reindex_tprod, PiTensorProduct.congr_tprod]
   rfl
 
-/-- Given a morphism in `OverColor C` the corresopnding map of representations induced by
+/-- Given a morphism in `OverColor C` the corresponding map of representations induced by
   reindexing. -/
 def objMap' {f g : OverColor C} (m : f ⟶ g) : objObj' F f ⟶ objObj' F g where
   hom := (mapToLinearEquiv' F m).toLinearMap
@@ -198,7 +198,7 @@ def ε : 𝟙_ (Rep k G) ≅ objObj' F (𝟙_ (OverColor C)) :=
     erw [objObj'_ρ_empty F g]
     rfl)
 
-/-- An auxillary equivalence, and trivial, of modules needed to define `μModEquiv`. -/
+/-- An auxiliary equivalence, and trivial, of modules needed to define `μModEquiv`. -/
 def discreteSumEquiv {X Y : OverColor C} (i : X.left ⊕ Y.left) :
     Sum.elim (fun i => F.obj (Discrete.mk (X.hom i)))
     (fun i => F.obj (Discrete.mk (Y.hom i))) i ≃ₗ[k] F.obj (Discrete.mk ((X ⊗ Y).hom i)) :=
@@ -215,7 +215,7 @@ def discreteSumEquiv' {X Y : Type} {cX : X → C} {cY : Y → C} (i : X ⊕ Y) :
   | Sum.inl _ => LinearEquiv.refl _ _
   | Sum.inr _ => LinearEquiv.refl _ _
 
-/-- The equivalence of modules corresonding to the tensorate. -/
+/-- The equivalence of modules corresponding to the tensor. -/
 def μModEquiv (X Y : OverColor C) :
     (objObj' F X ⊗ objObj' F Y).V ≃ₗ[k] objObj' F (X ⊗ Y) :=
   HepLean.PiTensorProduct.tmulEquiv ≪≫ₗ PiTensorProduct.congr (discreteSumEquiv F)
@@ -238,7 +238,7 @@ lemma μModEquiv_tmul_tprod {X Y : OverColor C}
   rw [PiTensorProduct.congr_tprod]
   rfl
 
-/-- The natural isomorphism corresponding to the tensorate. -/
+/-- The natural isomorphism corresponding to the tensor. -/
 def μ (X Y : OverColor C) : objObj' F X ⊗ objObj' F Y ≅ objObj' F (X ⊗ Y) :=
   Action.mkIso (μModEquiv F X Y).toModuleIso
   (fun M => by
diff --git a/HepLean/Tensors/TensorSpecies/Contractions/Categorical.lean b/HepLean/Tensors/TensorSpecies/Contractions/Categorical.lean
index cc06d67..2857f92 100644
--- a/HepLean/Tensors/TensorSpecies/Contractions/Categorical.lean
+++ b/HepLean/Tensors/TensorSpecies/Contractions/Categorical.lean
@@ -27,7 +27,7 @@ open TensorTree
 
 variable {S : TensorSpecies}
 
-/-- Th map built contracting a 1-tensor with a 2-tensor using basic categorical consstructions.s -/
+/-- Th map built contracting a 1-tensor with a 2-tensor using basic categorical constructions. -/
 def contrOneTwoLeft {c1 c2 : S.C}
     (x : S.F.obj (OverColor.mk ![c1])) (y : S.F.obj (OverColor.mk ![S.τ c1, c2])) :
     S.F.obj (OverColor.mk ![c2]) :=
diff --git a/HepLean/Tensors/TensorSpecies/Contractions/ContrMap.lean b/HepLean/Tensors/TensorSpecies/Contractions/ContrMap.lean
index b1dc6c3..f73b558 100644
--- a/HepLean/Tensors/TensorSpecies/Contractions/ContrMap.lean
+++ b/HepLean/Tensors/TensorSpecies/Contractions/ContrMap.lean
@@ -22,7 +22,7 @@ namespace TensorSpecies
 
 variable (S : TensorSpecies)
 
-/-- The isomorphism between the image of a map `Fin 1 ⊕ Fin 1 → S.C` contructed by `finExtractTwo`
+/-- The isomorphism between the image of a map `Fin 1 ⊕ Fin 1 → S.C` constructed by `finExtractTwo`
   under `S.F.obj`, and an object in the image of `OverColor.Discrete.pairτ S.FD`. -/
 def contrFin1Fin1 {n : ℕ} (c : Fin n.succ.succ → S.C)
     (i : Fin n.succ.succ) (j : Fin n.succ) (h : c (i.succAbove j) = S.τ (c i)) :