refactor: Lint

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
 
-
 -/

PhysLean/Optics/Basic.lean

@@ -18,5 +18,4 @@ Some directories which are NOT currently place holders are:
 - Quantum Mechanics
 - Relativity
 
-
 -/

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

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
 

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`. -/

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

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]

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.ξ))  *
+    _ = (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
+        (physHermite n (x / Q.ξ) * physHermite p (x / Q.ξ)) * (Real.exp (- x^2 / Q.ξ^2)) := by
       congr 1
       · congr 1
         · congr 1

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.ξ)))

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

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'']

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,
+  simp only [Action.instMonoidalCategory_tensorUnit_V, map_add, map_sub] at hp' hn'
-    Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
-    Action.FunctorCategoryEquivalence.functor_obj_obj, 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]

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(
+\end{vmatrix} \det\left(\begin{bmatrix} \lvert x\rvert^2 & □ \\ 0 & \lvert y\rvert^2 \end{bmatrix} -
-  \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}

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_ρ
+      Action.tensorUnit_ρ, CategoryTheory.Category.id_comp, Action.tensor_ρ, ModuleCat.hom_comp,
-      , CategoryTheory.Category.id_comp, Action.tensor_ρ, ModuleCat.hom_comp,
       Function.comp_apply]
     change x • altRightRightUnitVal =
       (TensorProduct.map (altRightHanded.ρ M) (rightHanded.ρ M)) (x • altRightRightUnitVal)

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"

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 enumLines := (lines.toList.zipIdx 1)
-  let errors := enumLines.filterMap (fun (lno, l) ↦
+  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 enumLines := (lines.toList.zipIdx 1)
-  let errors := enumLines.filterMap (fun (lno, l) ↦
+  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 enumLines := (lines.toList.zipIdx 1)
-  let errors := enumLines.filterMap (fun (lno, l) ↦
+  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 enumLines := (lines.toList.zipIdx 1)
-  let errors := enumLines.filterMap (fun (lno, l) ↦
+  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 enumLines := (lines.toList.zipIdx 1)
-  let errors := enumLines.filterMap (fun (lno, l) ↦
+  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)