diff --git a/HepLean/FeynmanDiagrams/Basic.lean b/HepLean/FeynmanDiagrams/Basic.lean
index 6df89ef..1dab9cc 100644
--- a/HepLean/FeynmanDiagrams/Basic.lean
+++ b/HepLean/FeynmanDiagrams/Basic.lean
@@ -137,14 +137,17 @@ class IsFinitePreFeynmanRule (P : PreFeynmanRule) where
   /-- The type of half-edges associated with an edge is decidable. -/
   edgeMapDecidable : ∀ v : P.EdgeLabel, DecidableEq (P.edgeLabelMap v).left
 
+/-- If `P` is a finite pre feynman rule, then equality of edge labels of `P` is decidable. -/
 instance preFeynmanRuleDecEq𝓔 (P : PreFeynmanRule) [IsFinitePreFeynmanRule P] :
     DecidableEq P.EdgeLabel :=
   IsFinitePreFeynmanRule.edgeLabelDecidable
 
+/-- If `P` is a finite pre feynman rule, then equality of vertex labels of `P` is decidable. -/
 instance preFeynmanRuleDecEq𝓥 (P : PreFeynmanRule) [IsFinitePreFeynmanRule P] :
     DecidableEq P.VertexLabel :=
   IsFinitePreFeynmanRule.vertexLabelDecidable
 
+/-- If `P` is a finite pre feynman rule, then equality of half-edge labels of `P` is decidable. -/
 instance preFeynmanRuleDecEq𝓱𝓔 (P : PreFeynmanRule) [IsFinitePreFeynmanRule P] :
     DecidableEq P.HalfEdgeLabel :=
   IsFinitePreFeynmanRule.halfEdgeLabelDecidable
