Merge pull request #134 from HEPLean/pitmonticone/golfing

refactor: golf a few proofs

HepLean/AnomalyCancellation/GroupActions.lean

@@ -45,12 +45,8 @@ def linSolMap {χ : ACCSystem} (G : ACCSystemGroupAction χ) (g : G.group) :
   toFun S := ⟨G.rep g S.val, by
     intro i
     rw [G.linearInvariant, S.linearSol]⟩
-  map_add' S T := by
-    apply ACCSystemLinear.LinSols.ext
-    exact (G.rep g).map_add' _ _
-  map_smul' a S := by
-    apply ACCSystemLinear.LinSols.ext
-    exact (G.rep g).map_smul' _ _
+  map_add' S T := ACCSystemLinear.LinSols.ext ((G.rep g).map_add' _ _)
+  map_smul' a S := ACCSystemLinear.LinSols.ext ((G.rep g).map_smul' _ _)
 
 /-- The representation acting on the vector space of solutions to the linear ACCs. -/
 @[simps!]
@@ -58,16 +54,12 @@ def linSolRep {χ : ACCSystem} (G : ACCSystemGroupAction χ) :
     Representation ℚ G.group χ.LinSols where
   toFun := G.linSolMap
   map_mul' g1 g2 := by
-    apply LinearMap.ext
-    intro S
-    apply ACCSystemLinear.LinSols.ext
+    refine LinearMap.ext fun S ↦ ACCSystemLinear.LinSols.ext ?_
     change (G.rep (g1 * g2)) S.val = _
     rw [G.rep.map_mul]
     rfl
   map_one' := by
-    apply LinearMap.ext
-    intro S
-    apply ACCSystemLinear.LinSols.ext
+    refine LinearMap.ext fun S ↦ ACCSystemLinear.LinSols.ext ?_
     change (G.rep.toFun 1) S.val = _
     rw [G.rep.map_one']
     rfl

HepLean/AnomalyCancellation/SMNu/Basic.lean

@@ -40,8 +40,8 @@ def toSpeciesEquiv : (SMνCharges n).Charges ≃ (Fin 6 → Fin n → ℚ) :=
 @[simps!]
 def toSpecies (i : Fin 6) : (SMνCharges n).Charges →ₗ[ℚ] (SMνSpecies n).Charges where
   toFun S := toSpeciesEquiv S i
-  map_add' _ _ := by aesop
-  map_smul' _ _ := by aesop
+  map_add' _ _ := rfl
+  map_smul' _ _ := rfl
 
 lemma charges_eq_toSpecies_eq (S T : (SMνCharges n).Charges) :
     S = T ↔ ∀ i, toSpecies i S = toSpecies i T := by
@@ -194,7 +194,8 @@ def accYY : (SMνCharges n).Charges →ₗ[ℚ] ℚ where
   map_add' S T := by
     simp only
     repeat rw [map_add]
-    simp [Pi.add_apply, mul_add]
+    simp only [SMνSpecies_numberCharges, ACCSystemCharges.chargesAddCommMonoid_add, toSpecies_apply,
+      Fin.isValue, mul_add]
     repeat erw [Finset.sum_add_distrib]
     ring
   map_smul' a S := by
@@ -232,8 +233,7 @@ def quadBiLin : BiLinearSymm (SMνCharges n).Charges := BiLinearSymm.mk₂
     intro a S T
     simp only
     rw [Finset.mul_sum]
-    apply Fintype.sum_congr
-    intro i
+    refine Fintype.sum_congr _ _ fun i ↦ ?_
     repeat erw [map_smul]
     simp [HSMul.hSMul, SMul.smul]
     ring)
@@ -241,8 +241,7 @@ def quadBiLin : BiLinearSymm (SMνCharges n).Charges := BiLinearSymm.mk₂
     intro S T R
     simp only
     rw [← Finset.sum_add_distrib]
