From 869a9925ef1de69264e058f7b3c294e6b05389c3 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Thu, 20 Mar 2025 09:06:23 -0400
Subject: [PATCH] refactor: lint

---
 PhysLean/Electromagnetism/Basic.lean              |  1 +
 .../FieldStrength/Derivative.lean                 | 15 ++++++++++-----
 PhysLean/Electromagnetism/MaxwellEquations.lean   |  6 ++++--
 .../Relativity/Lorentz/RealTensor/Derivative.lean |  6 ++++--
 PhysLean/Relativity/SpaceTime/Basic.lean          |  2 ++
 5 files changed, 21 insertions(+), 9 deletions(-)

diff --git a/PhysLean/Electromagnetism/Basic.lean b/PhysLean/Electromagnetism/Basic.lean
index 8e44563..5ccdc96 100644
--- a/PhysLean/Electromagnetism/Basic.lean
+++ b/PhysLean/Electromagnetism/Basic.lean
@@ -27,4 +27,5 @@ open realLorentzTensor
 
 /-- The vector potential of an electromagnetic field-/
 abbrev VectorPotential (d : ℕ := 3) := SpaceTime d → ℝT[d, .up]
+
 end Electromagnetism
diff --git a/PhysLean/Electromagnetism/FieldStrength/Derivative.lean b/PhysLean/Electromagnetism/FieldStrength/Derivative.lean
index 5d4941a..c4f171a 100644
--- a/PhysLean/Electromagnetism/FieldStrength/Derivative.lean
+++ b/PhysLean/Electromagnetism/FieldStrength/Derivative.lean
@@ -25,8 +25,11 @@ open IndexNotation
 open TensorSpecies.TensorBasis in
 private lemma finsupp_single_prodEquiv (b : (j : Fin (Nat.succ 0 + (Nat.succ 0).succ)) →
       Fin (realLorentzTensor.repDim
-        ((Sum.elim (fun (i : Fin 1) => realLorentzTensor.τ (![Color.up] i)) ![Color.up, Color.up] ∘ ⇑finSumFinEquiv.symm) j))) :
-      (Finsupp.single (fun i => Fin.cast (by simp : realLorentzTensor.repDim (realLorentzTensor.τ (![Color.up] i)) = realLorentzTensor.repDim (![Color.up] i)) ((prodEquiv b).1 i)) (1 : ℝ)) =
+        ((Sum.elim (fun (i : Fin 1) => realLorentzTensor.τ (![Color.up] i))
+          ![Color.up, Color.up] ∘ ⇑finSumFinEquiv.symm) j))) :
+      (Finsupp.single (fun i => Fin.cast
+        (by simp : realLorentzTensor.repDim (realLorentzTensor.τ (![Color.up] i)) =
+        realLorentzTensor.repDim (![Color.up] i)) ((prodEquiv b).1 i)) (1 : ℝ)) =
       (Finsupp.single (fun | 0 => b 0) 1) := by
   congr
   funext x
