Merge pull request #135 from HEPLean/pitmonticone/golf

refactor: golf
2024-09-01 14:55:08 -04:00 · 2024-09-01 14:55:08 -04:00 · cb661e1612
commit cb661e1612
parent 86b3b8acd6 72f3992eaf
10 changed files with 45 additions and 110 deletions
--- a/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean
@ -74,8 +74,7 @@ lemma sum_δ₁_δ₂ (S : Fin (2 * n.succ) → ℚ) :
    · intro i
      simp only [mem_univ, Fin.symm_castOrderIso, RelIso.coe_fn_toEquiv]
    · exact fun _ _=> rfl
-  rw [h1]
-  rw [Fin.sum_univ_add, Finset.sum_add_distrib]
+  rw [h1, Fin.sum_univ_add, Finset.sum_add_distrib]
  rfl

 lemma sum_δ₁_δ₂' (S : Fin (2 * n.succ) → ℚ) :
@ -85,8 +84,7 @@ lemma sum_δ₁_δ₂' (S : Fin (2 * n.succ) → ℚ) :
    · intro i
      simp only [mem_univ, Fin.symm_castOrderIso, RelIso.coe_fn_toEquiv]
    · exact fun _ _ => rfl
-  rw [h1]
-  rw [Fin.sum_univ_add, Finset.sum_add_distrib]
+  rw [h1, Fin.sum_univ_add, Finset.sum_add_distrib]
  rfl

 lemma sum_δ!₁_δ!₂ (S : Fin (2 * n.succ) → ℚ) :
