docs: More docs related to elab

HepLean/Tensors/Tree/Basic.lean

@@ -11,6 +11,14 @@ import Mathlib.CategoryTheory.Monoidal.NaturalTransformation
 
 # Tensor species and trees
 
+## Tensor species
+
+- A tensor species is a structure including all of the ingredients needed to define a type of
+  tensor.
+- Examples of tensor species will include real Lorentz tensors, complex Lorentz tensors, and
+  Einstien tensors.
+- Tensor species are built upon symmetric monoidal categories.
+
 ## Trees
 
 - Tensor trees provide an abstract way to represent tensor expressions.
@@ -110,6 +118,7 @@ instance (c : S.C) : NeZero (S.repDim c) := S.repDim_neZero c
 /-- The lift of the functor `S.F` to a monoidal functor. -/
 def F : BraidedFunctor (OverColor S.C) (Rep S.k S.G) := (OverColor.lift).obj S.FDiscrete
 
+/- The definition of `F` as a lemma. -/
 lemma F_def : F S = (OverColor.lift).obj S.FDiscrete := rfl
 
 lemma perm_contr_cond {n : ℕ} {c : Fin n.succ.succ → S.C} {c1 : Fin n.succ.succ → S.C}

HepLean/Tensors/Tree/Elab.lean

@@ -44,6 +44,10 @@ import HepLean.Tensors.ComplexLorentz.Basic
 - In all of theses expressions `μ`, `ν` etc are free. It does not matter what they are called,
  Lean will elaborate them in the same way. I.e. `{T | μ ν ⊗ T3 | μ ν }ᵀ` is exactly the same
  to Lean as `{T | α β ⊗ T3 | α β }ᵀ`.
+- Note that compared to ordinary index notation, we do not rise or lower the indices.
+  This is for two reasons: 1) It is difficult to make this general for all tensor species,
+  2) It is a reduency in ordinary index notation, since the tensor `T` itself already tells you
+  this information.
 
 -/
 open Lean