-    apply Fintype.sum_congr
-    intro i
+    refine Fintype.sum_congr _ _ fun i ↦ ?_
     repeat erw [map_add]
     simp only [ACCSystemCharges.chargesAddCommMonoid_add, toSpecies_apply, Fin.isValue, neg_mul,
       one_mul]
@@ -250,8 +249,7 @@ def quadBiLin : BiLinearSymm (SMνCharges n).Charges := BiLinearSymm.mk₂
   (by
     intro S T
     simp only [SMνSpecies_numberCharges, toSpecies_apply, Fin.isValue, neg_mul, one_mul]
-    apply Fintype.sum_congr
-    intro i
+    refine Fintype.sum_congr _ _ fun i ↦ ?_
     ring)
 
 lemma quadBiLin_decomp (S T : (SMνCharges n).Charges) :
@@ -298,8 +296,7 @@ def cubeTriLin : TriLinearSymm (SMνCharges n).Charges := TriLinearSymm.mk₃
     intro a S T R
     simp only
     rw [Finset.mul_sum]
-    apply Fintype.sum_congr
-    intro i
+    refine Fintype.sum_congr _ _ fun i ↦ ?_
     repeat erw [map_smul]
     simp [HSMul.hSMul, SMul.smul]
     ring)
@@ -307,22 +304,19 @@ def cubeTriLin : TriLinearSymm (SMνCharges n).Charges := TriLinearSymm.mk₃
     intro S T R L
     simp only
     rw [← Finset.sum_add_distrib]
-    apply Fintype.sum_congr
-    intro i
+    refine Fintype.sum_congr _ _ fun i ↦ ?_
     repeat erw [map_add]
     simp only [ACCSystemCharges.chargesAddCommMonoid_add, toSpecies_apply, Fin.isValue]
     ring)
   (by
     intro S T L
     simp only [SMνSpecies_numberCharges, toSpecies_apply, Fin.isValue]
-    apply Fintype.sum_congr
-    intro i
+    refine Fintype.sum_congr _ _ fun i ↦ ?_
     ring)
   (by
     intro S T L
     simp only [SMνSpecies_numberCharges, toSpecies_apply, Fin.isValue]
-    apply Fintype.sum_congr
-    intro i
+    refine Fintype.sum_congr _ _ fun i ↦ ?_
     ring)
 
 lemma cubeTriLin_decomp (S T R : (SMνCharges n).Charges) :

HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean

@@ -8,7 +8,6 @@ import HepLean.AnomalyCancellation.SMNu.Basic
 # Family maps for the Standard Model for RHN ACCs
 
 We define the a series of maps between the charges for different numbers of families.
-
 -/
 
 universe v u
