diff --git a/HepLean/Meta/Informal.lean b/HepLean/Meta/Informal.lean
index fd3de33..2147592 100644
--- a/HepLean/Meta/Informal.lean
+++ b/HepLean/Meta/Informal.lean
@@ -15,8 +15,6 @@ open Lean Elab System
 
 /-! TODO: Can likely make this a bona-fide command. -/
 
-/-! TODO: Add expected dependencies. -/
-
 /-- The structure representating an informal definition. -/
 structure InformalDefinition where
   /-- The name of the informal definition. This is autogenerated. -/
@@ -27,6 +25,8 @@ structure InformalDefinition where
   physics : String
   /-- References. -/
   ref : String
+  /-- The names of top-level commands we expect this definition to depend on. -/
+  dependencies : List Name
 
 /-- The structure representating an informal proof. -/
 structure InformalLemma where
@@ -40,6 +40,8 @@ structure InformalLemma where
   proof : String
   /-- References. -/
   ref : String
+  /-- The names of top-level commands we expect this lemma to depend on. -/
+  dependencies : List Name
 
 namespace Informal
 
@@ -49,6 +51,8 @@ declare_syntax_cat informalAssignment
 /-- The syntax describing an informal assignment of `ident` to a string. -/
 syntax (name := informalAssignment) ident ":≈" str : informalAssignment
 
+syntax (name := informalAssignmentDeps) ident ":≈" "[" sepBy(term, ",") "]" : informalAssignment
+
 /-- The syntax for the command informal_definition. -/
 syntax (name := informal_definition) "informal_definition " ident
   " where " (colGt informalAssignment)* : command
@@ -58,6 +62,7 @@ macro "informal_definition " name:ident " where " assignments:informalAssignment
   let mut math_def? : Option (TSyntax `term) := none
   let mut physics_def? : Option (TSyntax `term) := none
   let mut ref_def? : Option (TSyntax `term) := none
+  let mut dep_def? : Option (TSyntax `term) := none
   for assignment in assignments do
     match assignment with
     | `(informalAssignment| physics :≈ $val:str) =>
@@ -69,7 +74,9 @@ macro "informal_definition " name:ident " where " assignments:informalAssignment
     | `(informalAssignment| ref :≈ $val:str) =>
       let some strVal := val.raw.isStrLit? | Macro.throwError "Expected string literal for ref"
       ref_def? := some (← `($(Lean.quote strVal)))
-    | _ => Macro.throwError "invalid assignment syntax"
+    | `(informalAssignmentDeps| deps :≈ [ $deps,* ]) =>
+      dep_def? := some (← `([ $deps,* ]))
+    | _ => Macro.throwError "invalid assignment syntax in informal_definition"
   unless math_def?.isSome do
     Macro.throwError "A 'math' assignments is required"
   `(
@@ -78,7 +85,8 @@ def $name : InformalDefinition := {
   name := $(Lean.quote name.getId),
   physics := $(physics_def?.getD (← `("No physics description provided"))),
   math := $(math_def?.getD (panic! "math not assigned")),
-  ref := $(ref_def?.getD (← `("No references provided")))
+  ref := $(ref_def?.getD (← `("No references provided"))),
+  dependencies := $(dep_def?.getD (← `([])))
     })
 
 /-- The syntax for the command `informal_lemma`. -/
@@ -91,6 +99,7 @@ macro "informal_lemma " name:ident " where " assignments:informalAssignment* : c
   let mut physics_def? : Option (TSyntax `term) := none
   let mut proof_def? : Option (TSyntax `term) := none
   let mut ref_def? : Option (TSyntax `term) := none
+  let mut dep_def? : Option (TSyntax `term) := none
   for assignment in assignments do
     match assignment with
     | `(informalAssignment| physics :≈ $val:str) =>
@@ -105,6 +114,8 @@ macro "informal_lemma " name:ident " where " assignments:informalAssignment* : c
     | `(informalAssignment| ref :≈ $val:str) =>
       let some strVal := val.raw.isStrLit? | Macro.throwError "Expected string literal for ref"
       ref_def? := some (← `($(Lean.quote strVal)))
+    | `(informalAssignmentDeps| deps :≈ [ $deps,* ]) =>
+      dep_def? := some (← `([ $deps,* ]))
     | _ => Macro.throwError "invalid assignment syntax"
   unless math_def?.isSome do
     Macro.throwError "A 'math' assignments is required"
@@ -115,7 +126,8 @@ def $name : InformalLemma := {
   physics := $(physics_def?.getD (← `("No physics description provided"))),
   math := $(math_def?.getD (panic! "math not assigned")),
   proof := $(proof_def?.getD (← `("No proof description provided"))),
-  ref := $(ref_def?.getD (← `("No references provided")))
+  ref := $(ref_def?.getD (← `("No references provided"))),
+  dependencies := $(dep_def?.getD (← `([])))
     })
 
 end Informal
diff --git a/HepLean/SpaceTime/WeylFermion/Basic.lean b/HepLean/SpaceTime/WeylFermion/Basic.lean
index fc8f0fc..47c8f5b 100644
--- a/HepLean/SpaceTime/WeylFermion/Basic.lean
+++ b/HepLean/SpaceTime/WeylFermion/Basic.lean
@@ -39,14 +39,15 @@ informal_definition altRightHandedWeylFermion where
 ## Equivalences between Weyl fermion vector spaces.
 
 -/
-
 informal_definition leftHandedWeylFermionAltEquiv where
   math :≈ "The linear equiv between leftHandedWeylFermion and altLeftHandedWeylFermion given
     by multiplying an element of rightHandedWeylFermion by the matrix εᵃ⁰ᵃ¹ ={{0, 1}, {-1, 0}}."
+  deps :≈ [`leftHandedWeylFermion, `altLeftHandedWeylFermion]
 
 informal_lemma leftHandedWeylFermionAltEquiv_equivariant where
   math :≈ "The linear equiv leftHandedWeylFermionAltEquiv is equivariant with respect to the
     action of SL(2,C) on leftHandedWeylFermion and altLeftHandedWeylFermion."
+  deps :≈ [`leftHandedWeylFermionAltEquiv]
 
 informal_definition rightHandedWeylFermionAltEquiv where
   math :≈ "The linear equiv between rightHandedWeylFermion and altRightHandedWeylFermion given