From 12a568b45f49fe5ce1d5aa90bf883651b49cd886 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Fri, 19 Apr 2024 10:08:56 -0400
Subject: [PATCH] refactor: Lint

---
 HepLean.lean                                  |  3 +++
 HepLean/AnomalyCancellation/LinearMaps.lean   |  3 ++-
 .../SMNu/Ordinary/DimSevenPlane.lean          | 25 ++++++++++++-------
 .../SMNu/PlusU1/BoundPlaneDim.lean            | 10 +++++++-
 .../SMNu/PlusU1/PlaneNonSols.lean             | 16 ++++++++++--
 5 files changed, 44 insertions(+), 13 deletions(-)

diff --git a/HepLean.lean b/HepLean.lean
index 9b65669c..5e92471c 100644
--- a/HepLean.lean
+++ b/HepLean.lean
@@ -36,11 +36,14 @@ import HepLean.AnomalyCancellation.SMNu.Basic
 import HepLean.AnomalyCancellation.SMNu.FamilyMaps
 import HepLean.AnomalyCancellation.SMNu.NoGrav.Basic
 import HepLean.AnomalyCancellation.SMNu.Ordinary.Basic
+import HepLean.AnomalyCancellation.SMNu.Ordinary.DimSevenPlane
 import HepLean.AnomalyCancellation.SMNu.Ordinary.FamilyMaps
 import HepLean.AnomalyCancellation.SMNu.Permutations
 import HepLean.AnomalyCancellation.SMNu.PlusU1.BMinusL
 import HepLean.AnomalyCancellation.SMNu.PlusU1.Basic
+import HepLean.AnomalyCancellation.SMNu.PlusU1.BoundPlaneDim
 import HepLean.AnomalyCancellation.SMNu.PlusU1.FamilyMaps
 import HepLean.AnomalyCancellation.SMNu.PlusU1.HyperCharge
+import HepLean.AnomalyCancellation.SMNu.PlusU1.PlaneNonSols
 import HepLean.AnomalyCancellation.SMNu.PlusU1.QuadSol
 import HepLean.AnomalyCancellation.SMNu.PlusU1.QuadSolToSol
diff --git a/HepLean/AnomalyCancellation/LinearMaps.lean b/HepLean/AnomalyCancellation/LinearMaps.lean
index 13712cce..2147ac26 100644
--- a/HepLean/AnomalyCancellation/LinearMaps.lean
+++ b/HepLean/AnomalyCancellation/LinearMaps.lean
@@ -149,7 +149,7 @@ lemma map_add₂ (f : BiLinearSymm V) (S : V) (T1 T2 : V) :
     f (S, T1 + T2) = f (S, T1) + f (S, T2) := by
   rw [f.swap, f.map_add₁, f.swap T1 S, f.swap T2 S]
 
-
+/-- Fixing the second input vectors, the resulting linear map. -/
 def toLinear₁  (f : BiLinearSymm V) (T : V) : V →ₗ[ℚ] ℚ where
   toFun S := f (S, T)
   map_add' S1 S2 := by
@@ -301,6 +301,7 @@ lemma map_add₃ (f : TriLinearSymm V) (S T L1 L2 : V) :
     f (S, T, L1 + L2) = f (S, T, L1) + f (S, T, L2) := by
   rw [f.swap₃, f.map_add₁, f.swap₃, f.swap₃ L2 T S]
 
+/-- Fixing the second and third input vectors, the resulting linear map. -/
 def toLinear₁  (f : TriLinearSymm V) (T L : V) : V →ₗ[ℚ] ℚ where
   toFun S := f (S, T, L)
   map_add' S1 S2 := by
diff --git a/HepLean/AnomalyCancellation/SMNu/Ordinary/DimSevenPlane.lean b/HepLean/AnomalyCancellation/SMNu/Ordinary/DimSevenPlane.lean
index 08d14abc..d2806a7b 100644
--- a/HepLean/AnomalyCancellation/SMNu/Ordinary/DimSevenPlane.lean
+++ b/HepLean/AnomalyCancellation/SMNu/Ordinary/DimSevenPlane.lean
@@ -23,7 +23,7 @@ open BigOperators
 
 namespace PlaneSeven
 