--- a/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
+++ b/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
@ -162,12 +162,8 @@ def bijectionQEZero : {S : linearParameters // S.Q' ≠ 0 ∧ S.E' ≠ 0} ≃
    {S : (SMNoGrav 1).LinSols // Q S.val (0 : Fin 1) ≠ 0 ∧ E S.val (0 : Fin 1) ≠ 0} where
  toFun S := ⟨bijection S, S.2⟩
  invFun S := ⟨bijection.symm S, S.2⟩
-  left_inv S := by
-    apply Subtype.ext
-    exact bijection.left_inv S.1
-  right_inv S := by
-    apply Subtype.ext
-    exact bijection.right_inv S.1
+  left_inv S := Subtype.ext (bijection.left_inv S.1)
+  right_inv S := Subtype.ext (bijection.right_inv S.1)

 lemma grav (S : linearParameters) :
    accGrav S.asCharges = 0 ↔ S.E' = 6 * S.Q' := by
--- a/HepLean/AnomalyCancellation/SMNu/Ordinary/Basic.lean
+++ b/HepLean/AnomalyCancellation/SMNu/Ordinary/Basic.lean
@ -10,7 +10,6 @@ import HepLean.AnomalyCancellation.GroupActions
 # ACC system for SM with RHN (without hypercharge).

 We define the ACC system for the Standard Model (without hypercharge) with right-handed neutrinos.
-
 -/

 universe v u
@ -29,9 +28,7 @@ def SM (n : ℕ) : ACCSystem where
    | 1 => accSU2
    | 2 => accSU3
  numberQuadratic := 0
-  quadraticACCs := by
-    intro i
-    exact Fin.elim0 i
+  quadraticACCs := fun i ↦ Fin.elim0 i
  cubicACC := accCube

 namespace SM
--- a/HepLean/AnomalyCancellation/SMNu/Ordinary/DimSevenPlane.lean
+++ b/HepLean/AnomalyCancellation/SMNu/Ordinary/DimSevenPlane.lean
@ -259,21 +259,14 @@ lemma Bi_Bj_Bk_cubic (i j k : Fin 7) :
 theorem B_in_accCube (f : Fin 7 → ℚ) : accCube (∑ i, f i • B i) = 0 := by
  change cubeTriLin _ _ _ = 0
  rw [cubeTriLin.map_sum₁₂₃]
-  apply Fintype.sum_eq_zero
-  intro i
-  apply Fintype.sum_eq_zero
-  intro k
-  apply Fintype.sum_eq_zero
-  intro l
-  rw [cubeTriLin.map_smul₁, cubeTriLin.map_smul₂, cubeTriLin.map_smul₃]
-  rw [Bi_Bj_Bk_cubic]
+  apply Fintype.sum_eq_zero _ fun i ↦ Fintype.sum_eq_zero _ fun k ↦ Fintype.sum_eq_zero _ fun l ↦ ?_
+  rw [cubeTriLin.map_smul₁, cubeTriLin.map_smul₂, cubeTriLin.map_smul₃, Bi_Bj_Bk_cubic]
  simp

 lemma B_sum_is_sol (f : Fin 7 → ℚ) : (SM 3).IsSolution (∑ i, f i • B i) := by
  let X := chargeToAF (∑ i, f i • B i) (by
    rw [map_sum]
-    apply Fintype.sum_eq_zero
-    intro i
+    apply Fintype.sum_eq_zero _ fun i ↦ ?_
    rw [map_smul]
    have h : accGrav (B i) = 0 := by
      fin_cases i <;> rfl
@ -281,20 +274,16 @@ lemma B_sum_is_sol (f : Fin 7 → ℚ) : (SM 3).IsSolution (∑ i, f i • B i)
    exact DistribMulAction.smul_zero (f i))
    (by
      rw [map_sum]
-      apply Fintype.sum_eq_zero
-      intro i
+      apply Fintype.sum_eq_zero _ fun i ↦ ?_
      rw [map_smul]
-      have h : accSU2 (B i) = 0 := by
-        fin_cases i <;> rfl
+      have h : accSU2 (B i) = 0 := by fin_cases i <;> rfl
      rw [h]
      exact DistribMulAction.smul_zero (f i))
    (by
      rw [map_sum]
-      apply Fintype.sum_eq_zero
-      intro i
+      apply Fintype.sum_eq_zero _ fun i ↦ ?_
      rw [map_smul]
-      have h : accSU3 (B i) = 0 := by
-        fin_cases i <;> rfl
+      have h : accSU3 (B i) = 0 := by fin_cases i <;> rfl
      rw [h]
      exact DistribMulAction.smul_zero (f i))
    (B_in_accCube f)
@ -302,8 +291,7 @@ lemma B_sum_is_sol (f : Fin 7 → ℚ) : (SM 3).IsSolution (∑ i, f i • B i)
  rfl

 theorem basis_linear_independent : LinearIndependent ℚ B := by
-  apply Fintype.linearIndependent_iff.mpr
-  intro f h
+  refine Fintype.linearIndependent_iff.mpr fun f h ↦ ?_
  have h0 := congrFun h (0 : Fin 18)
  have h1 := congrFun h (3 : Fin 18)
  have h2 := congrFun h (6 : Fin 18)
--- a/HepLean/AnomalyCancellation/SMNu/Ordinary/FamilyMaps.lean
+++ b/HepLean/AnomalyCancellation/SMNu/Ordinary/FamilyMaps.lean
@ -29,12 +29,8 @@ def familyUniversalLinear (n : ℕ) :
    (by rw [familyUniversal_accGrav, gravSol S, mul_zero])
    (by rw [familyUniversal_accSU2, SU2Sol S, mul_zero])
    (by rw [familyUniversal_accSU3, SU3Sol S, mul_zero])
-  map_add' S T := by
-    apply ACCSystemLinear.LinSols.ext
-    exact (familyUniversal n).map_add' _ _
-  map_smul' a S := by
-    apply ACCSystemLinear.LinSols.ext
-    exact (familyUniversal n).map_smul' _ _
+  map_add' S T := ACCSystemLinear.LinSols.ext ((familyUniversal n).map_add' _ _)
+  map_smul' a S := ACCSystemLinear.LinSols.ext ((familyUniversal n).map_smul' _ _)

 /-- The family universal maps on `QuadSols`. -/
 def familyUniversalQuad (n : ℕ) :
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean
@ -66,8 +66,7 @@ lemma on_quadBiLin (S : (PlusU1 n).Charges) :
  ring

 lemma on_quadBiLin_AFL (S : (PlusU1 n).LinSols) : quadBiLin (BL n).val S.val = 0 := by
-  rw [on_quadBiLin]
-  rw [YYsol S, SU2Sol S, SU3Sol S]
+  rw [on_quadBiLin, YYsol S, SU2Sol S, SU3Sol S]
  simp

 lemma add_AFL_quad (S : (PlusU1 n).LinSols) (a b : ℚ) :
@ -87,7 +86,7 @@ def addQuad (S : (PlusU1 n).QuadSols) (a b : ℚ) : (PlusU1 n).QuadSols :=
  linearToQuad (a • S.1 + b • (BL n).1.1) (add_quad S a b)

 lemma addQuad_zero (S : (PlusU1 n).QuadSols) (a : ℚ) : addQuad S a 0 = a • S := by