@@ -425,27 +428,37 @@ instance {𝓔 𝓥 𝓱𝓔 : Type} [h1 : Fintype 𝓔] [h2 : DecidableEq 𝓔]
     IsFiniteDiagram (mk' 𝓔𝓞 𝓥𝓞 𝓱𝓔To𝓔𝓥 C) :=
   ⟨h1, h2, h3, h4, h5, h6⟩
 
+/-- If `F` is a finite Feynman diagram, then its edges are finite. -/
 instance {F : FeynmanDiagram P} [IsFiniteDiagram F] : Fintype F.𝓔 :=
   IsFiniteDiagram.𝓔Fintype
 
+/-- If `F` is a finite Feynman diagram, then its edges are decidable. -/
 instance {F : FeynmanDiagram P} [IsFiniteDiagram F] : DecidableEq F.𝓔 :=
   IsFiniteDiagram.𝓔DecidableEq
 
+/-- If `F` is a finite Feynman diagram, then its vertices are finite. -/
 instance {F : FeynmanDiagram P} [IsFiniteDiagram F] : Fintype F.𝓥 :=
   IsFiniteDiagram.𝓥Fintype
 
+/-- If `F` is a finite Feynman diagram, then its vertices are decidable. -/
 instance {F : FeynmanDiagram P} [IsFiniteDiagram F] : DecidableEq F.𝓥 :=
   IsFiniteDiagram.𝓥DecidableEq
 
+/-- If `F` is a finite Feynman diagram, then its half-edges are finite. -/
 instance {F : FeynmanDiagram P} [IsFiniteDiagram F] : Fintype F.𝓱𝓔 :=
   IsFiniteDiagram.𝓱𝓔Fintype
 
+/-- If `F` is a finite Feynman diagram, then its half-edges are decidable. -/
 instance {F : FeynmanDiagram P} [IsFiniteDiagram F] : DecidableEq F.𝓱𝓔 :=
   IsFiniteDiagram.𝓱𝓔DecidableEq
 
+/-- The proposition of whether the given an half-edge and an edge,
+  the edge corresponding to the half edges is the given edge is decidable. -/
 instance {F : FeynmanDiagram P} [IsFiniteDiagram F] (i : F.𝓱𝓔) (j : F.𝓔) :
     Decidable (F.𝓱𝓔To𝓔.hom i = j) := IsFiniteDiagram.𝓔DecidableEq (F.𝓱𝓔To𝓔.hom i) j
 
+/-- For a finite feynman diagram, the type of half edge lables, edges and vertices
+  is decidable. -/
 instance fintypeProdHalfEdgeLabel𝓔𝓥 {F : FeynmanDiagram P} [IsFinitePreFeynmanRule P]
     [IsFiniteDiagram F] : DecidableEq (P.HalfEdgeLabel × F.𝓔 × F.𝓥) :=
   instDecidableEqProd
@@ -557,10 +570,16 @@ lemma cond_symm {F G : FeynmanDiagram P} (𝓔 : F.𝓔 ≃ G.𝓔) (𝓥 : F.
     simp only [Functor.const_obj_obj, Equiv.apply_symm_apply] at h1
     exact (edgeVertexEquiv 𝓔 𝓥).apply_eq_iff_eq_symm_apply.mp (h1).symm
 
+/-- If `𝓔` is a map between the edges of one finite Feynman diagram and another Feynman diagram,
+  then deciding whether `𝓔` froms a morphism in `Over P.EdgeLabel` between the edge
+  maps is decidable. -/
 instance {F G : FeynmanDiagram P} [IsFiniteDiagram F] [IsFinitePreFeynmanRule P]
     (𝓔 : F.𝓔 → G.𝓔) : Decidable (∀ x, G.𝓔𝓞.hom (𝓔 x) = F.𝓔𝓞.hom x) :=
   @Fintype.decidableForallFintype _ _ (fun _ => preFeynmanRuleDecEq𝓔 P _ _) _
 
+/-- If `𝓥` is a map between the vertices of one finite Feynman diagram and another Feynman diagram,
+  then deciding whether `𝓥` froms a morphism in `Over P.VertexLabel` between the vertex
+  maps is decidable. -/
 instance {F G : FeynmanDiagram P} [IsFiniteDiagram F] [IsFinitePreFeynmanRule P]
     (𝓥 : F.𝓥 → G.𝓥) : Decidable (∀ x, G.𝓥𝓞.hom (𝓥 x) = F.𝓥𝓞.hom x) :=
   @Fintype.decidableForallFintype _ _ (fun _ => preFeynmanRuleDecEq𝓥 P _ _) _
diff --git a/HepLean/FeynmanDiagrams/Instances/ComplexScalar.lean b/HepLean/FeynmanDiagrams/Instances/ComplexScalar.lean
index d51a6a0..50a3529 100644
--- a/HepLean/FeynmanDiagrams/Instances/ComplexScalar.lean
+++ b/HepLean/FeynmanDiagrams/Instances/ComplexScalar.lean
@@ -32,15 +32,19 @@ def complexScalarFeynmanRules : PreFeynmanRule where
     | 1 => Over.mk ![1]
     | 2 => Over.mk ![0, 0, 1, 1]
 
+/-- An instance allowing us to use integers for edge labels for complex scalar theory. -/
 instance (a : ℕ) : OfNat complexScalarFeynmanRules.EdgeLabel a where
   ofNat := (a : Fin _)
 
+/-- An instance allowing us to use integers for half-edge labels for complex scalar theory. -/
 instance (a : ℕ) : OfNat complexScalarFeynmanRules.HalfEdgeLabel a where
   ofNat := (a : Fin _)
 
+/-- An instance allowing us to use integers for vertex labels for complex scalar theory. -/
 instance (a : ℕ) : OfNat complexScalarFeynmanRules.VertexLabel a where
   ofNat := (a : Fin _)
 
+/-- The pre feynman rules for complex scalars are finite. -/
 instance : IsFinitePreFeynmanRule complexScalarFeynmanRules where
   edgeLabelDecidable := instDecidableEqFin _
   vertexLabelDecidable := instDecidableEqFin _
diff --git a/HepLean/FeynmanDiagrams/Instances/Phi4.lean b/HepLean/FeynmanDiagrams/Instances/Phi4.lean
index 14a318a..8f9df3f 100644
--- a/HepLean/FeynmanDiagrams/Instances/Phi4.lean
+++ b/HepLean/FeynmanDiagrams/Instances/Phi4.lean
@@ -34,15 +34,19 @@ def phi4PreFeynmanRules : PreFeynmanRule where
     | 0 => Over.mk ![0]
     | 1 => Over.mk ![0, 0, 0, 0]
 
+/-- An instance allowing us to use integers for edge labels for Phi-4. -/
 instance (a : ℕ) : OfNat phi4PreFeynmanRules.EdgeLabel a where
   ofNat := (a : Fin _)
 
+/-- An instance allowing us to use integers for half edge labels for Phi-4. -/
 instance (a : ℕ) : OfNat phi4PreFeynmanRules.HalfEdgeLabel a where
   ofNat := (a : Fin _)
 
+/-- An instance allowing us to use integers for vertex labels for Phi-4. -/
 instance (a : ℕ) : OfNat phi4PreFeynmanRules.VertexLabel a where
   ofNat := (a : Fin _)
 
+/-- The pre feynman rules for Phi-4 are finite. -/
 instance : IsFinitePreFeynmanRule phi4PreFeynmanRules where
   edgeLabelDecidable := instDecidableEqFin _
   vertexLabelDecidable := instDecidableEqFin _
diff --git a/HepLean/FeynmanDiagrams/Momentum.lean b/HepLean/FeynmanDiagrams/Momentum.lean
index 5a33c3c..705d3fb 100644
--- a/HepLean/FeynmanDiagrams/Momentum.lean
+++ b/HepLean/FeynmanDiagrams/Momentum.lean
@@ -48,8 +48,10 @@ We define the direct sum of the edge and vertex momentum spaces.
   Corresponding to that spanned by its momentum. -/
 def HalfEdgeMomenta : Type := F.𝓱𝓔 → ℝ
 
+/-- The half momenta carries the structure of an addative commutative group. -/
 instance : AddCommGroup F.HalfEdgeMomenta := Pi.addCommGroup
 
+/-- The half momenta carries the structure of a module over `ℝ`. Defined via its target. -/
 instance : Module ℝ F.HalfEdgeMomenta := Pi.module _ _ _
 
 /-- An auxiliary function used to define the Euclidean inner product on `F.HalfEdgeMomenta`. -/
@@ -81,16 +83,20 @@ def euclidInner : F.HalfEdgeMomenta →ₗ[ℝ] F.HalfEdgeMomenta →ₗ[ℝ] 
   Corresponding to that spanned by its total outflowing momentum. -/
 def EdgeMomenta : Type := F.𝓔 → ℝ
 
+/-- The edge momenta form an addative commuative group. -/
 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.
   Corresponding to that spanned by its total inflowing momentum. -/
 def VertexMomenta : Type := F.𝓥 → ℝ
 
+/-- The vertex momenta carries the structure of an addative commuative group. -/
 instance : AddCommGroup F.VertexMomenta := Pi.addCommGroup
 
+/-- The vertex momenta carries the structure of a module over `ℝ`. -/
 instance : Module ℝ F.VertexMomenta := Pi.module _ _ _
 
 /-- The map from `Fin 2` to `Type` landing on `EdgeMomenta` and `VertexMomenta`. -/
@@ -99,11 +105,15 @@ def EdgeVertexMomentaMap : Fin 2 → Type := fun i =>
   | 0 => F.EdgeMomenta
   | 1 => F.VertexMomenta
 
+/-- The target of the map `EdgeVertexMomentaMap` is either the type of edge momenta
+  or vertex momenta and thus carries the structure of an addative commuative group. -/
 instance (i : Fin 2) : AddCommGroup (EdgeVertexMomentaMap F i) :=
   match i with
   | 0 => instAddCommGroupEdgeMomenta F
   | 1 => instAddCommGroupVertexMomenta F
 
+/-- The target of the map `EdgeVertexMomentaMap` is either the type of edge momenta
+  or vertex momenta and thus carries the structure of a module over `ℝ`. -/
 instance (i : Fin 2) : Module ℝ (EdgeVertexMomentaMap F i) :=
   match i with
   | 0 => instModuleRealEdgeMomenta F
diff --git a/HepLean/Lorentz/ComplexTensor/Basic.lean b/HepLean/Lorentz/ComplexTensor/Basic.lean
index 9a8396f..e331cd5 100644
--- a/HepLean/Lorentz/ComplexTensor/Basic.lean
+++ b/HepLean/Lorentz/ComplexTensor/Basic.lean
@@ -199,6 +199,8 @@ namespace complexLorentzTensor
 /-- Color for complex Lorentz tensors is decidable. -/
 instance : DecidableEq complexLorentzTensor.C := complexLorentzTensor.instDecidableEqColor
 
+/-- Contracting two basis elements gives `1` if the index for the basis elements is the same,
+  and `0` otherwise. Holds for any color of index. -/
 lemma basis_contr (c : complexLorentzTensor.C) (i : Fin (complexLorentzTensor.repDim c))
     (j : Fin (complexLorentzTensor.repDim (complexLorentzTensor.τ c))) :
     complexLorentzTensor.castToField
@@ -213,9 +215,11 @@ lemma basis_contr (c : complexLorentzTensor.C) (i : Fin (complexLorentzTensor.re
   | Color.up => Lorentz.contrCoContraction_basis _ _
   | Color.down => Lorentz.coContrContraction_basis _ _
 
+/-- For any object in the over color category, with source `Fin n`, has a decidable source. -/
 instance {n : ℕ} {c : Fin n → complexLorentzTensor.C} :
     DecidableEq (OverColor.mk c).left := instDecidableEqFin n
 
+/-- For any object in the over color category, with source `Fin n`, has a finite source. -/
 instance {n : ℕ} {c : Fin n → complexLorentzTensor.C} :
     Fintype (OverColor.mk c).left := Fin.fintype n
 
diff --git a/HepLean/Lorentz/RealVector/Basic.lean b/HepLean/Lorentz/RealVector/Basic.lean
index 8d43efc..b27217b 100644
--- a/HepLean/Lorentz/RealVector/Basic.lean
+++ b/HepLean/Lorentz/RealVector/Basic.lean
@@ -30,6 +30,8 @@ open minkowskiMatrix
   Lorentz vectors. In index notation these have an up index `ψⁱ`. -/
 def Contr (d : ℕ) : Rep ℝ (LorentzGroup d) := Rep.of ContrMod.rep
 
+/-- The representation of contrvariant Lorentz vectors forms a topological space, induced
+  by its equivalence to `Fin 1 ⊕ Fin d → ℝ`. -/
 instance : TopologicalSpace (Contr d) := TopologicalSpace.induced
   ContrMod.toFin1dℝEquiv (Pi.topologicalSpace)
 
diff --git a/HepLean/Mathematics/PiTensorProduct.lean b/HepLean/Mathematics/PiTensorProduct.lean
index 910b460..f5ca75d 100644
--- a/HepLean/Mathematics/PiTensorProduct.lean
+++ b/HepLean/Mathematics/PiTensorProduct.lean
@@ -154,11 +154,15 @@ lemma induction_mod_tmul
 # Dependent type version of PiTensorProduct.tmulEquiv
 -/
 
+/-- Given two maps `s1` and `s2` whose targets carry an instance of an addative commutative
+  monoid, the target of the sum of these two maps also carry an instance thereof. -/
 instance : (i : ι1 ⊕ ι2) → AddCommMonoid ((fun i => Sum.elim s1 s2 i) i) := fun i =>
   match i with
   | Sum.inl i => inst1 i
   | Sum.inr i => inst2 i
 
+/-- Given two maps `s1` and `s2` whose targets carry an instance of a module over `R`,
+  the target of the sum of these two maps also carry an instance thereof. -/
 instance : (i : ι1 ⊕ ι2) → Module R ((fun i => Sum.elim s1 s2 i) i) := fun i =>
   match i with
   | Sum.inl i => inst1' i