docs: Fix typos in docs

HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean

@@ -83,7 +83,7 @@ lemma S₂₃_nonneg (V : Quotient CKMMatrixSetoid) : 0 ≤ S₂₃ V := by
   · rw [S₂₃, if_neg ha, @div_nonneg_iff]
     exact .inl (.intro (VAbs_ge_zero 1 2 V) (Real.sqrt_nonneg (VudAbs V ^ 2 + VusAbs V ^ 2)))
 
-/-- For a CKM matrix `sin θ₁₂` is less then or equal to 1. -/
+/-- For a CKM matrix `sin θ₁₂` is less than or equal to 1. -/
 lemma S₁₂_leq_one (V : Quotient CKMMatrixSetoid) : S₁₂ V ≤ 1 := by
   rw [S₁₂, @div_le_one_iff]
   by_cases h1 : √(VudAbs V ^ 2 + VusAbs V ^ 2) = 0
@@ -99,11 +99,11 @@ lemma S₁₂_leq_one (V : Quotient CKMMatrixSetoid) : S₁₂ V ≤ 1 := by
     simp only [Fin.isValue, le_add_iff_nonneg_left]
     exact sq_nonneg (VAbs 0 0 V)
 
-/-- For a CKM matrix `sin θ₁₃` is less then or equal to 1. -/
+/-- For a CKM matrix `sin θ₁₃` is less than or equal to 1. -/
 lemma S₁₃_leq_one (V : Quotient CKMMatrixSetoid) : S₁₃ V ≤ 1 :=
   VAbs_leq_one 0 2 V
 
-/-- For a CKM matrix `sin θ₂₃` is less then or equal to 1. -/
+/-- For a CKM matrix `sin θ₂₃` is less than or equal to 1. -/
 lemma S₂₃_leq_one (V : Quotient CKMMatrixSetoid) : S₂₃ V ≤ 1 := by
   by_cases ha : VubAbs V = 1
   · rw [S₂₃, if_pos ha]

HepLean/Lorentz/Group/Orthochronous.lean

@@ -47,7 +47,7 @@ lemma IsOrthochronous_iff_ge_one :
   rw [IsOrthochronous_iff_futurePointing, NormOne.FuturePointing.mem_iff_inl_one_le_inl,
     toNormOne_inl]
 
-/-- A Lorentz transformation is not orthochronous if and only if its `0 0` element is less then
+/-- A Lorentz transformation is not orthochronous if and only if its `0 0` element is less than
   or equal to minus one. -/
 lemma not_orthochronous_iff_le_neg_one :
     ¬ IsOrthochronous Λ ↔ Λ.1 (Sum.inl 0) (Sum.inl 0) ≤ -1 := by