-  simp [addQuad, linearToQuad]
+  simp only [addQuad, linearToQuad, zero_smul, add_zero]
  rfl

 lemma on_cubeTriLin (S : (PlusU1 n).Charges) :
@ -100,8 +99,7 @@ lemma on_cubeTriLin (S : (PlusU1 n).Charges) :

 lemma on_cubeTriLin_AFL (S : (PlusU1 n).LinSols) :
    cubeTriLin (BL n).val (BL n).val S.val = 0 := by
-  rw [on_cubeTriLin]
-  rw [gravSol S, SU3Sol S]
+  rw [on_cubeTriLin, gravSol S, SU3Sol S]
  simp

 lemma add_AFL_cube (S : (PlusU1 n).LinSols) (a b : ℚ) :
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/Basic.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/Basic.lean
@ -10,7 +10,6 @@ import HepLean.AnomalyCancellation.GroupActions
 # ACC system for SM with RHN

 We define the ACC system for the Standard Model with right-handed neutrinos.
-
 -/
 universe v u

--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean
@ -24,19 +24,15 @@ 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)
+  LinearIndependent ℚ B ∧ ∀ (f : Fin n → ℚ), (PlusU1 3).IsSolution (∑ i, f i • B i)

 lemma exists_plane_exists_basis {n : ℕ} (hE : ExistsPlane n) :
    ∃ (B : Fin 11 ⊕ Fin n → (PlusU1 3).Charges), LinearIndependent ℚ B := by
  obtain ⟨E, hE1, hE2⟩ := hE
  obtain ⟨B, hB1, hB2⟩ := eleven_dim_plane_of_no_sols_exists
  let Y := Sum.elim B E
-  use Y
-  apply Fintype.linearIndependent_iff.mpr
-  intro g hg
-  rw [@Fintype.sum_sum_type] at hg
-  rw [@add_eq_zero_iff_eq_neg] at hg
-  rw [← @Finset.sum_neg_distrib] at hg
+  refine ⟨Y, Fintype.linearIndependent_iff.mpr fun g hg ↦ ?_⟩
+  rw [@Fintype.sum_sum_type, @add_eq_zero_iff_eq_neg, ← @Finset.sum_neg_distrib] at hg
  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
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean
@ -65,8 +65,7 @@ lemma on_quadBiLin (S : (PlusU1 n).Charges) :
  simp

 lemma on_quadBiLin_AFL (S : (PlusU1 n).LinSols) : quadBiLin (Y n).val S.val = 0 := by
-  rw [on_quadBiLin]
-  rw [YYsol S]
+  rw [on_quadBiLin, YYsol S]

 lemma add_AFL_quad (S : (PlusU1 n).LinSols) (a b : ℚ) :
    accQuad (a • S.val + b • (Y n).val) = a ^ 2 * accQuad S.val := by
@ -77,16 +76,14 @@ lemma add_AFL_quad (S : (PlusU1 n).LinSols) (a b : ℚ) :

 lemma add_quad (S : (PlusU1 n).QuadSols) (a b : ℚ) :
    accQuad (a • S.val + b • (Y n).val) = 0 := by
-  rw [add_AFL_quad, quadSol S]
-  simp
+  rw [add_AFL_quad, quadSol S]; simp

 /-- The `QuadSol` obtained by adding hypercharge to a `QuadSol`. -/
 def addQuad (S : (PlusU1 n).QuadSols) (a b : ℚ) : (PlusU1 n).QuadSols :=
  linearToQuad (a • S.1 + b • (Y n).1.1) (add_quad S a b)

 lemma addQuad_zero (S : (PlusU1 n).QuadSols) (a : ℚ) : addQuad S a 0 = a • S := by
-  simp [addQuad, linearToQuad]
-  rfl
+  simp only [addQuad, linearToQuad, zero_smul, add_zero]; rfl

 lemma on_cubeTriLin (S : (PlusU1 n).Charges) :
    cubeTriLin (Y n).val (Y n).val S = 6 * accYY S := by
@ -98,9 +95,7 @@ lemma on_cubeTriLin (S : (PlusU1 n).Charges) :

 lemma on_cubeTriLin_AFL (S : (PlusU1 n).LinSols) :
    cubeTriLin (Y n).val (Y n).val S.val = 0 := by
-  rw [on_cubeTriLin]
-  rw [YYsol S]
-  simp
+  rw [on_cubeTriLin, YYsol S]; simp

 lemma on_cubeTriLin' (S : (PlusU1 n).Charges) :
    cubeTriLin (Y n).val S S = 6 * accQuad S := by