-
+/-- A charge assignment forming one of the basis elements of the plane. -/
 def B₀ : (SM 3).charges := toSpeciesEquiv.invFun ( fun s => fun i =>
   match s, i with
   | 0, 0 => 1
@@ -36,6 +36,7 @@ lemma B₀_cubic (S T : (SM 3).charges) : cubeTriLin (B₀, S, T) =
   simp [Fin.sum_univ_three, B₀, Fin.divNat, Fin.modNat, finProdFinEquiv]
   ring
 
+/-- A charge assignment forming one of the basis elements of the plane. -/
 def B₁ : (SM 3).charges := toSpeciesEquiv.invFun ( fun s => fun i =>
   match s, i with
   | 1, 0 => 1
@@ -48,6 +49,7 @@ lemma B₁_cubic (S T : (SM 3).charges) : cubeTriLin (B₁, S, T) =
   simp [Fin.sum_univ_three, B₁, Fin.divNat, Fin.modNat, finProdFinEquiv]
   ring
 
+/-- A charge assignment forming one of the basis elements of the plane. -/
 def B₂ : (SM 3).charges := toSpeciesEquiv.invFun ( fun s => fun i =>
   match s, i with
   | 2, 0 => 1
@@ -60,6 +62,7 @@ lemma B₂_cubic (S T : (SM 3).charges) : cubeTriLin (B₂, S, T) =
   simp [Fin.sum_univ_three, B₂, Fin.divNat, Fin.modNat, finProdFinEquiv]
   ring
 
+/-- A charge assignment forming one of the basis elements of the plane. -/
 def B₃ : (SM 3).charges := toSpeciesEquiv.invFun ( fun s => fun i =>
   match s, i with
   | 3, 0 => 1
@@ -73,6 +76,7 @@ lemma B₃_cubic (S T : (SM 3).charges) : cubeTriLin (B₃, S, T) =
   ring_nf
   rfl
 
+/-- A charge assignment forming one of the basis elements of the plane. -/
 def B₄ : (SM 3).charges := toSpeciesEquiv.invFun ( fun s => fun i =>
   match s, i with
   | 4, 0 => 1
@@ -86,6 +90,7 @@ lemma B₄_cubic (S T : (SM 3).charges) : cubeTriLin (B₄, S, T) =
   ring_nf
   rfl
 
+/-- A charge assignment forming one of the basis elements of the plane. -/
 def B₅ : (SM 3).charges := toSpeciesEquiv.invFun ( fun s => fun i =>
   match s, i with
   | 5, 0 => 1
@@ -99,6 +104,7 @@ lemma B₅_cubic (S T : (SM 3).charges) : cubeTriLin (B₅, S, T) =
   ring_nf
   rfl
 
+/-- A charge assignment forming one of the basis elements of the plane. -/
 def B₆ : (SM 3).charges := toSpeciesEquiv.invFun ( fun s => fun i =>
   match s, i with
   | 1, 2 => 1
@@ -111,6 +117,7 @@ lemma B₆_cubic (S T : (SM 3).charges) : cubeTriLin (B₆, S, T) =
   simp [Fin.sum_univ_three, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
   ring_nf
 
+/-- The charge assignments forming a basis of the plane. -/
 @[simp]
 def B : Fin 7 → (SM 3).charges := fun i =>
   match i with
@@ -191,49 +198,49 @@ lemma Bi_Bj_ne_cubic {i j : Fin 7} (h : i ≠ j) (S : (SM 3).charges) :
   exact B₆_Bi_cubic h S
 
 lemma B₀_B₀_Bi_cubic {i : Fin 7} :
-  cubeTriLin (B 0, B 0, B i) = 0 := by
+    cubeTriLin (B 0, B 0, B i) = 0 := by
   change cubeTriLin (B₀, B₀, B i) = 0
   rw [B₀_cubic]
   fin_cases i <;>
   simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
 
 lemma B₁_B₁_Bi_cubic {i : Fin 7} :
-  cubeTriLin (B 1, B 1, B i) = 0 := by
+    cubeTriLin (B 1, B 1, B i) = 0 := by
   change cubeTriLin (B₁, B₁, B i) = 0
   rw [B₁_cubic]
   fin_cases i <;>
   simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
 
 lemma B₂_B₂_Bi_cubic {i : Fin 7} :
-  cubeTriLin (B 2, B 2, B i) = 0 := by
+    cubeTriLin (B 2, B 2, B i) = 0 := by
   change cubeTriLin (B₂, B₂, B i) = 0
   rw [B₂_cubic]
   fin_cases i <;>
   simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
 
 lemma B₃_B₃_Bi_cubic {i : Fin 7} :
-  cubeTriLin (B 3, B 3, B i) = 0 := by
+    cubeTriLin (B 3, B 3, B i) = 0 := by
   change cubeTriLin (B₃, B₃, B i) = 0
   rw [B₃_cubic]
   fin_cases i <;>
   simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
 
 lemma B₄_B₄_Bi_cubic {i : Fin 7} :
-  cubeTriLin (B 4, B 4, B i) = 0 := by
+    cubeTriLin (B 4, B 4, B i) = 0 := by
   change cubeTriLin (B₄, B₄, B i) = 0
   rw [B₄_cubic]
   fin_cases i <;>
   simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
 
 lemma B₅_B₅_Bi_cubic {i : Fin 7} :
-  cubeTriLin (B 5, B 5, B i) = 0 := by
+    cubeTriLin (B 5, B 5, B i) = 0 := by
   change cubeTriLin (B₅, B₅, B i) = 0
   rw [B₅_cubic]
   fin_cases i <;>
   simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
 
 lemma B₆_B₆_Bi_cubic {i : Fin 7} :
-  cubeTriLin (B 6, B 6, B i) = 0 := by
+    cubeTriLin (B 6, B 6, B i) = 0 := by
   change cubeTriLin (B₆, B₆, B i) = 0
   rw [B₆_cubic]
   fin_cases i <;>
@@ -241,7 +248,7 @@ lemma B₆_B₆_Bi_cubic {i : Fin 7} :
 
 
 lemma Bi_Bi_Bj_cubic (i j : Fin 7) :
-  cubeTriLin (B i, B i, B j) = 0 := by
+    cubeTriLin (B i, B i, B j) = 0 := by
   fin_cases i
   exact B₀_B₀_Bi_cubic
   exact B₁_B₁_Bi_cubic
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean
index b2701f83..a116fa51 100644
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean
@@ -6,7 +6,13 @@ Authors: Joseph Tooby-Smith
 import HepLean.AnomalyCancellation.SMNu.PlusU1.Basic
 import HepLean.AnomalyCancellation.SMNu.PlusU1.FamilyMaps
 import HepLean.AnomalyCancellation.SMNu.PlusU1.PlaneNonSols
+/-!
+# Bound on plane dimension
 
+We place an upper bound on the dimension of a plane of charges on which every point is a solution.
+The upper bound is 7, proven in the theorem `plane_exists_dim_le_7`.
+
+-/
 universe v u
 
 namespace SMRHN
@@ -16,6 +22,8 @@ open SMνCharges
 open SMνACCs
 open BigOperators
 
+/-- A proposition which is true if for a given `n` a plane of charges of dimension `n` exists
+in which each point is a solution. -/
 def existsPlane (n : ℕ) : Prop := ∃ (B : Fin n → (PlusU1 3).charges),
    LinearIndependent ℚ B ∧ ∀ (f : Fin n → ℚ), (PlusU1 3).isSolution (∑ i, f i • B i)
 
@@ -33,7 +41,7 @@ lemma exists_plane_exists_basis {n : ℕ} (hE : existsPlane n) :
   have h1 : ∑ x : Fin n, -(g (Sum.inr x) • Y (Sum.inr x)) =
       ∑ x : Fin n, (-g (Sum.inr x)) • Y (Sum.inr x):= by
     apply Finset.sum_congr
-    simp
+    simp only
     intro i _
     simp
   rw [h1] at hg
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/PlaneNonSols.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/PlaneNonSols.lean
index 9252076c..98e74a09 100644
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/PlaneNonSols.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/PlaneNonSols.lean
@@ -26,28 +26,40 @@ open BigOperators
 
 namespace ElevenPlane
 
+/-- A charge assignment forming one of the basis elements of the plane. -/
 def B₀ : (PlusU1 3).charges := ![1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
 
+/-- A charge assignment forming one of the basis elements of the plane. -/
 def B₁ : (PlusU1 3).charges := ![0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
 
+/-- A charge assignment forming one of the basis elements of the plane. -/
 def B₂ : (PlusU1 3).charges := ![0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
 
+/-- A charge assignment forming one of the basis elements of the plane. -/
 def B₃ : (PlusU1 3).charges := ![0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
 
+/-- A charge assignment forming one of the basis elements of the plane. -/
 def B₄ : (PlusU1 3).charges := ![0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
 
+/-- A charge assignment forming one of the basis elements of the plane. -/
 def B₅ : (PlusU1 3).charges := ![0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0]
 
+/-- A charge assignment forming one of the basis elements of the plane. -/
 def B₆ : (PlusU1 3).charges := ![0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0]
 
+/-- A charge assignment forming one of the basis elements of the plane. -/
 def B₇ : (PlusU1 3).charges := ![0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0]
 
+/-- A charge assignment forming one of the basis elements of the plane. -/
 def B₈  : (PlusU1 3).charges := ![0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0]
 
+/-- A charge assignment forming one of the basis elements of the plane. -/
 def B₉ : (PlusU1 3).charges := ![0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 2, 0]
 
+/-- A charge assignment forming one of the basis elements of the plane. -/
 def B₁₀ : (PlusU1 3).charges := ![0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1]
 
+/-- The charge assignment forming a basis of the plane. -/
 def B : Fin 11 → (PlusU1 3).charges := fun i =>
   match i with
   | 0 => B₀
@@ -76,7 +88,7 @@ lemma Bi_sum_quad (i : Fin 11) (f : Fin 11 → ℚ) :
   rw [quadBiLin.map_smul₂, Bi_Bj_quad hij.symm]
   simp
 
-
+/-- The coefficents of the quadratic equation in our basis. -/
 @[simp]
 def quadCoeff : Fin 11 → ℚ := ![1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0]
 
@@ -102,7 +114,7 @@ lemma isSolution_quadCoeff_f_sq_zero (f : Fin 11 → ℚ) (hS : (PlusU1 3).isSol
   rw [Fintype.sum_eq_zero_iff_of_nonneg] at hQ
   exact congrFun hQ k
   intro i
-  simp
+  simp only [Pi.zero_apply, quadCoeff]
   rw [mul_nonneg_iff]
   apply Or.inl
   apply And.intro