diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean
index e1e3f04..fd6cdb0 100644
--- a/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean
+++ b/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean
@@ -230,7 +230,8 @@ The proof of this result ultimately goes as follows
 - `superCommuteF_ofCrAnListF_ofCrAnListF_eq_sum` is used to rewrite the super commutator of `φ`
   (considered as a list with one element) with
   `ofCrAnList φsn` as a sum of super commutators, one for each element of `φsn`.
-- The fact that super-commutators are in the center of `𝓕.FieldOpAlgebra` is used to  rearrange terms.
+- The fact that super-commutators are in the center of `𝓕.FieldOpAlgebra` is used to  rearrange
+  terms.
 - Properties of ordered lists, and `normalOrderSign_eraseIdx` are then used to complete the proof.
 -/
 lemma ofCrAnOp_superCommute_normalOrder_ofCrAnList_sum (φ : 𝓕.CrAnFieldOp)