@ -112,9 +107,7 @@ lemma on_cubeTriLin' (S : (PlusU1 n).Charges) :

 lemma on_cubeTriLin'_ALQ (S : (PlusU1 n).QuadSols) :
    cubeTriLin (Y n).val S.val S.val = 0 := by
-  rw [on_cubeTriLin']
-  rw [quadSol S]
-  simp
+  rw [on_cubeTriLin', quadSol S]; simp

 lemma add_AFL_cube (S : (PlusU1 n).LinSols) (a b : ℚ) :
    accCube (a • S.val + b • (Y n).val) =
@ -128,15 +121,12 @@ lemma add_AFL_cube (S : (PlusU1 n).LinSols) (a b : ℚ) :

 lemma add_AFQ_cube (S : (PlusU1 n).QuadSols) (a b : ℚ) :
    accCube (a • S.val + b • (Y n).val) = a ^ 3 * accCube S.val := by
-  rw [add_AFL_cube]
-  rw [cubeTriLin.swap₃]
-  rw [on_cubeTriLin'_ALQ]
+  rw [add_AFL_cube, cubeTriLin.swap₃, on_cubeTriLin'_ALQ]
  ring

 lemma add_AF_cube (S : (PlusU1 n).Sols) (a b : ℚ) :
    accCube (a • S.val + b • (Y n).val) = 0 := by
-  rw [add_AFQ_cube]
-  rw [cubeSol S]
+  rw [add_AFQ_cube, cubeSol S]
  simp

 /-- The `Sol` obtained by adding hypercharge to a `Sol`. -/
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/PlaneNonSols.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/PlaneNonSols.lean
@ -80,8 +80,7 @@ lemma Bi_Bj_quad {i j : Fin 11} (hi : i ≠ j) : quadBiLin (B i) (B j) = 0 := by

 lemma Bi_sum_quad (i : Fin 11) (f : Fin 11 → ℚ) :
    quadBiLin (B i) (∑ k, f k • B k) = f i * quadBiLin (B i) (B i) := by
-  rw [quadBiLin.map_sum₂]
-  rw [Fintype.sum_eq_single i]
+  rw [quadBiLin.map_sum₂, Fintype.sum_eq_single i]
  · rw [quadBiLin.map_smul₂]
  · intro k hij
    rw [quadBiLin.map_smul₂, Bi_Bj_quad hij.symm]
@ -99,8 +98,7 @@ lemma on_accQuad (f : Fin 11 → ℚ) :
    accQuad (∑ i, f i • B i) = ∑ i, quadCoeff i * (f i)^2 := by
  change quadBiLin _ _ = _
  rw [quadBiLin.map_sum₁]
-  apply Fintype.sum_congr
-  intro i
+  refine Fintype.sum_congr _ _ fun i ↦ ?_
  rw [quadBiLin.map_smul₁, Bi_sum_quad, quadCoeff_eq_bilinear]
  ring

@ -108,14 +106,12 @@ lemma isSolution_quadCoeff_f_sq_zero (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSol
    (k : Fin 11) : quadCoeff k * (f k)^2 = 0 := by
  obtain ⟨S, hS⟩ := hS
  have hQ := quadSol S.1
-  rw [hS, on_accQuad] at hQ
-  rw [Fintype.sum_eq_zero_iff_of_nonneg] at hQ
+  rw [hS, on_accQuad, Fintype.sum_eq_zero_iff_of_nonneg] at hQ
  · exact congrFun hQ k
  · intro i
    simp only [Pi.zero_apply, quadCoeff]
    rw [mul_nonneg_iff]
-    apply Or.inl
-    apply And.intro
+    apply Or.inl (And.intro _ _)
    fin_cases i <;> rfl
    exact sq_nonneg (f i)

@ -174,39 +170,31 @@ lemma isSolution_grav (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f
  have hx := isSolution_sum_part f hS
  obtain ⟨S, hS'⟩ := hS
  have hg := gravSol S.toLinSols
-  rw [hS'] at hg
-  rw [hx] at hg
-  rw [accGrav.map_add, accGrav.map_smul, accGrav.map_smul] at hg
-  rw [show accGrav B₉ = 3 by rfl] at hg
-  rw [show accGrav B₁₀ = 1 by rfl] at hg
+  rw [hS', hx, accGrav.map_add, accGrav.map_smul, accGrav.map_smul, show accGrav B₉ = 3 by rfl,
+    show accGrav B₁₀ = 1 by rfl] at hg
  simp at hg
  linear_combination hg

 lemma isSolution_sum_part' (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f i • B i)) :
    ∑ i, f i • B i = f 9 • B₉ + (- 3 * f 9) • B₁₀ := by
-  rw [isSolution_sum_part f hS]
-  rw [isSolution_grav f hS]
+  rw [isSolution_sum_part f hS, isSolution_grav f hS]

 lemma isSolution_f9 (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f i • B i)) :
    f 9 = 0 := by
  have hx := isSolution_sum_part' f hS
  obtain ⟨S, hS'⟩ := hS
  have hc := cubeSol S
-  rw [hS'] at hc
-  rw [hx] at hc
+  rw [hS', hx] at hc
  change cubeTriLin.toCubic _ = _ at hc
  rw [cubeTriLin.toCubic_add] at hc
  erw [accCube.map_smul] at hc
  erw [accCube.map_smul (- 3 * f 9) B₁₀] at hc
  rw [cubeTriLin.map_smul₁, cubeTriLin.map_smul₁, cubeTriLin.map_smul₂, cubeTriLin.map_smul₂,
    cubeTriLin.map_smul₃, cubeTriLin.map_smul₃] at hc
-  rw [show accCube B₉ = 9 by rfl] at hc
-  rw [show accCube B₁₀ = 1 by rfl] at hc
-  rw [show cubeTriLin B₉ B₉ B₁₀ = 0 by rfl] at hc
-  rw [show cubeTriLin B₁₀ B₁₀ B₉ = 0 by rfl] at hc
+  rw [show accCube B₉ = 9 by rfl, show accCube B₁₀ = 1 by rfl, show cubeTriLin B₉ B₉ B₁₀ = 0 by rfl,
+    show cubeTriLin B₁₀ B₁₀ B₉ = 0 by rfl] at hc
  simp at hc
-  have h1 : f 9 ^ 3 * 9 + (-(3 * f 9)) ^ 3 = - 18 * f 9 ^ 3 := by
-    ring
+  have h1 : f 9 ^ 3 * 9 + (-(3 * f 9)) ^ 3 = - 18 * f 9 ^ 3 := by ring
  rw [h1] at hc
  simpa using hc

@ -232,30 +220,19 @@ lemma isSolution_f_zero (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i,

 lemma isSolution_only_if_zero (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f i • B i)) :
    ∑ i, f i • B i = 0 := by
-  rw [isSolution_sum_part f hS]
-  rw [isSolution_grav f hS]
-  rw [isSolution_f9 f hS]
+  rw [isSolution_sum_part f hS, isSolution_grav f hS, isSolution_f9 f hS]
  simp

-theorem basis_linear_independent : LinearIndependent ℚ B := by
-  apply Fintype.linearIndependent_iff.mpr
-  intro f h
-  let X : (PlusU1 3).Sols := chargeToAF 0 (by rfl) (by rfl) (by rfl) (by rfl) (by rfl) (by rfl)
-  have hS : (PlusU1 3).IsSolution (∑ i, f i • B i) := by
-    use X
-    rw [h]
-    rfl
-  exact isSolution_f_zero f hS
+theorem basis_linear_independent : LinearIndependent ℚ B :=
+  Fintype.linearIndependent_iff.mpr fun f h ↦ isSolution_f_zero f
+    ⟨chargeToAF 0 (by rfl) (by rfl) (by rfl) (by rfl) (by rfl) (by rfl), id (Eq.symm h)⟩

 end ElevenPlane

 theorem eleven_dim_plane_of_no_sols_exists : ∃ (B : Fin 11 → (PlusU1 3).Charges),
    LinearIndependent ℚ B ∧
-    ∀ (f : Fin 11 → ℚ), (PlusU1 3).IsSolution (∑ i, f i • B i) → ∑ i, f i • B i = 0 := by
-  use ElevenPlane.B
-  apply And.intro
-  · exact ElevenPlane.basis_linear_independent
-  · exact ElevenPlane.isSolution_only_if_zero
+    ∀ (f : Fin 11 → ℚ), (PlusU1 3).IsSolution (∑ i, f i • B i) → ∑ i, f i • B i = 0 :=
+  ⟨ElevenPlane.B, ElevenPlane.basis_linear_independent, ElevenPlane.isSolution_only_if_zero⟩

 end PlusU1
 end SMRHN