diff --git a/PhysLean/CondensedMatter/Basic.lean b/PhysLean/CondensedMatter/Basic.lean index a80d434..03b8b83 100644 --- a/PhysLean/CondensedMatter/Basic.lean +++ b/PhysLean/CondensedMatter/Basic.lean @@ -10,7 +10,6 @@ Authors: Joseph Tooby-Smith This directory is currently a place holder. Please feel free to contribute! - Some directories which are NOT currently place holders are: - Mathematics - Meta @@ -19,5 +18,4 @@ Some directories which are NOT currently place holders are: - Quantum Mechanics - Relativity - -/ diff --git a/PhysLean/Optics/Basic.lean b/PhysLean/Optics/Basic.lean index 1853536..8eadccb 100644 --- a/PhysLean/Optics/Basic.lean +++ b/PhysLean/Optics/Basic.lean @@ -18,5 +18,4 @@ Some directories which are NOT currently place holders are: - Quantum Mechanics - Relativity - -/ diff --git a/PhysLean/Particles/StandardModel/HiggsBoson/Basic.lean b/PhysLean/Particles/StandardModel/HiggsBoson/Basic.lean index 411a9b6..b9f75c7 100644 --- a/PhysLean/Particles/StandardModel/HiggsBoson/Basic.lean +++ b/PhysLean/Particles/StandardModel/HiggsBoson/Basic.lean @@ -93,7 +93,7 @@ instance : ContMDiffVectorBundle ⊤ HiggsVec HiggsBundle SpaceTime.asSmoothMani /-- The type `HiggsField` is defined such that elements are smooth sections of the trivial vector bundle `HiggsBundle`. Such elements are Higgs fields. Since `HiggsField` is trivial as a vector bundle, a Higgs field is equivalent to a smooth map - from `SpaceTime` to `HiggsVec`. -/ + from `SpaceTime` to `HiggsVec`. -/ abbrev HiggsField : Type := ContMDiffSection SpaceTime.asSmoothManifold HiggsVec ⊤ HiggsBundle /-- Given a vector in `HiggsVec` the constant Higgs field with value equal to that diff --git a/PhysLean/Particles/StandardModel/HiggsBoson/PointwiseInnerProd.lean b/PhysLean/Particles/StandardModel/HiggsBoson/PointwiseInnerProd.lean index 6d79745..e4197dc 100644 --- a/PhysLean/Particles/StandardModel/HiggsBoson/PointwiseInnerProd.lean +++ b/PhysLean/Particles/StandardModel/HiggsBoson/PointwiseInnerProd.lean @@ -113,7 +113,7 @@ lemma smooth_innerProd (φ1 φ2 : HiggsField) : ContMDiff 𝓘(ℝ, SpaceTime) the function `SpaceTime → ℝ` obtained by taking the square norm of the pointwise Higgs vector. In other words, `normSq φ x = ‖φ x‖ ^ 2`. - The notation `‖φ‖_H^2` is used for the `normSq φ` -/ + The notation `‖φ‖_H^2` is used for the `normSq φ`. -/ @[simp] def normSq (φ : HiggsField) : SpaceTime → ℝ := fun x => ‖φ x‖ ^ 2 diff --git a/PhysLean/QuantumMechanics/FiniteTarget/Basic.lean b/PhysLean/QuantumMechanics/FiniteTarget/Basic.lean index 27d3399..55ddd90 100644 --- a/PhysLean/QuantumMechanics/FiniteTarget/Basic.lean +++ b/PhysLean/QuantumMechanics/FiniteTarget/Basic.lean @@ -35,7 +35,7 @@ abbrev V (_ : FiniteTarget n hℏ) := Fin n → ℂ /-- Given a finite target QM system `A`, the time evolution matrix for a `t : ℝ`, `A.timeEvolutionMatrix t` is defined as `e ^ (- I t /ℏ * A.H)`. -/ noncomputable def timeEvolutionMatrix (A : FiniteTarget n hℏ) (t : ℝ) : Matrix (Fin n) (Fin n) ℂ := - NormedSpace.exp ℂ (- (Complex.I * t / ℏ) • A.H) + NormedSpace.exp ℂ (- (Complex.I * t / ℏ) • A.H) /-- Given a finite target QM system `A`, `timeEvolution` is the linear map from `A.V` to `A.V` obtained by multiplication with `timeEvolutionMatrix`. -/ diff --git a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Basic.lean b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Basic.lean index 3d800c2..1bf1eb6 100644 --- a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Basic.lean +++ b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Basic.lean @@ -134,7 +134,7 @@ lemma one_over_ξ : 1/Q.ξ = √(Q.m * Q.ω / Q.ℏ) := by have := Q.hℏ field_simp [ξ] -lemma ξ_inverse : Q.ξ⁻¹ = √(Q.m * Q.ω / Q.ℏ):= by +lemma ξ_inverse : Q.ξ⁻¹ = √(Q.m * Q.ω / Q.ℏ) := by rw [inv_eq_one_div] exact one_over_ξ Q @@ -182,7 +182,7 @@ lemma schrodingerOperator_eq (ψ : ℝ → ℂ) : /-- The schrodinger operator written in terms of `ξ`. -/ lemma schrodingerOperator_eq_ξ (ψ : ℝ → ℂ) : Q.schrodingerOperator ψ = - fun x => (Q.ℏ ^2 / (2 * Q.m)) * (- (deriv (deriv ψ) x) + (1/Q.ξ^2 )^2 * x^2 * ψ x) := by + fun x => (Q.ℏ ^2 / (2 * Q.m)) * (- (deriv (deriv ψ) x) + (1/Q.ξ^2)^2 * x^2 * ψ x) := by funext x simp [schrodingerOperator_eq, ξ_sq, ξ_inverse, ξ_ne_zero, ξ_pos, ξ_abs, ← Complex.ofReal_pow] have hm' := Complex.ofReal_ne_zero.mpr Q.m_ne_zero diff --git a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Completeness.lean b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Completeness.lean index b28ed4f..3daf1bb 100644 --- a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Completeness.lean +++ b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Completeness.lean @@ -175,7 +175,7 @@ lemma orthogonal_physHermite_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f) or_false, Real.sqrt_nonneg] at h1 have h0 : n ! ≠ 0 := by exact factorial_ne_zero n - have h0' : ¬ (√Q.ξ = 0 ∨ √Real.pi = 0):= by + have h0' : ¬ (√Q.ξ = 0 ∨ √Real.pi = 0) := by simpa using And.intro (Real.sqrt_ne_zero'.mpr Q.ξ_pos) (Real.sqrt_ne_zero'.mpr Real.pi_pos) simp only [h0, h0', or_self, false_or] at h1 rw [← h1] diff --git a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean index 09ef79e..8e6a0e6 100644 --- a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean +++ b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean @@ -43,7 +43,7 @@ lemma eigenfunction_eq (n : ℕ) : ring lemma eigenfunction_zero : Q.eigenfunction 0 = fun (x : ℝ) => - (1/ √(√Real.pi * Q.ξ)) * Complex.exp (- x^2 / (2 * Q.ξ^2)):= by + (1/ √(√Real.pi * Q.ξ)) * Complex.exp (- x^2 / (2 * Q.ξ^2)) := by funext x simp [eigenfunction] @@ -190,8 +190,8 @@ lemma eigenfunction_mul (n p : ℕ) : one_div, mul_inv_rev, neg_mul, Complex.ofReal_exp, Complex.ofReal_div, Complex.ofReal_neg, Complex.ofReal_pow, Complex.ofReal_ofNat, mul_one] ring - _ = (1/√(2 ^ n * n !) * 1/√(2 ^ p * p !)) * (1/ (√Real.pi * Q.ξ)) * - (physHermite n (x / Q.ξ) * physHermite p (x / Q.ξ)) * (Real.exp (- x^2 / Q.ξ^2)) := by + _ = (1/√(2 ^ n * n !) * 1/√(2 ^ p * p !)) * (1/ (√Real.pi * Q.ξ)) * + (physHermite n (x / Q.ξ) * physHermite p (x / Q.ξ)) * (Real.exp (- x^2 / Q.ξ^2)) := by congr 1 · congr 1 · congr 1 diff --git a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/TISE.lean b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/TISE.lean index d2feb00..716c457 100644 --- a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/TISE.lean +++ b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/TISE.lean @@ -70,7 +70,7 @@ lemma deriv_eigenfunction_zero : deriv (Q.eigenfunction 0) = ring lemma deriv_eigenfunction_zero' : deriv (Q.eigenfunction 0) = - (- √2 / (2 * Q.ξ) : ℂ) • Q.eigenfunction 1 := by + (- √2 / (2 * Q.ξ) : ℂ) • Q.eigenfunction 1 := by rw [deriv_eigenfunction_zero] funext x simp only [Complex.ofReal_div, Complex.ofReal_neg, Complex.ofReal_one, Complex.ofReal_pow, @@ -89,7 +89,7 @@ lemma deriv_physHermite_characteristic_length (n : ℕ) : match n with | 0 => rw [physHermite_zero] - simp [deriv_const_mul_field', Complex.ofReal_div, Complex.ofReal_mul, Algebra.smul_mul_assoc, + simp [deriv_const_mul_field', Complex.ofReal_div, Complex.ofReal_mul, Algebra.smul_mul_assoc, Complex.ofReal_zero, zero_mul, zero_add, zero_div, cast_zero, Complex.ofReal_zero, zero_smul] | n + 1 => funext x @@ -158,7 +158,6 @@ lemma deriv_deriv_eigenfunction_zero (x : ℝ) : deriv (deriv (Q.eigenfunction 0 simp only [Complex.ofReal_one, Complex.ofReal_pow, one_mul, one_pow, inv_pow] ring - lemma deriv_deriv_eigenfunction_succ (n : ℕ) (x : ℝ) : deriv (fun x => deriv (Q.eigenfunction (n + 1)) x) x = Complex.ofReal (1/√(2 ^ (n + 1) * (n + 1) !) * (1/Q.ξ)) * @@ -183,7 +182,7 @@ lemma deriv_deriv_eigenfunction_succ (n : ℕ) (x : ℝ) : simp only [differentiableAt_const, deriv_mul, deriv_const', zero_mul, mul_zero, add_zero, deriv_add, zero_add] rw [deriv_mul (by fun_prop) (by fun_prop)] - simp [deriv_mul_const_field', Complex.deriv_ofReal, mul_one] + simp [deriv_mul_const_field', Complex.deriv_ofReal, mul_one] nth_rewrite 2 [deriv_physHermite_characteristic_length] ring_nf simp only [one_div, Complex.ofReal_inv, cast_add, cast_one, add_tsub_cancel_right] @@ -195,7 +194,7 @@ lemma deriv_deriv_eigenfunction (n : ℕ) (x : ℝ) : match n with | 0 => simpa using Q.deriv_deriv_eigenfunction_zero x | n + 1 => - trans Complex.ofReal (1/Real.sqrt (2 ^ (n + 1) * (n + 1) !) ) * + trans Complex.ofReal (1/Real.sqrt (2 ^ (n + 1) * (n + 1) !)) * (((- 1 / Q.ξ ^ 2) * (2 * (n + 1) + (1 + (- 1/ Q.ξ ^ 2) * x ^ 2)) * (physHermite (n + 1) (x/Q.ξ))) * Q.eigenfunction 0 x) @@ -223,7 +222,7 @@ lemma deriv_deriv_eigenfunction (n : ℕ) (x : ℝ) : trans (- 1/ Q.ξ^2) * (2 * (n + 1) * (2 * ((1 / Q.ξ) * x) * (physHermite n (x/Q.ξ)) - 2 * n * (physHermite (n - 1) (x/Q.ξ))) - + (1 + (- 1 / Q.ξ^2) * x ^ 2) * (physHermite (n + 1) ( x/Q.ξ))) + + (1 + (- 1 / Q.ξ^2) * x ^ 2) * (physHermite (n + 1) (x/Q.ξ))) · ring_nf trans (- 1 / Q.ξ^2) * (2 * (n + 1) * (physHermite (n + 1) (x/Q.ξ)) + (1 + (- 1/ Q.ξ^2) * x ^ 2) * (physHermite (n + 1) (x/Q.ξ))) diff --git a/PhysLean/QuantumMechanics/OneDimension/HilbertSpace/Basic.lean b/PhysLean/QuantumMechanics/OneDimension/HilbertSpace/Basic.lean index cf4716a..7bd586b 100644 --- a/PhysLean/QuantumMechanics/OneDimension/HilbertSpace/Basic.lean +++ b/PhysLean/QuantumMechanics/OneDimension/HilbertSpace/Basic.lean @@ -55,7 +55,7 @@ lemma memHS_iff {f : ℝ → ℂ} : MemHS f ↔ exact Continuous.comp_aestronglyMeasurable continuous_norm h1 simp only [h0, true_and] simp only [HasFiniteIntegral, enorm_pow] - simp only [enorm, nnnorm, Real.norm_eq_abs, abs_norm] + simp only [enorm, nnnorm, Real.norm_eq_abs, abs_norm] lemma aeEqFun_mk_mem_iff (f : ℝ → ℂ) (hf : AEStronglyMeasurable f volume) : AEEqFun.mk f hf ∈ HilbertSpace ↔ MemHS f := by diff --git a/PhysLean/Relativity/Lorentz/ComplexVector/Unit.lean b/PhysLean/Relativity/Lorentz/ComplexVector/Unit.lean index c35d712..849c2e2 100644 --- a/PhysLean/Relativity/Lorentz/ComplexVector/Unit.lean +++ b/PhysLean/Relativity/Lorentz/ComplexVector/Unit.lean @@ -143,11 +143,11 @@ lemma contr_contrCoUnit (x : complexCo) : Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, Finset.sum_singleton, Fin.sum_univ_three, tmul_add, add_tmul, smul_tmul, tmul_smul, map_add, _root_.map_smul] - have h1' (x y : complexCo.V) (z : complexContr.V) : + have h1' (x y : complexCo.V) (z : complexContr.V) : (α_ complexCo.V complexContr.V complexCo.V).inv (x ⊗ₜ[ℂ] z ⊗ₜ[ℂ] y) = (x ⊗ₜ[ℂ] z) ⊗ₜ[ℂ] y := rfl repeat rw [h1'] have h1'' (y : complexCo.V) - (z : complexCo.V ⊗[ℂ] complexContr.V) : + (z : complexCo.V ⊗[ℂ] complexContr.V) : (coContrContraction.hom ▷ complexCo.V) (z ⊗ₜ[ℂ] y) = (coContrContraction.hom z) ⊗ₜ[ℂ] y := rfl repeat rw (config := { transparency := .instances }) [h1''] repeat rw [coContrContraction_basis'] @@ -182,7 +182,7 @@ lemma contr_coContrUnit (x : complexContr) : (x ⊗ₜ[ℂ] z ⊗ₜ[ℂ] y) = (x ⊗ₜ[ℂ] z) ⊗ₜ[ℂ] y := rfl repeat rw [h1'] have h1'' (y : complexContr.V) - (z : complexContr.V ⊗[ℂ] complexCo.V) : + (z : complexContr.V ⊗[ℂ] complexCo.V) : (contrCoContraction.hom ▷ complexContr.V) (z ⊗ₜ[ℂ] y) = (contrCoContraction.hom z) ⊗ₜ[ℂ] y := rfl repeat rw (config := { transparency := .instances }) [h1''] diff --git a/PhysLean/Relativity/Lorentz/RealVector/Contraction.lean b/PhysLean/Relativity/Lorentz/RealVector/Contraction.lean index 900f07c..3f9b6c6 100644 --- a/PhysLean/Relativity/Lorentz/RealVector/Contraction.lean +++ b/PhysLean/Relativity/Lorentz/RealVector/Contraction.lean @@ -335,9 +335,7 @@ lemma _root_.LorentzGroup.mem_iff_norm : Λ ∈ LorentzGroup d ↔ apply e.injective have hp' := e.injective.eq_iff.mpr hp have hn' := e.injective.eq_iff.mpr hn - simp [Action.instMonoidalCategory_tensorUnit_V, Action.instMonoidalCategory_tensorObj_V, - Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor, - Action.FunctorCategoryEquivalence.functor_obj_obj, map_add, map_sub] at hp' hn' + simp only [Action.instMonoidalCategory_tensorUnit_V, map_add, map_sub] at hp' hn' linear_combination (norm := ring_nf) (1 / 4) * hp' + (-1/ 4) * hn' rw [symm (Λ *ᵥ y) (Λ *ᵥ x), symm y x] simp only [Action.instMonoidalCategory_tensorUnit_V] diff --git a/PhysLean/Relativity/Lorentz/SL2C/SelfAdjoint.lean b/PhysLean/Relativity/Lorentz/SL2C/SelfAdjoint.lean index c7b20a0..47cee44 100644 --- a/PhysLean/Relativity/Lorentz/SL2C/SelfAdjoint.lean +++ b/PhysLean/Relativity/Lorentz/SL2C/SelfAdjoint.lean @@ -72,8 +72,7 @@ $$\begin{align} \begin{vmatrix} \operatorname{Re}(x\bar{y}) & -\operatorname{Im}(x\bar{y}) \\ \operatorname{Im}(x\bar{y}) & \operatorname{Re}(x\bar{y}) -\end{vmatrix} \det\left( - \begin{bmatrix} \lvert x\rvert^2 & □ \\ 0 & \lvert y\rvert^2 \end{bmatrix} - +\end{vmatrix} \det\left(\begin{bmatrix} \lvert x\rvert^2 & □ \\ 0 & \lvert y\rvert^2 \end{bmatrix} - \begin{bmatrix} □ & □ \\ 0 & 0 \end{bmatrix} \begin{bmatrix} □ & □ \\ □ & □ \end{bmatrix} \begin{bmatrix} 0 & □ \\ 0 & □ \end{bmatrix} diff --git a/PhysLean/Relativity/Lorentz/Weyl/Unit.lean b/PhysLean/Relativity/Lorentz/Weyl/Unit.lean index b366e2d..0669238 100644 --- a/PhysLean/Relativity/Lorentz/Weyl/Unit.lean +++ b/PhysLean/Relativity/Lorentz/Weyl/Unit.lean @@ -190,8 +190,7 @@ def altRightRightUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altRightHanded ⊗ rightHa refine ModuleCat.hom_ext ?_ refine LinearMap.ext fun x : ℂ => ?_ simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, - Action.tensorUnit_ρ - , CategoryTheory.Category.id_comp, Action.tensor_ρ, ModuleCat.hom_comp, + Action.tensorUnit_ρ, CategoryTheory.Category.id_comp, Action.tensor_ρ, ModuleCat.hom_comp, Function.comp_apply] change x • altRightRightUnitVal = (TensorProduct.map (altRightHanded.ρ M) (rightHanded.ρ M)) (x • altRightRightUnitVal) diff --git a/PhysLean/Relativity/Tensors/Tree/Elab.lean b/PhysLean/Relativity/Tensors/Tree/Elab.lean index d42f60f..689773f 100644 --- a/PhysLean/Relativity/Tensors/Tree/Elab.lean +++ b/PhysLean/Relativity/Tensors/Tree/Elab.lean @@ -380,7 +380,7 @@ partial def getContrPos (stx : Syntax) : TermElabM (List (ℕ × ℕ)) := do let ind ← getIndices stx let indFilt : List (TSyntax `indexExpr) := ind.filter (fun x => ¬ indexExprIsNum x) let indEnum := indFilt.zipIdx - let bind := List.flatMap (fun a => indEnum.map (fun b => (a, b))) indEnum + let bind := List.flatMap (fun a => indEnum.map (fun b => (a, b))) indEnum let filt ← bind.filterMapM (fun x => indexPosEq x.1 x.2) if ¬ ((filt.map Prod.fst).Nodup ∧ (filt.map Prod.snd).Nodup) then throwError "To many contractions" diff --git a/scripts/hepLean_style_lint.lean b/scripts/hepLean_style_lint.lean index a02fd5a..3de6a34 100644 --- a/scripts/hepLean_style_lint.lean +++ b/scripts/hepLean_style_lint.lean @@ -31,9 +31,9 @@ def PhysLeanTextLinter : Type := Array String → Array (String × ℕ × ℕ) /-- Checks if there are two consecutive empty lines. -/ def doubleEmptyLineLinter : PhysLeanTextLinter := fun lines ↦ Id.run do - let enumLines := (lines.toList.enumFrom 1) + let enumLines := (lines.toList.zipIdx 1) let pairLines := List.zip enumLines (List.tail! enumLines) - let errors := pairLines.filterMap (fun ((lno1, l1), _, l2) ↦ + let errors := pairLines.filterMap (fun ((l1, lno1), l2, _) ↦ if l1.length == 0 && l2.length == 0 then some (s!" Double empty line. ", lno1, 1) else none) @@ -41,8 +41,8 @@ def doubleEmptyLineLinter : PhysLeanTextLinter := fun lines ↦ Id.run do /-- Checks if there is a double space in the line, which is not at the start. -/ def doubleSpaceLinter : PhysLeanTextLinter := fun lines ↦ Id.run do - let enumLines := (lines.toList.enumFrom 1) - let errors := enumLines.filterMap (fun (lno, l) ↦ + let enumLines := (lines.toList.zipIdx 1) + let errors := enumLines.filterMap (fun (l, lno) ↦ if String.containsSubstr l.trimLeft " " then let k := (Substring.findAllSubstr l " ").toList.getLast? let col := match k with @@ -53,8 +53,8 @@ def doubleSpaceLinter : PhysLeanTextLinter := fun lines ↦ Id.run do errors.toArray def longLineLinter : PhysLeanTextLinter := fun lines ↦ Id.run do - let enumLines := (lines.toList.enumFrom 1) - let errors := enumLines.filterMap (fun (lno, l) ↦ + let enumLines := (lines.toList.zipIdx 1) + let errors := enumLines.filterMap (fun (l, lno) ↦ if l.length > 100 ∧ ¬ String.containsSubstr l "http" then some (s!" Line is too long.", lno, 100) else none) @@ -62,8 +62,8 @@ def longLineLinter : PhysLeanTextLinter := fun lines ↦ Id.run do /-- Substring linter. -/ def substringLinter (s : String) : PhysLeanTextLinter := fun lines ↦ Id.run do - let enumLines := (lines.toList.enumFrom 1) - let errors := enumLines.filterMap (fun (lno, l) ↦ + let enumLines := (lines.toList.zipIdx 1) + let errors := enumLines.filterMap (fun (l, lno) ↦ if String.containsSubstr l s then let k := (Substring.findAllSubstr l s).toList.getLast? let col := match k with @@ -74,8 +74,8 @@ def substringLinter (s : String) : PhysLeanTextLinter := fun lines ↦ Id.run do errors.toArray def endLineLinter (s : String) : PhysLeanTextLinter := fun lines ↦ Id.run do - let enumLines := (lines.toList.enumFrom 1) - let errors := enumLines.filterMap (fun (lno, l) ↦ + let enumLines := (lines.toList.zipIdx 1) + let errors := enumLines.filterMap (fun (l, lno) ↦ if l.endsWith s then some (s!" Line ends with `{s}`.", lno, l.length) else none) @@ -83,8 +83,8 @@ def endLineLinter (s : String) : PhysLeanTextLinter := fun lines ↦ Id.run do /-- Number of space at new line must be even. -/ def numInitialSpacesEven : PhysLeanTextLinter := fun lines ↦ Id.run do - let enumLines := (lines.toList.enumFrom 1) - let errors := enumLines.filterMap (fun (lno, l) ↦ + let enumLines := (lines.toList.zipIdx 1) + let errors := enumLines.filterMap (fun (l, lno) ↦ let numSpaces := (l.takeWhile (· == ' ')).length if numSpaces % 2 != 0 then some (s!"Number of initial spaces is not even.", lno, 1)