diff --git a/.gitpod.yml b/.gitpod.yml
new file mode 100644
index 0000000..7789c01
--- /dev/null
+++ b/.gitpod.yml
@@ -0,0 +1,12 @@
+# This is run when starting a Gitpod workspace on this repository
+
+image: leanprovercommunity/gitpod4
+
+vscode:
+  extensions:
+    - leanprover.lean4 # install the Lean 4 VS Code extension
+
+tasks:
+  - init: |
+      elan self update
+      lake exe cache get
diff --git a/HepLean/Tensors/ComplexLorentz/Metrics/Basis.lean b/HepLean/Tensors/ComplexLorentz/Metrics/Basis.lean
index 37a1e14..a5096ad 100644
--- a/HepLean/Tensors/ComplexLorentz/Metrics/Basis.lean
+++ b/HepLean/Tensors/ComplexLorentz/Metrics/Basis.lean
@@ -52,6 +52,8 @@ lemma coMetric_basis_expand : {η' | μ ν}ᵀ.tensor =
       simp only [Fin.isValue, Lorentz.complexCoBasisFin4, Basis.coe_reindex, Function.comp_apply]
       rfl
 
+/-- Provides the explicit expansion of the co-metric tensor in terms of the basis elements, as
+a tensor tree.-/
 lemma coMetric_basis_expand_tree : {η' | μ ν}ᵀ.tensor =
     (TensorTree.add (tensorNode (basisVector ![Color.down, Color.down] (fun _ => 0))) <|
     TensorTree.add (smul (-1) (tensorNode (basisVector ![Color.down, Color.down] (fun _ => 1)))) <|