Tagged TODOs (#435)

* feat: Add tags

* feat: Add tags to YML

* refactor: Lint

PhysLean/ClassicalMechanics/HarmonicOscillator/Basic.lean

@@ -92,12 +92,12 @@ lemma lagrangian_parity (x : ℝ → ℝ) (hx : Differentiable ℝ x) :
   · fun_prop
   · exact hx t
 
-TODO "Derive the force from the lagrangian of the classical harmonic oscillator"
+TODO "6VZGU" "Derive the force from the lagrangian of the classical harmonic oscillator"
 
-TODO "Derive the Euler-Lagraange equation for the classical harmonic oscillator
+TODO "6VZG4" "Derive the Euler-Lagraange equation for the classical harmonic oscillator
   from the lagrangian."
 
-TODO "Include damping into the classical harmonic oscillator."
+TODO "6VZHC" "Include damping into the classical harmonic oscillator."
 
 end HarmonicOscillator
 

PhysLean/ClassicalMechanics/HarmonicOscillator/Solution.lean

@@ -31,7 +31,7 @@ structure InitialConditions where
   /-- The initial velocity of the harmonic oscillator. -/
   v₀ : ℝ
 
-TODO "Implement other initial conditions for the harmonic oscillator."
+TODO "6VZME" "Implement other initial conditions for the harmonic oscillator."
 
 @[ext]
 lemma InitialConditions.ext {IC₁ IC₂ : InitialConditions} (h1 : IC₁.x₀ = IC₂.x₀)
@@ -285,15 +285,16 @@ lemma sol_action (IC : InitialConditions) (t1 t2 : ℝ) :
       · field_simp
         ring
 
-TODO "For the classical harmonic oscillator find the time for which it returns to
+TODO "6VZI3" "For the classical harmonic oscillator find the time for which it returns to
   it's initial position and velocity."
 
-TODO "For the classical harmonic oscillator find the times for which it passes through zero."
+TODO "6VZJB" "For the classical harmonic oscillator find the times for
+  which it passes through zero."
 
-TODO "For the classical harmonic oscillator find the velocity when it passes through
+TODO "6VZJH" "For the classical harmonic oscillator find the velocity when it passes through
   zero."
 
-TODO "Show uniqueness of the solution for the classical harmonic oscillator."
+TODO "6VZJO" "Show uniqueness of the solution for the classical harmonic oscillator."
 
 end HarmonicOscillator
 

PhysLean/Electromagnetism/FieldStrength/Basic.lean

@@ -452,11 +452,11 @@ lemma fromElectricMagneticField_repr (EM : ElectricField × MagneticField) (y :
     fin_cases j <;>
     simp
 
-TODO "Define the dual field strength."
+TODO "6V2OU" "Define the dual field strength."
 
 end FieldStrength
 
-TODO "Show that the isomorphism between `ElectricField d × MagneticField d` and
+TODO "6V2O4" "Show that the isomorphism between `ElectricField d × MagneticField d` and
   `ElectricField d × MagneticField d` is equivariant with respect to the Lorentz group."
 
 end Electromagnetism

PhysLean/Electromagnetism/MaxwellEquations.lean

@@ -20,7 +20,8 @@ structure EMSystem where
   /-- The permittivity. -/
   ε₀ : ℝ
 
-TODO "Charge density and current desnity should be generalized to signed measures, in such a way
+TODO "6V2UZ" "Charge density and current desnity should be generalized to signed measures,
+  in such a way
   that they are still easy to work with and can be integrated with with tensor notation.
   See here:
   https://leanprover.zulipchat.com/#narrow/channel/479953-PhysLean/topic/Maxwell's.20Equations"
@@ -70,7 +71,7 @@ def MaxwellEquations (E : ElectricField) (B : MagneticField) : Prop :=
   GaussLawElectric 𝓔 ρ E ∧ GaussLawMagnetic B ∧
   FaradayLaw E B ∧ AmpereLaw 𝓔 J E B
 
-TODO "Show that if the charge density is spherically symmetric,
+TODO "6V2VD" "Show that if the charge density is spherically symmetric,
   then the electric field is also spherically symmetric."
 
 end Electromagnetism

PhysLean/Mathematics/LinearMaps.lean

@@ -14,7 +14,7 @@ Some definitions and properties of linear, bilinear, and trilinear maps, along w
 quadratic and cubic equations.
 
 -/
-TODO "Replace the definitions in this file with Mathlib definitions."
+TODO "6VZLZ" "Replace the definitions in this file with Mathlib definitions."
 
 /-- The structure defining a homogeneous quadratic equation. -/
 @[simp]

PhysLean/Meta/Informal/Basic.lean

@@ -19,11 +19,17 @@ Everything else about informal definitions and lemmas are in the `Informal.Post`
 structure InformalDefinition where
   /-- The names of top-level commands we expect this definition to depend on. -/
   deps : List Lean.Name
+  /-- The tag of the informal definition. This should be unique amongst informal results
+    and todo items. -/
+  tag : String
 
 /-- The structure representing an informal lemma. -/
 structure InformalLemma where
   /-- The names of top-level commands we expect this lemma to depend on. -/
   deps : List Lean.Name
+  /-- The tag of the informal lemma. This should be unique amongst informal results
+    and todo items. -/
+  tag : String
 
 namespace Informal
 

PhysLean/Meta/Informal/Post.lean

@@ -46,6 +46,17 @@ unsafe def constantInfoToInformalDefinition (c : ConstantInfo) : CoreM InformalD
   | _ => panic!
     "Passed constantInfoToInformalDefinition a `ConstantInfo` that is not a `InformalDefinition`"
 
+/-- Gets the tag associated with an informal definition or lemma. -/
+unsafe def getTag (c : ConstantInfo) : CoreM String := do
+  if isInformalLemma c then
+    let i ← constantInfoToInformalLemma c
+    return i.tag
+  else if isInformalDef c then
+    let i ← constantInfoToInformalDefinition c
+    return i.tag
+  else
+    panic! "getTag: Not an informal lemma or definition"
+
 end Informal
 
 namespace PhysLean
@@ -69,4 +80,5 @@ def AllInformal : CoreM (Array ConstantInfo) := do
   let y := x.flatten.filter fun c => Informal.isInformal c
   return y
 
+
 end PhysLean

PhysLean/Meta/TODO/Basic.lean

@@ -21,6 +21,8 @@ structure todoInfo where
   fileName : Name
   /-- The line from where the note came from. -/
   line : Nat
+  /-- The tag of the TODO item -/
+  tag : String
 
 /-- Environment extension to store `todo ...`. -/
 initialize todoExtension : SimplePersistentEnvExtension todoInfo (Array todoInfo) ←
@@ -31,14 +33,15 @@ initialize todoExtension : SimplePersistentEnvExtension todoInfo (Array todoInfo
   }
 
 /-- Syntax for the `TODO ...` command. -/
-syntax (name := todo_comment) "TODO " str : command
+syntax (name := todo_comment) "TODO " str str : command
 
 /-- Elaborator for the `TODO ...` command -/
 @[command_elab todo_comment]
 def elabTODO : Elab.Command.CommandElab := fun stx =>
   match stx with
-  | `(TODO $s) => do
+  | `(TODO $t $s) => do
     let str : String := s.getString
+    let tag : String := t.getString
     let pos := stx.getPos?
     match pos with
     | some pos => do
@@ -47,7 +50,7 @@ def elabTODO : Elab.Command.CommandElab := fun stx =>
       let filePos := fileMap.toPosition pos
       let line := filePos.line
       let modName := env.mainModule
-      let todoInfo : todoInfo := { content := str, fileName := modName, line := line }
+      let todoInfo : todoInfo := { content := str, fileName := modName, line := line, tag := tag }
       modifyEnv fun env => todoExtension.addEntry env todoInfo
     | none => throwError "Invalid syntax for `TODO` command"
   | _ => throwError "Invalid syntax for `TODO` command"

PhysLean/Meta/TransverseTactics.lean

@@ -75,8 +75,9 @@ def traverseForest (file : FilePath)
 
 end transverseTactics
 
-TODO "Find a way to free the environment `env` in `transverseTactics`.
+TODO "6VZEW" "Find a way to free the environment `env` in `transverseTactics`.
   This leads to memory problems when using `transverseTactics` directly in loops."
+
 open transverseTactics in
 /-- Applies `visitTacticInfo` to each tactic in a file. -/
 unsafe def transverseTactics (file : FilePath)

PhysLean/Particles/BeyondTheStandardModel/GeorgiGlashow/Basic.lean

@@ -20,6 +20,7 @@ namespace GeorgiGlashow
 /-- The gauge group of the Georgi-Glashow model, i.e., `SU(5)`. -/
 informal_definition GaugeGroupI where
   deps := []
+  tag := "6V2WM"
 
 /-- The homomorphism of the Standard Model gauge group into the Georgi-Glashow gauge group, i.e.,
 the group homomorphism `SU(3) × SU(2) × U(1) → SU(5)` taking `(h, g, α)` to
@@ -29,6 +30,7 @@ See page 34 of https://math.ucr.edu/home/baez/guts.pdf
 -/
 informal_definition inclSM where
   deps := [``GaugeGroupI, ``StandardModel.GaugeGroupI]
+  tag := "6V2WS"
 
 /-- The kernel of the map `inclSM` is equal to the subgroup `StandardModel.gaugeGroupℤ₆SubGroup`.
 
@@ -36,11 +38,13 @@ See page 34 of https://math.ucr.edu/home/baez/guts.pdf
 -/
 informal_lemma inclSM_ker where
   deps := [``inclSM, ``StandardModel.gaugeGroupℤ₆SubGroup]
+  tag := "6V2W2"
 
 /-- The group embedding from `StandardModel.GaugeGroupℤ₆` to `GaugeGroupI` induced by `inclSM` by
 quotienting by the kernel `inclSM_ker`.
 -/
 informal_definition embedSMℤ₆ where
   deps := [``inclSM, ``StandardModel.GaugeGroupℤ₆, ``GaugeGroupI, ``inclSM_ker]
+  tag := "6V2XA"
 
 end GeorgiGlashow

PhysLean/Particles/BeyondTheStandardModel/PatiSalam/Basic.lean

@@ -25,6 +25,7 @@ namespace PatiSalam
 /-- The gauge group of the Pati-Salam model (unquotiented by ℤ₂), i.e., `SU(4) × SU(2) × SU(2)`. -/
 informal_definition GaugeGroupI where
   deps := []
+  tag := "6V2Q2"
 
 /-- The homomorphism of the Standard Model gauge group into the Pati-Salam gauge group, i.e., the
 group homomorphism `SU(3) × SU(2) × U(1) → SU(4) × SU(2) × SU(2)` taking `(h, g, α)` to
@@ -34,6 +35,7 @@ See page 54 of https://math.ucr.edu/home/baez/guts.pdf
 -/
 informal_definition inclSM where
   deps := [``GaugeGroupI, ``StandardModel.GaugeGroupI]
+  tag := "6V2RH"
 
 /-- The kernel of the map `inclSM` is equal to the subgroup `StandardModel.gaugeGroupℤ₃SubGroup`.
 
@@ -41,16 +43,19 @@ See footnote 10 of https://arxiv.org/pdf/2201.07245
 -/
 informal_lemma inclSM_ker where
   deps := [``inclSM, ``StandardModel.gaugeGroupℤ₃SubGroup]
+  tag := "6V2RQ"
 
 /-- The group embedding from `StandardModel.GaugeGroupℤ₃` to `GaugeGroupI` induced by `inclSM` by
 quotienting by the kernel `inclSM_ker`.
 -/
 informal_definition embedSMℤ₃ where
   deps := [``inclSM, ``StandardModel.GaugeGroupℤ₃, ``GaugeGroupI, ``inclSM_ker]
+  tag := "6V2RY"
 
 /-- The equivalence between `GaugeGroupI` and `Spin(6) × Spin(4)`. -/
 informal_definition gaugeGroupISpinEquiv where
   deps := [``GaugeGroupI]
+  tag := "6V2R7"
 
 /-- The ℤ₂-subgroup of the un-quotiented gauge group which acts trivially on all particles in the
 standard model, i.e., the ℤ₂-subgroup of `GaugeGroupI` with the non-trivial element `(-1, -1, -1)`.
@@ -59,6 +64,7 @@ See https://math.ucr.edu/home/baez/guts.pdf
 -/
 informal_definition gaugeGroupℤ₂SubGroup where
   deps := [``GaugeGroupI]
+  tag := "6V2SG"
 
 /-- The gauge group of the Pati-Salam model with a ℤ₂ quotient, i.e., the quotient of `GaugeGroupI`
 by the ℤ₂-subgroup `gaugeGroupℤ₂SubGroup`.
@@ -67,17 +73,20 @@ See https://math.ucr.edu/home/baez/guts.pdf
 -/
 informal_definition GaugeGroupℤ₂ where
   deps := [``GaugeGroupI, ``gaugeGroupℤ₂SubGroup]
+  tag := "6V2SM"
 
 /-- The group `StandardModel.gaugeGroupℤ₆SubGroup` under the homomorphism `embedSM` factors through
 the subgroup `gaugeGroupℤ₂SubGroup`.
 -/
 informal_lemma sm_ℤ₆_factor_through_gaugeGroupℤ₂SubGroup where
   deps := [``inclSM, ``StandardModel.gaugeGroupℤ₆SubGroup, ``gaugeGroupℤ₂SubGroup]
+  tag := "6V2SV"
 
 /-- The group homomorphism from `StandardModel.GaugeGroupℤ₆` to `GaugeGroupℤ₂` induced by `embedSM`.
 -/
 informal_definition embedSMℤ₆Toℤ₂ where
   deps := [``inclSM, ``StandardModel.GaugeGroupℤ₆, ``GaugeGroupℤ₂,
     ``sm_ℤ₆_factor_through_gaugeGroupℤ₂SubGroup]
+  tag := "6V2S4"
 
 end PatiSalam

PhysLean/Particles/BeyondTheStandardModel/Spin10/Basic.lean

@@ -19,6 +19,7 @@ namespace Spin10Model
 /-- The gauge group of the Spin(10) model, i.e., the group `Spin(10)`. -/
 informal_definition GaugeGroupI where
   deps := []
+  tag := "6V2X7"
 
 /-- The inclusion of the Pati-Salam gauge group into Spin(10), i.e., the lift of the embedding
 `SO(6) × SO(4) → SO(10)` to universal covers, giving a homomorphism `Spin(6) × Spin(4) → Spin(10)`.
@@ -29,6 +30,7 @@ See page 56 of https://math.ucr.edu/home/baez/guts.pdf
 -/
 informal_definition inclPatiSalam where
   deps := [``GaugeGroupI, ``PatiSalam.GaugeGroupI, ``PatiSalam.gaugeGroupISpinEquiv]
+  tag := "6V2YG"
 
 /-- The inclusion of the Standard Model gauge group into Spin(10), i.e., the composition of
 `embedPatiSalam` and `PatiSalam.inclSM`.
@@ -37,21 +39,25 @@ See page 56 of https://math.ucr.edu/home/baez/guts.pdf
 -/
 informal_definition inclSM where
   deps := [``inclPatiSalam, ``PatiSalam.inclSM]
+  tag := "6V2YO"
 
 /-- The inclusion of the Georgi-Glashow gauge group into Spin(10), i.e., the Lie group homomorphism
 from `SU(n) → Spin(2n)` discussed on page 46 of https://math.ucr.edu/home/baez/guts.pdf for `n = 5`.
 -/
 informal_definition inclGeorgiGlashow where
   deps := [``GaugeGroupI, ``GeorgiGlashow.GaugeGroupI]
+  tag := "6V2YU"
 
 /-- The inclusion of the Standard Model gauge group into Spin(10), i.e., the composition of
 `inclGeorgiGlashow` and `GeorgiGlashow.inclSM`.
 -/
 informal_definition inclSMThruGeorgiGlashow where
   deps := [``inclGeorgiGlashow, ``GeorgiGlashow.inclSM]
+  tag := "6V2YZ"
 
 /-- The inclusion `inclSM` is equal to the inclusion `inclSMThruGeorgiGlashow`. -/
 informal_lemma inclSM_eq_inclSMThruGeorgiGlashow where
   deps := [``inclSM, ``inclSMThruGeorgiGlashow]
+  tag := "6V2Y6"
 
 end Spin10Model

PhysLean/Particles/BeyondTheStandardModel/TwoHDM/Basic.lean

@@ -22,7 +22,7 @@ open HiggsField
 
 noncomputable section
 
-TODO "Within the definition of the 2HDM potential. The structure `Potential` should be
+TODO "6V2TZ" "Within the definition of the 2HDM potential. The structure `Potential` should be
   renamed to TwoHDM and moved out of the TwoHDM namespace.
   Then `toFun` should be renamed to `potential`."
 
@@ -148,7 +148,7 @@ lemma left_eq_neg_right : P.toFun Φ1 (- Φ1) =
 
 -/
 
-TODO "Prove bounded properties of the 2HDM potential.
+TODO "6V2UD" "Prove bounded properties of the 2HDM potential.
   See e.g. https://inspirehep.net/literature/201299 and
   https://arxiv.org/pdf/hep-ph/0605184."
 

PhysLean/Particles/BeyondTheStandardModel/TwoHDM/GaugeOrbits.lean

@@ -87,6 +87,7 @@ lemma prodMatrix_smooth (Φ1 Φ2 : HiggsField) :
 Higgs fields. -/
 informal_lemma prodMatrix_invariant where
   deps := [``prodMatrix, ``gaugeAction]
+  tag := "6V2VS"
 
 /-- Given any smooth map `f` from spacetime to 2-by-2 complex matrices landing on positive
 semi-definite matrices, there exist smooth Higgs fields `Φ1` and `Φ2` such that `f` is equal to
@@ -96,6 +97,7 @@ See https://arxiv.org/pdf/hep-ph/0605184
 -/
 informal_lemma prodMatrix_to_higgsField where
   deps := [``prodMatrix, ``HiggsField, ``prodMatrix_smooth]
+  tag := "6V2V2"
 
 end
 end TwoHDM

PhysLean/Particles/StandardModel/Basic.lean

@@ -12,7 +12,7 @@ import PhysLean.Meta.Informal.Basic
 This file defines the basic properties of the standard model in particle physics.
 
 -/
-TODO "Redefine the gauge group as a quotient of SU(3) x SU(2) x U(1) by a subgroup of ℤ₆."
+TODO "6V2FP" "Redefine the gauge group as a quotient of SU(3) x SU(2) x U(1) by a subgroup of ℤ₆."
 universe v u
 namespace StandardModel
 
@@ -34,6 +34,7 @@ See https://math.ucr.edu/home/baez/guts.pdf
 -/
 informal_definition gaugeGroupℤ₆SubGroup where
   deps := [``GaugeGroupI]
+  tag := "6V2FZ"
 
 /-- The smallest possible gauge group of the Standard Model, i.e., the quotient of `GaugeGroupI` by
 the ℤ₆-subgroup `gaugeGroupℤ₆SubGroup`.
@@ -42,6 +43,7 @@ See https://math.ucr.edu/home/baez/guts.pdf
 -/
 informal_definition GaugeGroupℤ₆ where
   deps := [``GaugeGroupI, ``StandardModel.gaugeGroupℤ₆SubGroup]
+  tag := "6V2GA"
 
 /-- The ℤ₂subgroup of the un-quotiented gauge group which acts trivially on all particles in the
 standard model, i.e., the ℤ₂-subgroup of `GaugeGroupI` derived from the ℤ₂ subgroup of
@@ -51,6 +53,7 @@ See https://math.ucr.edu/home/baez/guts.pdf
 -/
 informal_definition gaugeGroupℤ₂SubGroup where
   deps := [``GaugeGroupI, ``StandardModel.gaugeGroupℤ₆SubGroup]
+  tag := "6V2GH"
 
 /-- The gauge group of the Standard Model with a ℤ₂ quotient, i.e., the quotient of `GaugeGroupI` by
 the ℤ₂-subgroup `gaugeGroupℤ₂SubGroup`.
@@ -59,6 +62,7 @@ See https://math.ucr.edu/home/baez/guts.pdf
 -/
 informal_definition GaugeGroupℤ₂ where
   deps := [``GaugeGroupI, ``StandardModel.gaugeGroupℤ₂SubGroup]
+  tag := "6V2GO"
 
 /-- The ℤ₃-subgroup of the un-quotiented gauge group which acts trivially on all particles in the
 standard model, i.e., the ℤ₃-subgroup of `GaugeGroupI` derived from the ℤ₃ subgroup of
@@ -68,6 +72,7 @@ See https://math.ucr.edu/home/baez/guts.pdf
 -/
 informal_definition gaugeGroupℤ₃SubGroup where
   deps := [``GaugeGroupI, ``StandardModel.gaugeGroupℤ₆SubGroup]
+  tag := "6V2GV"
 
 /-- The gauge group of the Standard Model with a ℤ₃-quotient, i.e., the quotient of `GaugeGroupI` by
 the ℤ₃-subgroup `gaugeGroupℤ₃SubGroup`.
@@ -76,6 +81,7 @@ See https://math.ucr.edu/home/baez/guts.pdf
 -/
 informal_definition GaugeGroupℤ₃ where
   deps := [``GaugeGroupI, ``StandardModel.gaugeGroupℤ₃SubGroup]
+  tag := "6V2G3"
 
 /-- Specifies the allowed quotients of `SU(3) x SU(2) x U(1)` which give a valid
   gauge group of the Standard Model. -/
@@ -101,6 +107,7 @@ See https://math.ucr.edu/home/baez/guts.pdf
 informal_definition GaugeGroup where
   deps := [``GaugeGroupI, ``gaugeGroupℤ₆SubGroup, ``gaugeGroupℤ₂SubGroup, ``gaugeGroupℤ₃SubGroup,
     ``GaugeGroupQuot]
+  tag := "6V2HF"
 
 /-!
 
@@ -111,17 +118,21 @@ informal_definition GaugeGroup where
 /-- The gauge group `GaugeGroupI` is a Lie group. -/
 informal_lemma gaugeGroupI_lie where
   deps := [``GaugeGroupI]
+  tag := "6V2HL"
 
 /-- For every `q` in `GaugeGroupQuot` the group `GaugeGroup q` is a Lie group. -/
 informal_lemma gaugeGroup_lie where
   deps := [``GaugeGroup]
+  tag := "6V2HR"
 
 /-- The trivial principal bundle over SpaceTime with structure group `GaugeGroupI`. -/
 informal_definition gaugeBundleI where
   deps := [``GaugeGroupI, ``SpaceTime]
+  tag := "6V2HX"
 
 /-- A global section of `gaugeBundleI`. -/
 informal_definition gaugeTransformI where
   deps := [``gaugeBundleI]
+  tag := "6V2H5"
 
 end StandardModel

PhysLean/Particles/StandardModel/HiggsBoson/Basic.lean

@@ -78,7 +78,7 @@ end HiggsVec
 We also define the Higgs bundle.
 -/
 
-TODO "Make `HiggsBundle` an associated bundle."
+TODO "6V2IS" "Make `HiggsBundle` an associated bundle."
 
 /-- The `HiggsBundle` is defined as the trivial vector bundle with base `SpaceTime` and
   fiber `HiggsVec`. Thus as a manifold it corresponds to `ℝ⁴ × ℂ²`. -/
@@ -181,6 +181,7 @@ defined by `ofReal 0` is the constant zero-section of the bundle `HiggsBundle`.
 -/
 informal_lemma zero_is_zero_section where
   deps := [`StandardModel.HiggsField.zero]
+  tag := "6V2I5"
 
 end HiggsField
 

PhysLean/Particles/StandardModel/HiggsBoson/GaugeAction.lean

@@ -11,7 +11,7 @@ import PhysLean.Particles.StandardModel.Representations
 # The action of the gauge group on the Higgs field
 
 -/
-TODO "Currently this only contains the action of the global gauge group. Generalize
+TODO "6V2LJ" "Currently this only contains the action of the global gauge group. Generalize
   to include the full action of the gauge group."
 noncomputable section
 
@@ -218,6 +218,7 @@ theorem rotate_fst_real_snd_zero (φ : HiggsVec) :
 /-- There exists a `g` in `GaugeGroupI` such that `rep g φ = φ'` iff `‖φ‖ = ‖φ'‖`. -/
 informal_lemma guage_orbit where
   deps := [``rotate_fst_zero_snd_real]
+  tag := "6V2L2"
 
 /-- The Higgs boson breaks electroweak symmetry down to the electromagnetic force, i.e., the
 stability group of the action of `rep` on `![0, Complex.ofReal ‖φ‖]`, for non-zero `‖φ‖`, is the
@@ -226,6 +227,7 @@ stability group of the action of `rep` on `![0, Complex.ofReal ‖φ‖]`, for n
 -/
 informal_lemma stability_group_single where
   deps := [``StandardModel.HiggsVec, ``StandardModel.HiggsVec.rep]
+  tag := "6V2MD"
 
 /-- The subgroup of `gaugeGroup := SU(3) × SU(2) × U(1)` which preserves every `HiggsVec` by the
 action of `StandardModel.HiggsVec.rep` is given by `SU(3) × ℤ₆` where `ℤ₆` is the subgroup of
@@ -233,12 +235,13 @@ action of `StandardModel.HiggsVec.rep` is given by `SU(3) × ℤ₆` where `ℤ
 -/
 informal_lemma stability_group where
   deps := [``HiggsVec, ``rep]
+  tag := "6V2MO"
 
 end HiggsVec
 
-TODO "Define the global gauge action on HiggsField."
-TODO "Prove `⟪φ1, φ2⟫_H` invariant under the global gauge action. (norm_map_of_mem_unitary)"
-TODO "Prove invariance of potential under global gauge action."
+TODO "6V2MV" "Define the global gauge action on HiggsField."
+TODO "6V2M3" "Prove `⟪φ1, φ2⟫_H` invariant under the global gauge action. (norm_map_of_mem_unitary)"
+TODO  "6V2NA" "Prove invariance of potential under global gauge action."
 
 namespace HiggsField
 
@@ -251,18 +254,21 @@ namespace HiggsField
 /-- The action of `gaugeTransformI` on `HiggsField` acting pointwise through `HiggsVec.rep`. -/
 informal_definition gaugeAction where
   deps := [``HiggsVec.rep, ``gaugeTransformI]
+  tag := "6V2NP"
 
 /-- There exists a `g` in `gaugeTransformI` such that `gaugeAction g φ = φ'` iff
 `φ(x)^† φ(x) = φ'(x)^† φ'(x)`.
 -/
 informal_lemma guage_orbit where
   deps := [``gaugeAction]
+  tag := "6V2NX"
 
 /-- For every smooth map `f` from `SpaceTime` to `ℝ` such that `f` is positive semidefinite, there
 exists a Higgs field `φ` such that `f = φ^† φ`.
 -/
 informal_lemma gauge_orbit_surject where
   deps := [``HiggsField, ``SpaceTime]
+  tag := "6V2OC"
 
 end HiggsField
 

PhysLean/Particles/StandardModel/HiggsBoson/Potential.lean

@@ -362,6 +362,7 @@ non-positive, i.e., for `P : Potential` then `P.IsBounded` iff `P.μ2 ≤ 0`. Th
 `- P.μ2 * ‖φ‖_H^2 x` is bounded below iff `P.μ2 ≤ 0`. -/
 informal_lemma isBounded_iff_of_𝓵_zero where
   deps := [`StandardModel.HiggsField.Potential.IsBounded, `StandardModel.HiggsField.Potential]
+  tag := "6V2K5"
 
 /-!
 

PhysLean/QFT/AnomalyCancellation/Basic.lean

@@ -14,10 +14,10 @@ This file defines the basic structures for the anomaly cancellation conditions.
 It defines a module structure on the charges, and the solutions to the linear ACCs.
 
 -/
-TODO "Anomaly cancellation conditions can be derived formally from the gauge group
+TODO "6VZMW" "Anomaly cancellation conditions can be derived formally from the gauge group
   and fermionic representations using e.g. topological invariants. Include such a
   definition."
-TODO "Anomaly cancellation conditions can be defined using algebraic varieties.
+TODO "6VZM3" "Anomaly cancellation conditions can be defined using algebraic varieties.
   Link such an approach to the approach here."
 
 /-- A system of charges, specified by the number of charges. -/

PhysLean/QFT/AnomalyCancellation/PureU1/BasisLinear.lean

@@ -75,7 +75,7 @@ lemma sum_of_vectors {n : ℕ} (f : Fin k → (PureU1 n).LinSols) (j : Fin n) :
     (∑ i : Fin k, (f i)).1 j = (∑ i : Fin k, (f i).1 j) :=
   sum_of_anomaly_free_linear (fun i => f i) j
 
-TODO "The definition of `coordinateMap` here may be improved by replacing
+TODO "6VZO6" "The definition of `coordinateMap` here may be improved by replacing
   `Finsupp.equivFunOnFinite` with `Finsupp.linearEquivFunOnFinite`. Investigate this."
 /-- The coordinate map for the basis. -/
 noncomputable

PhysLean/QFT/AnomalyCancellation/PureU1/Even/BasisLinear.lean

@@ -621,7 +621,7 @@ lemma Pa'_eq (f f' : (Fin n.succ) ⊕ (Fin n) → ℚ) : Pa' f = Pa' f' ↔ f =
     linarith
   · rw [h]
 
-TODO "Replace the definition of `join` with a Mathlib definition, most likely `Sum.elim`."
+TODO "6VZTB" "Replace the definition of `join` with a Mathlib definition, most likely `Sum.elim`."
 /-- A helper function for what follows. -/
 def join (g : Fin n.succ → ℚ) (f : Fin n → ℚ) : (Fin n.succ) ⊕ (Fin n) → ℚ := fun i =>
   match i with

PhysLean/QFT/AnomalyCancellation/PureU1/Odd/BasisLinear.lean

@@ -628,7 +628,7 @@ lemma Pa'_eq (f f' : (Fin n.succ) ⊕ (Fin n.succ) → ℚ) : Pa' f = Pa' f' ↔
     linarith
   · rw [h]
 
-TODO "Replace the definition of `join` with a Mathlib definition, most likely `Sum.elim`."
+TODO "6VZRN" "Replace the definition of `join` with a Mathlib definition, most likely `Sum.elim`."
 /-- A helper function for what follows. -/
 def join (g f : Fin n → ℚ) : Fin n ⊕ Fin n → ℚ := fun i =>
   match i with

PhysLean/QFT/AnomalyCancellation/PureU1/Permutations.lean

@@ -89,7 +89,7 @@ lemma FamilyPermutations_anomalyFreeLinear_apply (S : (PureU1 n).LinSols)
     ((FamilyPermutations n).linSolRep f S).val i = S.val (f.invFun i) := by
   rfl
 
-TODO "Remove `pairSwap`, and use the Mathlib defined function `Equiv.swap` instead."
+TODO "6VZPL" "Remove `pairSwap`, and use the Mathlib defined function `Equiv.swap` instead."
 /-- The permutation which swaps i and j. -/
 def pairSwap {n : ℕ} (i j : Fin n) : (FamilyPermutations n).group where
   toFun s :=

PhysLean/QFT/PerturbationTheory/FieldOpFreeAlgebra/NormalOrder.lean

@@ -397,7 +397,7 @@ lemma normalOrderF_ofFieldOpF_mul_ofFieldOpF (φ φ' : 𝓕.FieldOp) :
 
 -/
 
-TODO "Split the following two lemmas up into smaller parts."
+TODO "6V2JJ" "Split the following two lemmas up into smaller parts."
 
 lemma normalOrderF_superCommuteF_ofCrAnListF_create_create_ofCrAnListF
     (φc φc' : 𝓕.CrAnFieldOp) (hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create)

PhysLean/QuantumMechanics/FiniteTarget/Basic.lean

@@ -43,7 +43,7 @@ noncomputable def timeEvolution (A : FiniteTarget n hℏ) (t : ℝ) : A.V →ₗ
   (LinearMap.toMatrix (Pi.basisFun ℂ (Fin n)) (Pi.basisFun ℂ (Fin n))).symm
   (timeEvolutionMatrix A t)
 
-TODO "Define a smooth structure on `FiniteTarget`."
+TODO "6VZGG" "Define a smooth structure on `FiniteTarget`."
 
 end FiniteTarget
 

PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Basic.lean

@@ -142,7 +142,7 @@ lemma one_over_ξ_sq : (1/Q.ξ)^2 = Q.m * Q.ω / Q.ℏ := by
   rw [one_over_ξ]
   refine Real.sq_sqrt (le_of_lt Q.m_mul_ω_div_ℏ_pos)
 
-TODO "The momentum operator should be moved to a more general file."
+TODO "6VZH3" "The momentum operator should be moved to a more general file."
 
 /-- The momentum operator is defined as the map from `ℝ → ℂ` to `ℝ → ℂ` taking
   `ψ` to `- i ℏ ψ'`.

PhysLean/Relativity/Lorentz/Algebra/Basis.lean

@@ -16,4 +16,4 @@ This file is waiting for Lorentz Tensors to be done formally, before
 it can be completed.
 
 -/
-TODO "Define the standard basis of the Lorentz algebra."
+TODO "6VZKA" "Define the standard basis of the Lorentz algebra."

PhysLean/Relativity/Lorentz/Bispinors/Basic.lean

@@ -87,6 +87,7 @@ Proof: expand `contrBispinorDown` and use fact that metrics contract to the iden
 -/
 informal_lemma contrBispinorUp_eq_metric_contr_contrBispinorDown where
   deps := [``contrBispinorUp, ``contrBispinorDown, ``leftMetric, ``rightMetric]
+  tag := "6V2PV"
 
 /-- `{coBispinorUp p | α β = εL | α α' ⊗ εR | β β'⊗ coBispinorDown p | α' β' }ᵀ`.
 
@@ -94,6 +95,7 @@ proof: expand `coBispinorDown` and use fact that metrics contract to the identit
 -/
 informal_lemma coBispinorUp_eq_metric_contr_coBispinorDown where
   deps := [``coBispinorUp, ``coBispinorDown, ``leftMetric, ``rightMetric]
+  tag := "6V2P6"
 
 lemma contrBispinorDown_expand (p : ℂT[.up]) :
     {contrBispinorDown p | α β}ᵀ.tensor =

PhysLean/Relativity/Lorentz/ComplexTensor/Basic.lean

@@ -293,7 +293,7 @@ instance {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
     Decidable (σ = σ') :=
   decidable_of_iff _ (OverColor.Hom.ext_iff σ σ')
 
-TODO "The lemma `repDim_τ` should hold for any Tensor Species not just complex Lorentz
+TODO "6V2BK" "The lemma `repDim_τ` should hold for any Tensor Species not just complex Lorentz
   tensors."
 @[simp]
 lemma repDim_τ {c : complexLorentzTensor.C} :

PhysLean/Relativity/Lorentz/ComplexTensor/Basis.lean

@@ -32,7 +32,7 @@ open Fermion
 noncomputable section
 namespace complexLorentzTensor
 
-TODO "Replace basisVector in this file with TensorSpecies.tensorBasis.
+TODO "6V2C5" "Replace basisVector in this file with TensorSpecies.tensorBasis.
   All of the results here should be generalized to TensorSpecies.tensorBasis."
 
 /-- Basis vectors for complex Lorentz tensors. -/

PhysLean/Relativity/Lorentz/Group/Basic.lean

@@ -15,7 +15,7 @@ We define the Lorentz group.
 - http://home.ku.edu.tr/~amostafazadeh/phys517_518/phys517_2016f/Handouts/A_Jaffi_Lorentz_Group.pdf
 
 -/
-TODO "Define the Lie group structure on the Lorentz group."
+TODO "6VZHM" "Define the Lie group structure on the Lorentz group."
 
 noncomputable section
 

PhysLean/Relativity/Lorentz/Group/Boosts/Generalized.lean

@@ -203,13 +203,13 @@ lemma toMatrix_in_lorentzGroup (u v : FuturePointing d) : (toMatrix u v) ∈ Lor
   refine hn _ ?_ h1
   simpa using (FuturePointing.one_add_metric_non_zero u v)
 
-TODO "Make `toLorentz` the definition of a generalised boost. This will involve
+TODO "6VZKM" "Make `toLorentz` the definition of a generalised boost. This will involve
   refactoring this file."
 /-- A generalised boost as an element of the Lorentz Group. -/
 def toLorentz (u v : FuturePointing d) : LorentzGroup d :=
   ⟨toMatrix u v, toMatrix_in_lorentzGroup u v⟩
 
-TODO "Show that generalised boosts are in the restricted Lorentz group."
+TODO "6VZKU" "Show that generalised boosts are in the restricted Lorentz group."
 
 lemma toLorentz_continuous (u : FuturePointing d) : Continuous (toLorentz u) := by
   refine Continuous.subtype_mk ?_ (fun x => toMatrix_in_lorentzGroup u x)

PhysLean/Relativity/Lorentz/Group/Orthochronous.lean

@@ -12,7 +12,7 @@ We define the give a series of lemmas related to the orthochronous property of l
 matrices.
 
 -/
-TODO "Prove topological properties of the Orthochronous Lorentz Group."
+TODO "6VZLO" "Prove topological properties of the Orthochronous Lorentz Group."
 
 noncomputable section
 

PhysLean/Relativity/Lorentz/Group/Restricted.lean

@@ -11,10 +11,10 @@ import PhysLean.Meta.Informal.Basic
 This file is currently a stub.
 
 -/
-TODO "Add definition of the restricted Lorentz group."
-TODO "Prove that every member of the restricted Lorentz group is
+TODO "6VZNK" "Add definition of the restricted Lorentz group."
+TODO "6VZNP" "Prove that every member of the restricted Lorentz group is
   combiniation of a boost and a rotation."
-TODO "Prove restricted Lorentz group equivalent to connected component of identity
+TODO "6VZNU" "Prove restricted Lorentz group equivalent to connected component of identity
   of the Lorentz group."
 
 namespace LorentzGroup
@@ -22,5 +22,6 @@ namespace LorentzGroup
 /-- The subgroup of the Lorentz group consisting of elements which are proper and orthochronous. -/
 informal_definition Restricted where
   deps := [``LorentzGroup, ``IsProper, ``IsOrthochronous]
+  tag := "6VZN7"
 
 end LorentzGroup

PhysLean/Relativity/Lorentz/Group/Rotations.lean

@@ -11,7 +11,7 @@ import PhysLean.Mathematics.SO3.Basic
 This file describes the embedding of `SO(3)` into `LorentzGroup 3`.
 
 -/
-TODO "Generalize the inclusion of rotations into LorentzGroup to arbitrary dimension."
+TODO "6VZIS" "Generalize the inclusion of rotations into LorentzGroup to arbitrary dimension."
 noncomputable section
 
 namespace LorentzGroup

PhysLean/Relativity/Lorentz/RealTensor/Derivative.lean

@@ -70,7 +70,7 @@ lemma derivative_repr {d n m : ℕ} {cm : Fin m → (realLorentzTensor d).C}
   · rw [← differentiableAt_pi]
     exact h1
 
-TODO "Prove that the derivative obeys the following equivariant
+TODO "6V2CQ" "Prove that the derivative obeys the following equivariant
   property with respect to the Lorentz group.
   For a function `f : ℝT(d, cm) → ℝT(d, cn)` then
   `Λ • (∂ f (x)) = ∂ (fun x => Λ • f (Λ⁻¹ • x)) (Λ • x)`."

PhysLean/Relativity/Lorentz/SL2C/Basic.lean

@@ -311,8 +311,9 @@ lemma toLorentzGroup_det_one (M : SL(2, ℂ)) : det (toLorentzGroup M).val = 1 :
 informal_lemma toRestrictedLorentzGroup where
   deps := [``toLorentzGroup, ``toLorentzGroup_det_one, ``toLorentzGroup_isOrthochronous,
     ``LorentzGroup.Restricted]
+  tag := "6VZP6"
 
-TODO "Define homomorphism from `SL(2, ℂ)` to the restricted Lorentz group."
+TODO "6VZQF" "Define homomorphism from `SL(2, ℂ)` to the restricted Lorentz group."
 end
 end SL2C
 

PhysLean/Relativity/Lorentz/Weyl/Basic.lean

@@ -289,12 +289,14 @@ an element of `rightHandedWeyl` by the matrix `εᵃ⁰ᵃ¹ = !![0, 1; -1, 0]]`
 -/
 informal_definition rightHandedWeylAltEquiv where
   deps := [``rightHanded, ``altRightHanded]
+  tag := "6VZR4"
 
 /-- The linear equivalence `rightHandedWeylAltEquiv` is equivariant with respect to the action of
 `SL(2,C)` on `rightHandedWeyl` and `altRightHandedWeyl`.
 -/
 informal_lemma rightHandedWeylAltEquiv_equivariant where
   deps := [``rightHandedWeylAltEquiv]
+  tag := "6VZSG"
 
 end
 

PhysLean/Relativity/SpaceTime/Basic.lean

@@ -17,7 +17,7 @@ abbrev Space (d : ℕ := 3) := EuclideanSpace ℝ (Fin d)
 
 noncomputable section
 
-TODO "SpaceTime should be refactored into a structure, or similar, to prevent casting."
+TODO "6V2DR" "SpaceTime should be refactored into a structure, or similar, to prevent casting."
 
 /-- The space-time -/
 abbrev SpaceTime (d : ℕ := 3) := Lorentz.Vector d

PhysLean/Relativity/SpaceTime/CliffordAlgebra.lean

@@ -11,7 +11,7 @@ import PhysLean.Meta.TODO.Basic
 This file defines the Gamma matrices.
 
 -/
-TODO "Prove algebra generated by gamma matrices is isomorphic to Clifford algebra."
+TODO "6VZF2" "Prove algebra generated by gamma matrices is isomorphic to Clifford algebra."
 namespace spaceTime
 open Complex
 

PhysLean/Relativity/Special/TwinParadox/Basic.lean

@@ -47,7 +47,7 @@ def properTimeTwinB : ℝ := SpaceTime.properTime T.startPoint T.twinBMid +
 /-- The proper time of twin A minus the proper time of twin B. -/
 def ageGap : ℝ := T.properTimeTwinA - T.properTimeTwinB
 
-TODO "Find the conditions for which the age gap for the twin paradox is zero."
+TODO "6V2UQ" "Find the conditions for which the age gap for the twin paradox is zero."
 
 /-!
 

PhysLean/Relativity/Tensors/OverColor/Discrete.lean

@@ -166,7 +166,6 @@ lemma pairIsoSep_inv_tprod {c1 c2 : C} (fx : (i : (𝟭 Type).obj (OverColor.mk
 
 open PhysLean.Fin
 
-TODO "Find a better place for this."
 lemma pairIsoSep_β_perm_cond (c1 c2 : C) : ∀ (x : Fin (Nat.succ 0).succ), ![c2, c1] x =
     (![c1, c2] ∘ ⇑(finMapToEquiv ![1, 0] ![1, 0]).symm) x:= by
   intro x

PhysLean/Relativity/Tensors/OverColor/Iso.lean

@@ -90,8 +90,8 @@ lemma equivToIso_mkIso_inv {c1 c2 : X → C} (h : c1 = c2) :
     Hom.toEquiv (mkIso h).inv = Equiv.refl _ := by
   rfl
 
-TODO "In equivToHomEq the tactic `try {simp; decide}; try decide` can probably be made more
-  efficent."
+TODO "6VZTR" "In the definition equivToHomEq the tactic `try {simp; decide}; try decide`
+  can probably be made more efficent."
 
 /-- The morphism from `mk c` to `mk c1` obtained by an equivalence and
   an equality lemma. -/

PhysLean/Relativity/Tensors/OverColor/Lift.lean

@@ -928,6 +928,7 @@ lemma forgetLiftAppCon_naturality_eqToHom_apply (c c1 : C) (h : c = c1)
 -/
 informal_definition forgetLift where
   deps := [``forget, ``lift]
+  tag := "6VZWS"
 
 end
 end OverColor

PhysLean/Relativity/Tensors/TensorSpecies/Contractions/Basic.lean

@@ -56,11 +56,13 @@ unit in the tensor species.
 -/
 informal_lemma contractSelfField_non_degenerate where
   deps := [``contractSelfField]
+  tag := "6V2TI"
 
 /-- The contraction `⟪ψ, φ⟫ₜₛ` is related to the tensor tree
 `{ψ | μ ⊗ (S.dualRepIsoDiscrete c).hom φ | μ}ᵀ`. -/
 informal_lemma contractSelfField_tensorTree where
   deps := [``contractSelfField, ``TensorTree]
+  tag := "6V2TO"
 
 /-!
 

PhysLean/Relativity/Tensors/TensorSpecies/DualRepIso.lean

@@ -249,22 +249,27 @@ the `i`-th component of the color.
 -/
 informal_definition dualRepIso where
   deps := [``dualRepIsoDiscrete]
+  tag := "6V2D6"
 
 /-- Acting with `dualRepIso` on the fst component of a `unitTensor` returns a metric. -/
 informal_lemma dualRepIso_unitTensor_fst where
   deps := [``dualRepIso, ``unitTensor, ``metricTensor]
+  tag := "6V2EG"
 
 /-- Acting with `dualRepIso` on the snd component of a `unitTensor` returns a metric. -/
 informal_lemma dualRepIso_unitTensor_snd where
   deps := [``dualRepIso, ``unitTensor, ``metricTensor]
+  tag := "6V2EN"
 
 /-- Acting with `dualRepIso` on the fst component of a `metricTensor` returns a unitTensor. -/
 informal_lemma dualRepIso_metricTensor_fst where
   deps := [``dualRepIso, ``unitTensor, ``metricTensor]
+  tag := "6V2EV"
 
 /-- Acting with `dualRepIso` on the snd component of a `metricTensor` returns a unitTensor. -/
 informal_lemma dualRepIso_metricTensor_snd where
   deps := [``dualRepIso, ``unitTensor, ``metricTensor]
+  tag := "6V2E4"
 
 end TensorSpecies
 

PhysLean/Relativity/Tensors/TensorSpecies/Tensor/Basic.lean

@@ -510,7 +510,7 @@ lemma PermCond.comp {n n1 n2 : ℕ} {c : Fin n → S.C} {c1 : Fin n1 → S.C}
     simp only [Function.comp_apply]
     rw [h.2, h2.2]
 
-TODO "Prove that if `σ` satifies `PermCond c c1 σ` then `PermCond.inv σ h`
+TODO "6VZ3C" "Prove that if `σ` satifies `PermCond c c1 σ` then `PermCond.inv σ h`
   satifies `PermCond c1 c (PermCond.inv σ h)`."
 
 lemma fin_cast_permCond (n n1 : ℕ) {c : Fin n → S.C} (h : n1 = n) :
@@ -624,7 +624,7 @@ And its interaction with
 
 -/
 
-TODO "Change products of tensors to use `Fin.append` rather then
+TODO "6VZ3N" "Change products of tensors to use `Fin.append` rather then
   `Sum.elim c c1 ∘ ⇑finSumFinEquiv.symm`."
 
 /-- The equivalence between `ComponentIdx (Sum.elim c c1 ∘ ⇑finSumFinEquiv.symm)` and
@@ -739,7 +739,7 @@ noncomputable def prodEquiv {n1 n2} {c : Fin n1 → S.C} {c1 : Fin n2 → S.C} :
     S.F.obj (OverColor.mk (Sum.elim c c1)) ≃ₗ[k] S.Tensor (Sum.elim c c1 ∘ ⇑finSumFinEquiv.symm) :=
   ((Action.forget _ _).mapIso (S.F.mapIso (OverColor.equivToIso finSumFinEquiv))).toLinearEquiv
 
-TODO "Determine in `prodEquiv_symm_pure` why in `rw (transparency := .instances) [h1]`
+TODO "6VZ3U" "Determine in `prodEquiv_symm_pure` why in `rw (transparency := .instances) [h1]`
   `(transparency := .instances)` is needed. As a first step adding this as a comment here."
 
 lemma prodEquiv_symm_pure {n1 n2} {c : Fin n1 → S.C} {c1 : Fin n2 → S.C}

PhysLean/Relativity/Tensors/TensorSpecies/Tensor/Contraction.lean

@@ -350,7 +350,7 @@ lemma dropPair_update_dropPairEmb {n : ℕ} [inst : DecidableEq (Fin (n + 1 +1))
     · simp [h]
     · simp [h]
 
-TODO "Prove lemmas relating to the commutation rules of `dropPair` and `prodP`."
+TODO "6VZ6V" "Prove lemmas relating to the commutation rules of `dropPair` and `prodP`."
 
 @[simp]
 lemma dropPair_permP {n n1 : ℕ} {c : Fin (n + 1 + 1) → S.C}

PhysLean/Relativity/Tensors/TensorSpecies/Tensor/Evaluation.lean

@@ -118,7 +118,7 @@ noncomputable def evalT {n : ℕ} {c : Fin (n + 1) → S.C} (i : Fin (n + 1))
     Tensor S c →ₗ[k] Tensor S (c ∘ i.succAbove) :=
   PiTensorProduct.lift (Pure.evalPMultilinear i b)
 
-TODO "Add lemmas related to the interaction of evalT and permT, prodT and contrT."
+TODO "6VZ6G" "Add lemmas related to the interaction of evalT and permT, prodT and contrT."
 
 end Tensor
 

PhysLean/Relativity/Tensors/Tree/Basic.lean

@@ -296,7 +296,7 @@ lemma eq_tensorNode_of_eq_tensor {T1 : TensorTree S c} {t : S.F.obj (OverColor.m
 ## Properties on basis.
 -/
 
-TODO "Fill in the other relationships between tensor trees and tensor basis."
+TODO "6VZ5Z" "Fill in the other relationships between tensor trees and tensor basis."
 open TensorSpecies
 
 lemma tensorNode_tensorBasis_repr {c : Fin n → S.C} (T : S.F.obj (OverColor.mk c)) :

PhysLean/Relativity/Tensors/Tree/NodeIdentities/Basic.lean

@@ -24,19 +24,6 @@ namespace TensorTree
 
 variable {k : Type} [CommRing k] {S : TensorSpecies k}
 
-/-!
-
-## Equality of constructors.
-
--/
-
-/-- A `constVecNode` has equal tensor to the `vecNode` with the map evaluated at 1. -/
-informal_lemma constVecNode_eq_vecNode where
-  deps := [``constVecNode, ``vecNode]
-
-/-- A `constTwoNode` has equal tensor to the `twoNode` with the map evaluated at 1. -/
-informal_lemma constTwoNode_eq_twoNode where
-  deps := [``constTwoNode, ``twoNode]
 
 /-!
 

scripts/MetaPrograms/TODO_to_yml.lean

@@ -131,10 +131,12 @@ structure FullTODOInfo where
   isInformalDef : Bool
   isInformalLemma : Bool
   category : PhysLeanCategory
+  tag : String
 
 def FullTODOInfo.ofTODO (t : todoInfo) : FullTODOInfo :=
   {content := t.content, fileName := t.fileName, line := t.line, name := t.fileName,
-   isInformalDef := false, isInformalLemma := false, category := PhysLeanCategory.ofFileName t.fileName}
+   isInformalDef := false, isInformalLemma := false, category := PhysLeanCategory.ofFileName t.fileName,
+   tag := t.tag}
 
 unsafe def getTodoInfo : MetaM (Array FullTODOInfo) := do
   let env ← getEnv
@@ -142,8 +144,9 @@ unsafe def getTodoInfo : MetaM (Array FullTODOInfo) := do
   -- pure (todoInfo.qsort (fun x y => x.fileName.toString < y.fileName.toString)).toList
   pure (todoInfo.map FullTODOInfo.ofTODO)
 
-def informalTODO (x : ConstantInfo) : CoreM FullTODOInfo := do
+unsafe def informalTODO (x : ConstantInfo) : CoreM FullTODOInfo := do
   let name := x.name
+  let tag ← Informal.getTag x
   let lineNo ← Name.lineNumber name
   let docString ← Name.getDocString name
   let file ← Name.fileName name
@@ -151,9 +154,10 @@ def informalTODO (x : ConstantInfo) : CoreM FullTODOInfo := do
   let isInformalLemma := Informal.isInformalLemma x
   let category := PhysLeanCategory.ofFileName file
   return {content := docString, fileName := file, line := lineNo, name := name,
-          isInformalDef := isInformalDef, isInformalLemma := isInformalLemma, category := category}
+          isInformalDef := isInformalDef, isInformalLemma := isInformalLemma, category := category,
+          tag := tag}
 
-def allInformalTODO : CoreM (Array FullTODOInfo) := do
+unsafe def allInformalTODO : CoreM (Array FullTODOInfo) := do
   let x ← AllInformal
   x.mapM informalTODO
 
@@ -168,6 +172,7 @@ def FullTODOInfo.toYAML (todo : FullTODOInfo) : MetaM String := do
     isInformalLemma: {todo.isInformalLemma}
     category: {todo.category}
     name: {todo.name}
+    tag: {todo.tag}
     content: |
       {contentIndent}"
 
@@ -191,6 +196,11 @@ unsafe def categoriesToYML : MetaM String := do
 
 unsafe def todosToYAML : MetaM String := do
   let todos ← allTODOs
+  /- Check no dulicate tags-/
+  let tags := todos.map (fun x => x.tag)
+  if !tags.Nodup then
+    panic! "Duplicate tags found."
+  /- End of check. -/
   let todosYAML ← todos.mapM FullTODOInfo.toYAML
   return "TODOItem:\n" ++ String.intercalate "\n" todosYAML