@@ -65,8 +65,8 @@ def timeCompCont : C(LorentzGroup d, ℝ) := ⟨fun Λ => Λ.1 (Sum.inl 0) (Sum.
     Continuous.matrix_elem (continuous_iff_le_induced.mpr fun _ a => a) (Sum.inl 0) (Sum.inl 0)⟩
 
 /-- An auxiliary function used in the definition of `orthchroMapReal`.
-  This function takes all elements of `ℝ` less then `-1` to `-1`,
-  all elements of `R` greater then `1` to `1` and preserves all other elements. -/
+  This function takes all elements of `ℝ` less than `-1` to `-1`,
+  all elements of `R` greater than `1` to `1` and preserves all other elements. -/
 def stepFunction : ℝ → ℝ := fun t =>
   if t ≤ -1 then -1 else
     if 1 ≤ t then 1 else t

HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean

@@ -42,7 +42,7 @@ def fieldOpIdealSet : Set (FieldOpFreeAlgebra 𝓕) :=
   This corresponds to the condition that two operators with different statistics always
   super-commute. In other words, fermions and bosons always super-commute.
 - `[ofCrAnOpF φ1, [ofCrAnOpF φ2, ofCrAnOpF φ3]ₛca]ₛca`. This corresponds to the condition,
-  when combined with the conditions above, that the super-commutator is in the center of the
+  when combined with the conditions above, that the super-commutator is in the center
   of the algebra.
 -/
 abbrev FieldOpAlgebra : Type := (TwoSidedIdeal.span 𝓕.fieldOpIdealSet).ringCon.Quotient

HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Basic.lean

@@ -223,9 +223,9 @@ lemma ι_normalOrderF_eq_of_equiv (a b : 𝓕.FieldOpFreeAlgebra) (h : a ≈ b)
 
   `FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕`
 
-  defined as the decent of `ι ∘ₗ normalOrderF : FieldOpFreeAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕`
+  defined as the descent of `ι ∘ₗ normalOrderF : FieldOpFreeAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕`
   from `FieldOpFreeAlgebra 𝓕` to `FieldOpAlgebra 𝓕`.
-  This decent exists because `ι ∘ₗ normalOrderF` is well-defined on equivalence classes.
+  This descent exists because `ι ∘ₗ normalOrderF` is well-defined on equivalence classes.
 
   The notation `𝓝(a)` is used for `normalOrder a` for `a` an element of `FieldOpAlgebra 𝓕`. -/
 noncomputable def normalOrder : FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕 where

HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean

@@ -350,7 +350,7 @@ then `φ * 𝓝(φ₀φ₁…φₙ)` is equal to
 
 `𝓝(φφ₀φ₁…φₙ) + ∑ i, (𝓢(φ,φ₀φ₁…φᵢ₋₁) • [anPart φ, φᵢ]ₛ) * 𝓝(φ₀…φᵢ₋₁φᵢ₊₁…φₙ)`.
 
-The proof of ultimately goes as follows:
+The proof ultimately goes as follows:
 - `ofFieldOp_eq_crPart_add_anPart` is used to split `φ` into its creation and annihilation parts.
 - The following relation is then used
 

HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/WickContractions.lean

@@ -32,7 +32,7 @@ variable {𝓕 : FieldSpecification}
 
   where `s` is the exchange sign for `φ` and the uncontracted fields in `φ₀…φᵢ₋₁`.
 
-  The prove of this result ultimately a consequence of `normalOrder_superCommute_eq_zero`.
+  The proof of this result ultimately is a consequence of `normalOrder_superCommute_eq_zero`.
 -/
 lemma normalOrder_uncontracted_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
     (i : Fin φs.length.succ) (φsΛ : WickContraction φs.length) :
@@ -104,7 +104,7 @@ lemma normalOrder_uncontracted_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp
   `𝓝([φsΛ ↩Λ φ i (some k)]ᵘᶜ)` is equal to the normal ordering of `[φsΛ]ᵘᶜ` with the `𝓕.FieldOp`
   corresponding to `k` removed.
 
-  The proof of this result ultimately a consequence of definitions.
+  The proof of this result ultimately is a consequence of definitions.
 -/
 lemma normalOrder_uncontracted_some (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
     (i : Fin φs.length.succ) (φsΛ : WickContraction φs.length) (k : φsΛ.uncontracted) :

HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTerm.lean

@@ -27,7 +27,7 @@ noncomputable section
 
   `φsΛ.sign • φsΛ.staticContract * 𝓝([φsΛ]ᵘᶜ)`.
 
-  This is term which appears in the static version Wick's theorem. -/
+  This is a term which appears in the static version Wick's theorem. -/
 def staticWickTerm {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) : 𝓕.FieldOpAlgebra :=
   φsΛ.sign • φsΛ.staticContract * 𝓝(ofFieldOpList [φsΛ]ᵘᶜ)
 
@@ -120,7 +120,7 @@ holds
 
 where the sum is over all `k` in `Option φsΛ.uncontracted`,  so `k` is either `none` or `some k`.
 
-The proof of proceeds as follows:
+The proof proceeds as follows:
 - `ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum` is used to expand `φ 𝓝([φsΛ]ᵘᶜ)` as
   a sum over `k` in `Option φsΛ.uncontracted` of terms involving `[anPart φ, φs[k]]ₛ`.
 - Then `staticWickTerm_insert_zero_none` and `staticWickTerm_insert_zero_some` are

HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTheorem.lean

@@ -32,7 +32,7 @@ The proof is via induction on `φs`.
 The inductive step works as follows:
 
 For the LHS:
-1. The proof considers `φ₀…φₙ` as `φ₀(φ₁…φₙ)` and use the induction hypothesis on `φ₁…φₙ`.
+1. The proof considers `φ₀…φₙ` as `φ₀(φ₁…φₙ)` and uses the induction hypothesis on `φ₁…φₙ`.
 2. This gives terms of the form `φ * φsΛ.staticWickTerm` on which
   `mul_staticWickTerm_eq_sum` is used where `φsΛ` is a Wick contraction of `φ₁…φₙ`,
   to rewrite terms as a sum over optional uncontracted elements of `φsΛ`
@@ -45,7 +45,7 @@ For the RHS:
   is split via `insertLift_sum` into a sum over Wick contractions `φsΛ` of `φ₁…φₙ` and
   sum over optional uncontracted elements of `φsΛ`.
 
-Both side now are sums over the same thing and their terms equate by the nature of the
+Both sides are now sums over the same thing and their terms equate by the nature of the
 lemmas used.
 
 -/

HepLean/PerturbationTheory/FieldOpAlgebra/SuperCommute.lean

@@ -92,7 +92,7 @@ lemma superCommuteRight_eq_of_equiv (a1 a2 : 𝓕.FieldOpFreeAlgebra) (h : a1 
 
   `FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕`
 
-  defined as the decent of `ι ∘ superCommuteF` in both arguments.
+  defined as the descent of `ι ∘ superCommuteF` in both arguments.
   In particular for `φs` and `φs'` lists of `𝓕.CrAnFieldOp` in `FieldOpAlgebra 𝓕` the following
   relation holds:
 

HepLean/PerturbationTheory/FieldOpAlgebra/TimeOrder.lean

@@ -371,9 +371,9 @@ lemma ι_timeOrderF_eq_of_equiv (a b : 𝓕.FieldOpFreeAlgebra) (h : a ≈ b) :
 
 `FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕`
 
-defined as the decent of `ι ∘ₗ timeOrderF : FieldOpFreeAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕` from
+defined as the descent of `ι ∘ₗ timeOrderF : FieldOpFreeAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕` from
 `FieldOpFreeAlgebra 𝓕` to `FieldOpAlgebra 𝓕`.
-This decent exists because `ι ∘ₗ timeOrderF` is well-defined on equivalence classes.
+This descent exists because `ι ∘ₗ timeOrderF` is well-defined on equivalence classes.
 
 The notation `𝓣(a)` is used for `timeOrder a`. -/
 noncomputable def timeOrder : FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕 where

HepLean/PerturbationTheory/FieldOpAlgebra/WickTerm.lean

@@ -29,7 +29,7 @@ noncomputable section
 
   `φsΛ.sign • φsΛ.timeContract * 𝓝([φsΛ]ᵘᶜ)`.
 
-  This is term which appears in the Wick's theorem. -/
+  This is a term which appears in the Wick's theorem. -/
 def wickTerm {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) : 𝓕.FieldOpAlgebra :=
   φsΛ.sign • φsΛ.timeContract * 𝓝(ofFieldOpList [φsΛ]ᵘᶜ)
 
@@ -95,10 +95,10 @@ lemma wickTerm_insert_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
 
 /-- For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, an element `φ` of
   `𝓕.FieldOp`, `i ≤ φs.length` and a `k` in `φsΛ.uncontracted`,
-  such that all `𝓕.FieldOp` in `φ₀…φᵢ₋₁` have time strictly less then `φ` and
-  `φ` has a time greater then or equal to all `FieldOp` in `φ₀…φₙ`, then
+  such that all `𝓕.FieldOp` in `φ₀…φᵢ₋₁` have time strictly less than `φ` and
+  `φ` has a time greater than or equal to all `FieldOp` in `φ₀…φₙ`, then
   `(φsΛ ↩Λ φ i (some k)).staticWickTerm`
-is equal the product of
+is equal to the product of
 - the sign `𝓢(φ, φ₀…φᵢ₋₁) `
 - the sign `φsΛ.sign`
 - `φsΛ.timeContract`
@@ -177,14 +177,14 @@ lemma wickTerm_insert_some (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
 /--
 For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, an element `φ` of
   `𝓕.FieldOp`, and `i ≤ φs.length`
-  such that all `𝓕.FieldOp` in `φ₀…φᵢ₋₁` have time strictly less then `φ` and
-  `φ` has a time greater then or equal to all `FieldOp` in `φ₀…φₙ`, then
+  such that all `𝓕.FieldOp` in `φ₀…φᵢ₋₁` have time strictly less than `φ` and
+  `φ` has a time greater than or equal to all `FieldOp` in `φ₀…φₙ`, then
 
 `φ * φsΛ.wickTerm = 𝓢(φ, φ₀…φᵢ₋₁) • ∑ k, (φsΛ ↩Λ φ i k).wickTerm`
 
 where the sum is over all `k` in `Option φsΛ.uncontracted`, so `k` is either `none` or `some k`.
 
-The proof of proceeds as follows:
+The proof proceeds as follows:
 - `ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum` is used to expand `φ 𝓝([φsΛ]ᵘᶜ)` as
   a sum over `k` in `Option φsΛ.uncontracted` of terms involving `[anPart φ, φs[k]]ₛ`.
 - Then `wickTerm_insert_none` and `wickTerm_insert_some` are used to equate terms.

HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheorem.lean

@@ -91,7 +91,7 @@ For the RHS:
   is split via `insertLift_sum` into a sum over Wick contractions `φsΛ` of `φ₀…φᵢ₋₁φᵢ₊₁φ` and
   sum over optional uncontracted elements of `φsΛ`.
 
-Both side now are sums over the same thing and their terms equate by the nature of the
+Both sides are now sums over the same thing and their terms equate by the nature of the
 lemmas used.
 -/
 theorem wicks_theorem : (φs : List 𝓕.FieldOp) → 𝓣(ofFieldOpList φs) =

HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheoremNormal.lean

@@ -117,9 +117,9 @@ For a list `φs` of `𝓕.FieldOp`, then `𝓣(φs)` is equal to the sum of
   and the second sum is over all Wick contraction `φssucΛ` of the uncontracted elements of `φsΛ`
   which do not have any equal time contractions.
 
-The proof of proceeds as follows
+The proof proceeds as follows
 - `wicks_theorem` is used to rewrite `𝓣(φs)` as a sum over all Wick contractions.
-- The sum over all Wick contractions is then split additively into two parts using based on having
+- The sum over all Wick contractions is then split additively into two parts based on having
   or not having an equal time contractions.
 - Using `join`, the sum `∑ φsΛ, _` over Wick contractions which do have equal time contractions
   is split into two sums `∑ φsΛ, ∑ φsucΛ, _`, the first over non-zero elements

HepLean/PerturbationTheory/FieldSpecification/Basic.lean

@@ -43,7 +43,7 @@ The structure `FieldSpecification` is defined to have the following content:
       index of the field and its conjugate.
   - For every field `f` in `Field`, a type `AsymptoticLabel f` whose elements label the different
     types of incoming asymptotic field operators associated with the
-    field `f` (this is also matches the types of outgoing asymptotic field operators).
+    field `f` (this also matches the types of outgoing asymptotic field operators).
     For example,
     - For `f` a *real-scalar field*, `AsymptoticLabel f` will have a unique element.
     - For `f` a *complex-scalar field*, `AsymptoticLabel f` will have two elements, one for the
@@ -81,7 +81,7 @@ variable (𝓕 : FieldSpecification)
   element labelled `outAsymp f e p` corresponding to an outgoing asymptotic field operator of the
   field `f`, of label `e` (e.g. specifying the spin), and momentum `p`.
 
-As some intuition, if `f` corresponds to a Weyl-fermion field, then
+As an example, if `f` corresponds to a Weyl-fermion field, then
 - For `inAsymp f e p`, `e` would correspond to a spin `s`, and `inAsymp f e p` would, once
   represented in the operator algebra,
   be proportional to the creation operator `a(p, s)`.
@@ -120,7 +120,7 @@ def fieldOpToField : 𝓕.FieldOp → 𝓕.Field
 - For `φ` an element of `𝓕.FieldOp`, `𝓕 |>ₛ φ` is `fieldOpStatistic φ`.
 - For `φs` a list of `𝓕.FieldOp`, `𝓕 |>ₛ φs` is the product of `fieldOpStatistic φ` over
   the list `φs`.
-- For a function `f : Fin n → 𝓕.FieldOp` and a finset `a` of `Fin n`, `𝓕 |>ₛ ⟨f, a⟩` is the
+- For a function `f : Fin n → 𝓕.FieldOp` and a finite set `a` of `Fin n`, `𝓕 |>ₛ ⟨f, a⟩` is the
   product of `fieldOpStatistic (f i)` for all `i ∈ a`. -/
 def fieldOpStatistic : 𝓕.FieldOp → FieldStatistic := 𝓕.statistic ∘ 𝓕.fieldOpToField
 

HepLean/PerturbationTheory/FieldSpecification/CrAnFieldOp.lean

@@ -66,18 +66,18 @@ def fieldOpToCreateAnnihilateTypeCongr : {i j : 𝓕.FieldOp} → i = j →
 For a field specification `𝓕`, the (sigma) type `𝓕.CrAnFieldOp`
 corresponds to the type of creation and annihilation parts of field operators.
 It formally defined to consist of the following elements:
-- for each in incoming asymptotic field operator `φ` in `𝓕.FieldOp` an element
+- for each incoming asymptotic field operator `φ` in `𝓕.FieldOp` an element
   written as `⟨φ, ()⟩` in `𝓕.CrAnFieldOp`, corresponding to the creation part of `φ`.
   Here `φ` has no annihilation part. (Here `()` is the unique element of `Unit`.)
 - for each position field operator `φ` in `𝓕.FieldOp` an element of `𝓕.CrAnFieldOp`
   written as `⟨φ, .create⟩`, corresponding to the creation part of `φ`.
 - for each position field operator `φ` in `𝓕.FieldOp` an element of `𝓕.CrAnFieldOp`
   written as `⟨φ, .annihilate⟩`, corresponding to the annihilation part of `φ`.
-- for each out outgoing asymptotic field operator `φ` in `𝓕.FieldOp` an element
+- for each outgoing asymptotic field operator `φ` in `𝓕.FieldOp` an element
   written as `⟨φ, ()⟩` in `𝓕.CrAnFieldOp`, corresponding to the annihilation part of `φ`.
   Here `φ` has no creation part. (Here `()` is the unique element of `Unit`.)
 
-As some intuition, if `f` corresponds to a Weyl-fermion field, it would contribute
+As an example, if `f` corresponds to a Weyl-fermion field, it would contribute
   the following elements to `𝓕.CrAnFieldOp`
 - an element corresponding to incoming asymptotic operators for each spin `s`: `a(p, s)`.
 - an element corresponding to the creation parts of position operators for each each Lorentz

HepLean/PerturbationTheory/FieldSpecification/NormalOrder.lean

@@ -20,7 +20,7 @@ variable {𝓕 : FieldSpecification}
   - `φ₀` is a field creation operator
   - `φ₁` is a field annihilation operator.
 
-  Thus, colloquially `𝓕.normalOrderRel φ₀ φ₁` says the creation operators are 'less then'
+  Thus, colloquially `𝓕.normalOrderRel φ₀ φ₁` says the creation operators are less than
   annihilation operators. -/
 def normalOrderRel : 𝓕.CrAnFieldOp → 𝓕.CrAnFieldOp → Prop :=
   fun a b => CreateAnnihilate.normalOrder (𝓕 |>ᶜ a) (𝓕 |>ᶜ b)

HepLean/PerturbationTheory/FieldSpecification/TimeOrder.lean

@@ -198,10 +198,10 @@ lemma timeOrderList_eq_maxTimeField_timeOrderList (φ : 𝓕.FieldOp) (φs : Lis
 - `φ₀` is an *outgoing* asymptotic operator
 - `φ₁` is an *incoming* asymptotic field operator
 - `φ₀` and `φ₁` are both position field operators where
-  the `SpaceTime` point of `φ₀` has a time *greater* then or equal to that of `φ₁`.
+  the `SpaceTime` point of `φ₀` has a time *greater* than or equal to that of `φ₁`.
 
-Thus, colloquially `𝓕.crAnTimeOrderRel φ₀ φ₁` if `φ₀` has time *greater* then or equal to `φ₁`.
-The use of *greater* then rather then *less* then is because on ordering lists of operators
+Thus, colloquially `𝓕.crAnTimeOrderRel φ₀ φ₁` if `φ₀` has time *greater* than or equal to `φ₁`.
+The use of *greater* than rather then *less* than is because on ordering lists of operators
 it is needed that the operator with the greatest time is to the left.
 -/
 def crAnTimeOrderRel (a b : 𝓕.CrAnFieldOp) : Prop := 𝓕.timeOrderRel a.1 b.1

HepLean/PerturbationTheory/WickContraction/Basic.lean

@@ -17,7 +17,7 @@ variable {𝓕 : FieldSpecification}
 Given a natural number `n`, which will correspond to the number of fields needing
 contracting, a Wick contraction
 is a finite set of pairs of `Fin n` (numbers `0`, ..., `n-1`), such that no
-element of `Fin n` occurs in more then one pair. The pairs are the positions of fields we
+element of `Fin n` occurs in more than one pair. The pairs are the positions of fields we
 'contract' together.
 -/
 def WickContraction (n : ℕ) : Type :=
@@ -520,8 +520,8 @@ lemma prod_finset_eq_mul_fst_snd (c : WickContraction n) (a : c.1)
 /-- For a field specification `𝓕`, `φs` a list of `𝓕.FieldOp` and a Wick contraction
   `φsΛ` of `φs`, the Wick contraction `φsΛ` is said to be `GradingCompliant` if
   for every pair in `φsΛ` the contracted fields are either both `fermionic` or both `bosonic`.
-  In other words, in a `GradingCompliant` Wick contraction no contractions occur between
-  `fermionic` and `bosonic` fields. -/
+  In other words, in a `GradingCompliant` Wick contraction if
+  no contracted pairs occur between `fermionic` and `bosonic` fields. -/
 def GradingCompliant (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) :=
   ∀ (a : φsΛ.1), (𝓕 |>ₛ φs[φsΛ.fstFieldOfContract a]) = (𝓕 |>ₛ φs[φsΛ.sndFieldOfContract a])
 

HepLean/PerturbationTheory/WickContraction/InsertAndContract.lean

@@ -34,8 +34,8 @@ open HepLean.Fin
   of `φ` (at position `i`) with the new position of `j` after `φ` is added.
 
   In other words, `φsΛ.insertAndContract φ i j` is formed by adding `φ` to `φs` at position `i`,
-  and contracting `φ` with the field originally at position `j` if `j` is not none.
-  It is a Wick contraction of `φs.insertIdx φ i`, the list `φs` with `φ` inserted at
+  and contracting `φ` with the field originally at position `j` if `j` is not `none`.
+  It is a Wick contraction of the list `φs.insertIdx φ i` corresponding to `φs` with `φ` inserted at
   position `i`.
 
   The notation `φsΛ ↩Λ φ i j` is used to denote `φsΛ.insertAndContract φ i j`. -/

HepLean/PerturbationTheory/WickContraction/Sign/InsertNone.lean

@@ -241,7 +241,7 @@ lemma signInsertNone_eq_filterset (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
 /-- For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a graded compliant Wick contraction `φsΛ` of `φs`,
   an `i ≤ φs.length`, and a `φ` in `𝓕.FieldOp`, then
   `(φsΛ ↩Λ φ i none).sign = s * φsΛ.sign`
-  where `s` is the sign got by moving `φ` through the elements of `φ₀…φᵢ₋₁` which
+  where `s` is the sign arrived at by moving `φ` through the elements of `φ₀…φᵢ₋₁` which
   are contracted with some element.
 
   The proof of this result involves a careful consideration of the contributions of different