@@ -25,15 +24,12 @@ def chargesMapOfSpeciesMap {n m : ℕ} (f : (SMνSpecies n).Charges →ₗ[ℚ]
   map_add' S T := by
     rw [charges_eq_toSpecies_eq]
     intro i
-    rw [map_add]
-    rw [toSMSpecies_toSpecies_inv, toSMSpecies_toSpecies_inv, toSMSpecies_toSpecies_inv]
-    rw [map_add]
+    rw [map_add, toSMSpecies_toSpecies_inv, toSMSpecies_toSpecies_inv, toSMSpecies_toSpecies_inv,
+      map_add]
   map_smul' a S := by
     rw [charges_eq_toSpecies_eq]
     intro i
-    rw [map_smul]
-    rw [toSMSpecies_toSpecies_inv, toSMSpecies_toSpecies_inv]
-    rw [map_smul]
+    rw [map_smul, toSMSpecies_toSpecies_inv, toSMSpecies_toSpecies_inv, map_smul]
     rfl
 
 lemma chargesMapOfSpeciesMap_toSpecies {n m : ℕ}
@@ -89,9 +85,9 @@ a universal manor. -/
 @[simps!]
 def speciesFamilyUniversial (n : ℕ) :
     (SMνSpecies 1).Charges →ₗ[ℚ] (SMνSpecies n).Charges where
-  toFun S _ := S ⟨0, by simp⟩
-  map_add' S T := rfl
-  map_smul' a S := rfl
+  toFun S _ := S ⟨0, Nat.zero_lt_succ 0⟩
+  map_add' _ _ := rfl
+  map_smul' _ _ := rfl
 
 /-- The embedding of the `1`-family charges into the `n`-family charges in
 a universal manor. -/

HepLean/AnomalyCancellation/SMNu/NoGrav/Basic.lean

@@ -11,8 +11,8 @@ import HepLean.AnomalyCancellation.GroupActions
 
 We define the ACC system for the Standard Model with right-handed neutrinos and no gravitational
 anomaly.
-
 -/
+
 universe v u
 
 namespace SMRHN
@@ -29,9 +29,7 @@ def SMNoGrav (n : ℕ) : ACCSystem where
     | 0 => @accSU2 n
     | 1 => accSU3
   numberQuadratic := 0
-  quadraticACCs := by
-    intro i
-    exact Fin.elim0 i
+  quadraticACCs := fun i ↦ Fin.elim0 i
   cubicACC := accCube
 
 namespace SMNoGrav
@@ -48,8 +46,7 @@ lemma SU3Sol (S : (SMNoGrav n).LinSols) : accSU3 S.val = 0 := by
   simp at hS
   exact hS 1
 
-lemma cubeSol (S : (SMNoGrav n).Sols) : accCube S.val = 0 := by
-  exact S.cubicSol
+lemma cubeSol (S : (SMNoGrav n).Sols) : accCube S.val = 0 := S.cubicSol
 
 /-- An element of `charges` which satisfies the linear ACCs
   gives us a element of `LinSols`. -/
@@ -64,10 +61,7 @@ def chargeToLinear (S : (SMNoGrav n).Charges) (hSU2 : accSU2 S = 0) (hSU3 : accS
 
 /-- An element of `LinSols` which satisfies the quadratic ACCs
   gives us a element of `QuadSols`. -/
-def linearToQuad (S : (SMNoGrav n).LinSols) : (SMNoGrav n).QuadSols :=
-  ⟨S, by
-    intro i
-    exact Fin.elim0 i⟩
+def linearToQuad (S : (SMNoGrav n).LinSols) : (SMNoGrav n).QuadSols := ⟨S, fun i ↦ Fin.elim0 i⟩
 
 /-- An element of `QuadSols` which satisfies the quadratic ACCs
   gives us a element of `LinSols`. -/
@@ -100,13 +94,13 @@ def perm (n : ℕ) : ACCSystemGroupAction (SMNoGrav n) where
   rep := repCharges
   linearInvariant := by
     intro i
-    simp at i
+    simp only [SMNoGrav_numberLinear] at i
     match i with
     | 0 => exact accSU2_invariant
     | 1 => exact accSU3_invariant
   quadInvariant := by
     intro i
-    simp at i
+    simp only [SMNoGrav_numberQuadratic] at i
     exact Fin.elim0 i
   cubicInvariant := accCube_invariant
 

HepLean/AnomalyCancellation/SMNu/Ordinary/Basic.lean

@@ -14,7 +14,6 @@ We define the ACC system for the Standard Model (without hypercharge) with right
 -/
 
 universe v u
-
 namespace SMRHN
 open SMνCharges
 open SMνACCs
@@ -54,8 +53,7 @@ lemma SU3Sol (S : (SM n).LinSols) : accSU3 S.val = 0 := by
   simp at hS
   exact hS 2
 
-lemma cubeSol (S : (SM n).Sols) : accCube S.val = 0 := by
-  exact S.cubicSol
+lemma cubeSol (S : (SM n).Sols) : accCube S.val = 0 := S.cubicSol
 
 /-- An element of `charges` which satisfies the linear ACCs
   gives us a element of `LinSols`. -/
@@ -72,9 +70,7 @@ def chargeToLinear (S : (SM n).Charges) (hGrav : accGrav S = 0)
 /-- An element of `LinSols` which satisfies the quadratic ACCs
   gives us a element of `QuadSols`. -/
 def linearToQuad (S : (SM n).LinSols) : (SM n).QuadSols :=
-  ⟨S, by
-    intro i
-    exact Fin.elim0 i⟩
+  ⟨S, fun i ↦ Fin.elim0 i⟩
 
 /-- An element of `QuadSols` which satisfies the quadratic ACCs
   gives us a element of `Sols`. -/

HepLean/AnomalyCancellation/SMNu/Ordinary/DimSevenPlane.lean

@@ -12,7 +12,6 @@ We give an example of a 7 dimensional plane on which every point satisfies the A
 
 The main result of this file is `seven_dim_plane_exists` which states that there exists a
 7 dimensional plane of charges on which every point satisfies the ACCs.
-
 -/
 
 namespace SMRHN

HepLean/AnomalyCancellation/SMNu/Permutations.lean

@@ -10,7 +10,6 @@ import Mathlib.RepresentationTheory.Basic
 # Permutations of SM charges with RHN.
 
 We define the group of permutations for the SM charges with RHN.
-
 -/
 
 universe v u
@@ -54,8 +53,7 @@ def repCharges {n : ℕ} : Representation ℚ (PermGroup n) (SMνCharges n).Char
     repeat erw [toSMSpecies_toSpecies_inv]
     rfl
   map_one' := by
-    apply LinearMap.ext
-    intro S
+    refine LinearMap.ext fun S => ?_
     rw [charges_eq_toSpecies_eq]
     intro i
     erw [toSMSpecies_toSpecies_inv]
@@ -75,32 +73,26 @@ lemma toSpecies_sum_invariant (m : ℕ) (f : PermGroup n) (S : (SMνCharges n).C
 
 lemma accGrav_invariant (f : PermGroup n) (S : (SMνCharges n).Charges) :
     accGrav (repCharges f S) = accGrav S :=
-  accGrav_ext
-    (by simpa using toSpecies_sum_invariant 1 f S)
+  accGrav_ext (by simpa using toSpecies_sum_invariant 1 f S)
 
 lemma accSU2_invariant (f : PermGroup n) (S : (SMνCharges n).Charges) :
     accSU2 (repCharges f S) = accSU2 S :=
-  accSU2_ext
-    (by simpa using toSpecies_sum_invariant 1 f S)
+  accSU2_ext (by simpa using toSpecies_sum_invariant 1 f S)
 
 lemma accSU3_invariant (f : PermGroup n) (S : (SMνCharges n).Charges) :
     accSU3 (repCharges f S) = accSU3 S :=
-  accSU3_ext
-    (by simpa using toSpecies_sum_invariant 1 f S)
+  accSU3_ext (by simpa using toSpecies_sum_invariant 1 f S)
 
 lemma accYY_invariant (f : PermGroup n) (S : (SMνCharges n).Charges) :
     accYY (repCharges f S) = accYY S :=
-  accYY_ext
-    (by simpa using toSpecies_sum_invariant 1 f S)
+  accYY_ext (by simpa using toSpecies_sum_invariant 1 f S)
 
 lemma accQuad_invariant (f : PermGroup n) (S : (SMνCharges n).Charges) :
     accQuad (repCharges f S) = accQuad S :=
-  accQuad_ext
-    (toSpecies_sum_invariant 2 f S)
+  accQuad_ext (toSpecies_sum_invariant 2 f S)
 
 lemma accCube_invariant (f : PermGroup n) (S : (SMνCharges n).Charges) :
     accCube (repCharges f S) = accCube S :=
-  accCube_ext
-    (by simpa using toSpecies_sum_invariant 3 f S)
+  accCube_ext (by simpa using toSpecies_sum_invariant 3 f S)
 
 end SMRHN