@@ -35,7 +38,8 @@ private lemma finsupp_single_prodEquiv (b : (j : Fin (Nat.succ 0 + (Nat.succ 0).
 
 private lemma mapTobasis_prodEquiv (b : (j : Fin (Nat.succ 0 + (Nat.succ 0).succ)) →
     Fin (realLorentzTensor.repDim
-      ((Sum.elim  (fun (i : Fin 1) => realLorentzTensor.τ (![Color.up] i)) ![Color.up, Color.up] ∘ ⇑finSumFinEquiv.symm) j))) :
+      ((Sum.elim (fun (i : Fin 1) => realLorentzTensor.τ (![Color.up] i))
+        ![Color.up, Color.up] ∘ ⇑finSumFinEquiv.symm) j))) :
     (fun y => mapToBasis (↑(toElectricMagneticField.symm EM)) y
       (TensorSpecies.TensorBasis.prodEquiv b).2)
     = (fun y => mapToBasis ((toElectricMagneticField.symm EM).1) y
@@ -46,6 +50,7 @@ private lemma mapTobasis_prodEquiv (b : (j : Fin (Nat.succ 0 + (Nat.succ 0).succ
   fin_cases x
   · rfl
   · rfl
+
 lemma derivative_fromElectricMagneticField_repr_diag (EM : ElectricField × MagneticField)
     (hdiff :Differentiable ℝ (mapToBasis (toElectricMagneticField.symm EM).1))
     (y : SpaceTime) (j : ℕ) (hj : j < 4) :
@@ -56,7 +61,7 @@ lemma derivative_fromElectricMagneticField_repr_diag (EM : ElectricField × Magn
       (Finsupp.equivFunOnFinite ((realLorentzTensor.tensorBasis _).repr y)) := by
       exact hdiff (Finsupp.equivFunOnFinite ((realLorentzTensor.tensorBasis ![Color.up]).repr y))
   conv_lhs => erw [derivative_repr _ _ _ h_diff]
-  simp only [ Nat.reduceAdd, C_eq_color, Fin.isValue]
+  simp only [Nat.reduceAdd, C_eq_color, Fin.isValue]
   rw [finsupp_single_prodEquiv]
   rw [mapTobasis_prodEquiv]
   trans SpaceTime.deriv μ (fun y => 0) y
@@ -135,7 +140,7 @@ lemma derivative_fromElectricMagneticField_repr_zero_col (EM : ElectricField ×
     simp
 
 lemma derivative_fromElectricMagneticField_repr_one_two (EM : ElectricField × MagneticField)
-    (hdiff :Differentiable ℝ (mapToBasis (toElectricMagneticField.symm EM).1))
+    (hdiff : Differentiable ℝ (mapToBasis (toElectricMagneticField.symm EM).1))
     (y : SpaceTime) :
     (realLorentzTensor.tensorBasis _).repr (∂ (fromElectricMagneticField EM).1 y)
     (fun | 0 => μ | 1 => ⟨1, by simp⟩ | 2 => ⟨2, by simp⟩) =
diff --git a/PhysLean/Electromagnetism/MaxwellEquations.lean b/PhysLean/Electromagnetism/MaxwellEquations.lean
index df14e3b..9260a36 100644
--- a/PhysLean/Electromagnetism/MaxwellEquations.lean
+++ b/PhysLean/Electromagnetism/MaxwellEquations.lean
@@ -13,6 +13,8 @@ import PhysLean.Relativity.SpaceTime.Basic
 
 namespace Electromagnetism
 
+/-- An electromagnetic system consists of charge density, a current density,
+  the speed ofl light and the electric permittivity. -/
 structure EMSystem where
   /-- The charge density. -/
   ρ : SpaceTime → ℝ
@@ -48,7 +50,7 @@ def GaussLawMagnetic (B : MagneticField) : Prop :=
 
 /-- Faraday's law. -/
 def FaradayLaw (E : ElectricField) (B : MagneticField) : Prop :=
-  ∀ x : SpaceTime, ∇× B x =  μ₀ • (J x + ε₀ • ∂ₜ E x )
+  ∀ x : SpaceTime, ∇× B x = μ₀ • (J x + ε₀ • ∂ₜ E x)
 
 /-- Ampère's law. -/
 def AmpereLaw (E : ElectricField) (B : MagneticField) : Prop :=
@@ -57,7 +59,7 @@ def AmpereLaw (E : ElectricField) (B : MagneticField) : Prop :=
 /-- Maxwell's equations. -/
 def MaxwellEquations (E : ElectricField) (B : MagneticField) : Prop :=
   𝓔.GaussLawElectric E ∧ GaussLawMagnetic B ∧
-  𝓔.FaradayLaw  E B ∧ AmpereLaw E B
+  𝓔.FaradayLaw E B ∧ AmpereLaw E B
 
 end EMSystem
 end Electromagnetism
diff --git a/PhysLean/Relativity/Lorentz/RealTensor/Derivative.lean b/PhysLean/Relativity/Lorentz/RealTensor/Derivative.lean
index 336b42b..89087b0 100644
--- a/PhysLean/Relativity/Lorentz/RealTensor/Derivative.lean
+++ b/PhysLean/Relativity/Lorentz/RealTensor/Derivative.lean
@@ -33,7 +33,8 @@ noncomputable def mapToBasis {d n m : ℕ} {cm : Fin m → (realLorentzTensor d)
     `ℝT(d, cm) → ℝT(d, (Sum.elim cm cn) ∘ finSumFinEquiv.symm)`. -/
 noncomputable def derivative {d n m : ℕ} {cm : Fin m → (realLorentzTensor d).C}
     {cn : Fin n → (realLorentzTensor d).C} (f : ℝT(d, cm) → ℝT(d, cn)) :
-    ℝT(d, cm) → ℝT(d, (Sum.elim (fun i => (realLorentzTensor d).τ (cm i)) cn) ∘ finSumFinEquiv.symm) := fun y =>
+    ℝT(d, cm) → ℝT(d, (Sum.elim (fun i => (realLorentzTensor d).τ (cm i)) cn) ∘
+      finSumFinEquiv.symm) := fun y =>
       ((realLorentzTensor d).tensorBasis _).repr.toEquiv.symm <|
       Finsupp.equivFunOnFinite.symm <| fun b =>
   /- The `b` componenet of the derivative of `f` evaluated at `y` is: -/
@@ -54,7 +55,8 @@ lemma derivative_repr {d n m : ℕ} {cm : Fin m → (realLorentzTensor d).C}
     {cn : Fin n → (realLorentzTensor d).C} (f : ℝT(d, cm) → ℝT(d, cn))
     (y : ℝT(d, cm))
     (b : (j : Fin (m + n)) →
-      Fin ((realLorentzTensor d).repDim ((((fun i => (realLorentzTensor d).τ (cm i)) ⊕ᵥ cn) ∘ ⇑finSumFinEquiv.symm) j)))
+      Fin ((realLorentzTensor d).repDim
+      ((((fun i => (realLorentzTensor d).τ (cm i)) ⊕ᵥ cn) ∘ ⇑finSumFinEquiv.symm) j)))
     (h1 : DifferentiableAt ℝ (mapToBasis f)
       (Finsupp.equivFunOnFinite (((realLorentzTensor d).tensorBasis cm).repr y))) :
     ((realLorentzTensor d).tensorBasis _).repr (∂ f y) b =
diff --git a/PhysLean/Relativity/SpaceTime/Basic.lean b/PhysLean/Relativity/SpaceTime/Basic.lean
index 44f2aaf..22cf9bc 100644
--- a/PhysLean/Relativity/SpaceTime/Basic.lean
+++ b/PhysLean/Relativity/SpaceTime/Basic.lean
@@ -83,7 +83,9 @@ noncomputable def deriv {M : Type} [AddCommGroup M] [Module ℝ M] [TopologicalS
 @[inherit_doc deriv]
 scoped notation "∂_" => deriv
 
+/-- The derivative with respect to time. -/
 scoped notation "∂ₜ" => deriv 0
+
 lemma deriv_eq {d : ℕ} (μ : Fin (1 + d)) (f : SpaceTime d → ℝ) (y : SpaceTime d) :
     SpaceTime.deriv μ f y =
     fderiv ℝ f y ((realLorentzTensor d).tensorBasis _ (fun x => Fin.cast (by simp) μ)) := by