Merge pull request #55 from HEPLean/LorentzAlgebra

refactor: General golfing

HepLean/AnomalyCancellation/LinearMaps.lean

@@ -74,23 +74,15 @@ def mk₂ (f : V × V → ℚ) (map_smul : ∀ a S T, f (a • S, T) = a * f (S,
       intro T1 T2
       simp only
       rw [swap, map_add]
-      rw [swap T1 S, swap T2 S]
+      exact Mathlib.Tactic.LinearCombination.add_pf (swap T1 S) (swap T2 S)
     map_smul' :=by
       intro a T
       simp only [eq_ratCast, Rat.cast_eq_id, id_eq, smul_eq_mul]
       rw [swap, map_smul]
-      rw [swap T S]
+      exact congrArg (HMul.hMul a) (swap T S)
   }
-  map_smul' := by
+  map_smul' := fun a S  => LinearMap.ext fun T => map_smul a S T
-    intro a S
+  map_add' := fun S1 S2  => LinearMap.ext fun T => map_add S1 S2 T
-    apply LinearMap.ext
-    intro T
-    exact map_smul a S T
-  map_add' := by
-    intro S1 S2
-    apply LinearMap.ext
-    intro T
-    exact map_add S1 S2 T
   swap' := swap
 
 lemma map_smul₁ (f : BiLinearSymm V) (a : ℚ) (S T : V) : f (a • S) T = a * f S T := by
@@ -114,8 +106,7 @@ lemma map_add₂ (f : BiLinearSymm V) (S : V) (T1 T2 : V) :
 /-- 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
+  map_add' S1 S2 := map_add₁ f S1 S2 T
-    simp only [f.map_add₁]
   map_smul' a S := by
     simp only [f.map_smul₁]
     rfl

HepLean/AnomalyCancellation/MSSMNu/Basic.lean

@@ -45,10 +45,8 @@ def toSMPlusH : MSSMCharges.charges ≃ (Fin 18 ⊕ Fin 2 → ℚ) :=
 def splitSMPlusH : (Fin 18 ⊕ Fin 2 → ℚ) ≃ (Fin 18 → ℚ) × (Fin 2 → ℚ) where
   toFun f := (f ∘ Sum.inl , f ∘ Sum.inr)
   invFun f :=  Sum.elim f.1 f.2
-  left_inv f := by
+  left_inv f := Sum.elim_comp_inl_inr f
-    aesop
+  right_inv _ := rfl
-  right_inv f := by
-    aesop
 
 /-- An equivalence between `MSSMCharges.charges` and `(Fin 18 → ℚ) × (Fin 2 → ℚ)`. This
 splits the charges up into the SM and the additional ones for the MSSM. -/
@@ -74,8 +72,8 @@ corresponding SM species of charges. -/
 @[simps!]
 def toSMSpecies (i : Fin 6) : MSSMCharges.charges →ₗ[ℚ] MSSMSpecies.charges where
   toFun S := (Prod.fst ∘ toSpecies) S i
-  map_add' _ _ := by aesop
+  map_add' _ _ := by rfl
-  map_smul' _ _ := by aesop
+  map_smul' _ _ := by rfl
 
 lemma toSMSpecies_toSpecies_inv (i : Fin 6) (f :  (Fin 6 → Fin 3 → ℚ) × (Fin 2 → ℚ)) :
     (toSMSpecies i) (toSpecies.symm f) = f.1 i := by
@@ -98,16 +96,16 @@ abbrev N := toSMSpecies 5
 /-- The charge `Hd`. -/
 @[simps!]
 def Hd : MSSMCharges.charges →ₗ[ℚ] ℚ where
-  toFun S := S ⟨18, by simp⟩
+  toFun S := S ⟨18, Nat.lt_of_sub_eq_succ rfl⟩
-  map_add' _ _ := by aesop
+  map_add' _ _ := by rfl
-  map_smul' _ _ := by aesop
+  map_smul' _ _ := by rfl
 
 /-- The charge `Hu`. -/
 @[simps!]
 def Hu : MSSMCharges.charges →ₗ[ℚ] ℚ where
-  toFun S := S ⟨19, by simp⟩
+  toFun S := S ⟨19, Nat.lt_of_sub_eq_succ rfl⟩
-  map_add' _ _ := by aesop
+  map_add' _ _ := by rfl
-  map_smul' _ _ := by aesop
+  map_smul' _ _ := by rfl
 
 lemma charges_eq_toSpecies_eq (S T : MSSMCharges.charges) :
     S = T ↔ (∀ i, toSMSpecies i S = toSMSpecies i T) ∧ Hd S = Hd T ∧ Hu S = Hu T  := by
@@ -333,10 +331,7 @@ lemma accQuad_ext {S T : (MSSMCharges).charges}
   repeat erw [Finset.sum_add_distrib]
   repeat erw [← Finset.mul_sum]
   ring_nf
-  have h1 : ∀ j, ∑ i, (toSMSpecies j S i)^2 = ∑ i, (toSMSpecies j T i)^2 := by
+  have h1 : ∀ j, ∑ i, (toSMSpecies j S i)^2 = ∑ i, (toSMSpecies j T i)^2 := fun j => h j
-    intro j
-    erw [h]
-    rfl
   repeat rw [h1]
   rw [hd, hu]
 

HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean

@@ -80,13 +80,7 @@ lemma planeY₃B₃_val_eq' (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ) (hR' : R
     rw [← Module.add_smul]
     simp
   rw [← Module.add_smul] at h1i
-  have hR : ∃ i, R.val i ≠ 0 := by
+  have hR : ∃ i, R.val i ≠ 0 := Function.ne_iff.mp hR'
-    by_contra h
-    simp at h
-    have h0 : R.val = 0 := by
-      funext i
-      apply h i
-    exact hR' h0
   obtain ⟨i, hi⟩ := hR
   have h2 := congrArg (fun S => S i) h1i
   change _ = 0 at h2
@@ -242,12 +236,12 @@ lemma α₁_proj (T : MSSMACC.Sols) : α₁ (proj T.1.1) =
 lemma α₁_proj_zero (T : MSSMACC.Sols) (h1 : α₃ (proj T.1.1) = 0) :
     α₁ (proj T.1.1) = 0 := by
   rw [α₁_proj, h1]
-  simp
+  exact mul_eq_zero_of_left rfl ((dot B₃.val) T.val - (dot Y₃.val) T.val)
 
 lemma α₂_proj_zero (T : MSSMACC.Sols) (h1 : α₃ (proj T.1.1) = 0) :
     α₂ (proj T.1.1) = 0 := by
   rw [α₂_proj, h1]
-  simp
+  exact mul_eq_zero_of_left rfl ((dot Y₃.val) T.val - 2 * (dot B₃.val) T.val)
 
 end proj
 

HepLean/AnomalyCancellation/MSSMNu/Permutations.lean

@@ -39,28 +39,18 @@ def chargeMap (f : permGroup) : MSSMCharges.charges →ₗ[ℚ] MSSMCharges.char
   map_add' S T := by
     simp only
     rw [charges_eq_toSpecies_eq]
-    apply And.intro
+    refine And.intro ?_ $ Prod.mk.inj_iff.mp rfl
     intro i
     rw [(toSMSpecies i).map_add]
     rw [toSMSpecies_toSpecies_inv, toSMSpecies_toSpecies_inv, toSMSpecies_toSpecies_inv]
-    simp only
-    erw [(toSMSpecies i).map_add]
-    rfl
-    apply And.intro
-    rw [Hd.map_add, Hd_toSpecies_inv, Hd_toSpecies_inv, Hd_toSpecies_inv]
-    rfl
-    rw [Hu.map_add, Hu_toSpecies_inv, Hu_toSpecies_inv, Hu_toSpecies_inv]
     rfl
   map_smul' a S := by
     simp only
     rw [charges_eq_toSpecies_eq]
-    apply And.intro
+    apply And.intro ?_ $ Prod.mk.inj_iff.mp rfl
     intro i
     rw [(toSMSpecies i).map_smul, toSMSpecies_toSpecies_inv, toSMSpecies_toSpecies_inv]
     rfl
-    apply And.intro
-    rfl
-    rfl
 
 lemma chargeMap_toSpecies (f : permGroup) (S : MSSMCharges.charges) (j : Fin 6) :
     toSMSpecies j (chargeMap f S) = toSMSpecies j S ∘ f j := by
@@ -75,27 +65,21 @@ def repCharges : Representation ℚ (permGroup) (MSSMCharges).charges where
     apply LinearMap.ext
     intro S
     rw [charges_eq_toSpecies_eq]
-    apply And.intro
+    refine And.intro ?_ $  Prod.mk.inj_iff.mp rfl
     intro i
     simp only [ Pi.mul_apply, Pi.inv_apply, Equiv.Perm.coe_mul, LinearMap.mul_apply]
     rw [chargeMap_toSpecies, chargeMap_toSpecies]
     simp only [Pi.mul_apply, Pi.inv_apply]
     rw [chargeMap_toSpecies]
     rfl
-    apply And.intro
-    rfl
-    rfl
   map_one' := by
     apply LinearMap.ext
     intro S
     rw [charges_eq_toSpecies_eq]
-    apply And.intro
+    refine And.intro ?_ $  Prod.mk.inj_iff.mp rfl
     intro i
     erw [toSMSpecies_toSpecies_inv]
     rfl
-    apply And.intro
-    rfl
-    rfl
 
 lemma repCharges_toSMSpecies (f : permGroup) (S : MSSMCharges.charges) (j : Fin 6) :
     toSMSpecies j (repCharges f S) = toSMSpecies j S ∘ f⁻¹ j := by
@@ -104,10 +88,8 @@ lemma repCharges_toSMSpecies (f : permGroup) (S : MSSMCharges.charges) (j : Fin
 lemma toSpecies_sum_invariant (m : ℕ) (f : permGroup) (S : MSSMCharges.charges) (j : Fin 6) :
     ∑ i, ((fun a => a ^ m) ∘ toSMSpecies j (repCharges f S)) i =
     ∑ i, ((fun a => a ^ m) ∘ toSMSpecies j S) i := by
-  erw [repCharges_toSMSpecies]
+  rw [repCharges_toSMSpecies]
-  change  ∑ i : Fin 3, ((fun a => a ^ m) ∘ _) (⇑(f⁻¹ _) i) = ∑ i : Fin 3, ((fun a => a ^ m) ∘ _) i
+  exact Equiv.sum_comp (f⁻¹ j) ((fun a => a ^ m) ∘ (toSMSpecies j) S)
-  refine Equiv.Perm.sum_comp _ _ _ ?_
-  simp only [permGroup, Fin.isValue, Pi.inv_apply, ne_eq, coe_univ, Set.subset_univ]
 
 lemma Hd_invariant (f : permGroup) (S : MSSMCharges.charges)  :
     Hd (repCharges f S) = Hd S := rfl
@@ -151,7 +133,7 @@ lemma accQuad_invariant (f : permGroup) (S : MSSMCharges.charges)  :
 lemma accCube_invariant (f : permGroup) (S : MSSMCharges.charges)  :
     accCube (repCharges f S) = accCube S :=
   accCube_ext
-    (by simpa using toSpecies_sum_invariant 3 f S)
+    (fun j => toSpecies_sum_invariant 3 f S j)
     (Hd_invariant f S)
     (Hu_invariant f S)
 

HepLean/AnomalyCancellation/PureU1/BasisLinear.lean

@@ -42,10 +42,7 @@ lemma asCharges_ne_castSucc {k j : Fin n} (h : k ≠ j) :
   simp [asCharges]
   split
   rename_i h1
-  rw [Fin.ext_iff] at h1
+  exact False.elim (h (id (Eq.symm h1)))
-  simp_all
-  rw [Fin.ext_iff] at h
-  simp_all
   split
   rename_i h1 h2
   rw [Fin.ext_iff] at h1 h2
@@ -68,11 +65,7 @@ def asLinSols (j : Fin n) : (PureU1 n.succ).LinSols :=
     rw [Fin.sum_univ_castSucc]
     rw [Finset.sum_eq_single j]
     simp only [asCharges, PureU1_numberCharges, ↓reduceIte]
-    have hn : ¬ (Fin.last n = Fin.castSucc j) := by
+    have hn : ¬ (Fin.last n = Fin.castSucc j) := Fin.ne_of_gt j.prop
-      have hj := j.prop
-      rw [Fin.ext_iff]
-      simp only [Fin.val_last, Fin.coe_castSucc, ne_eq]
-      omega
     split
     rename_i ht
     exact (hn ht).elim
@@ -84,30 +77,15 @@ def asLinSols (j : Fin n) : (PureU1 n.succ).LinSols :=
 
 
 lemma sum_of_vectors {n : ℕ} (f : Fin k → (PureU1 n).LinSols) (j : Fin n) :
-    (∑ i : Fin k, (f i)).1 j = (∑ i : Fin k, (f i).1 j) := by
+    (∑ i : Fin k, (f i)).1 j = (∑ i : Fin k, (f i).1 j) :=
-  induction k
+  sum_of_anomaly_free_linear (fun i => f i) j
-  simp
-  rfl
-  rename_i _ l hl
-  rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]
-  have hlt := hl (f ∘ Fin.castSucc)
-  erw [← hlt]
-  simp
 
 /-- The coordinate map for the basis. -/
 noncomputable
 def coordinateMap : ((PureU1 n.succ).LinSols) ≃ₗ[ℚ] Fin n →₀ ℚ where
   toFun S := Finsupp.equivFunOnFinite.invFun (S.1 ∘ Fin.castSucc)
-  map_add' S T := by
+  map_add' S T := Finsupp.ext (congrFun rfl)
-    simp only [PureU1_numberCharges, ACCSystemLinear.linSolsAddCommMonoid_add_val,
+  map_smul' a S :=  Finsupp.ext (congrFun rfl)
-      Equiv.invFun_as_coe]
-    ext
-    simp
-  map_smul' a S := by
-    simp only [PureU1_numberCharges, Equiv.invFun_as_coe, eq_ratCast, Rat.cast_eq_id, id_eq]
-    ext
-    simp
-    rfl
   invFun f := ∑ i : Fin n, f i • asLinSols i
   left_inv S := by
     simp only [PureU1_numberCharges, Equiv.invFun_as_coe, Finsupp.equivFunOnFinite_symm_apply_toFun,
@@ -122,7 +100,7 @@ def coordinateMap : ((PureU1 n.succ).LinSols) ≃ₗ[ℚ] Fin n →₀ ℚ where
     simp only [asCharges, PureU1_numberCharges, ↓reduceIte, mul_one]
     intro k _ hkj
     rw [asCharges_ne_castSucc hkj]
-    simp only [mul_zero]
+    exact Rat.mul_zero (S.val k.castSucc)
     simp
   right_inv f := by
     simp only [PureU1_numberCharges, Equiv.invFun_as_coe]
@@ -137,7 +115,7 @@ def coordinateMap : ((PureU1 n.succ).LinSols) ≃ₗ[ℚ] Fin n →₀ ℚ where
     simp only [asCharges, PureU1_numberCharges, ↓reduceIte, mul_one]
     intro k _ hkj
     rw [asCharges_ne_castSucc hkj]
-    simp only [mul_zero]
+    exact Rat.mul_zero (f k)
     simp
 
 /-- The basis of `LinSols`.-/
@@ -151,11 +129,8 @@ instance : Module.Finite ℚ ((PureU1 n.succ).LinSols) :=
 lemma finrank_AnomalyFreeLinear :
     FiniteDimensional.finrank ℚ (((PureU1 n.succ).LinSols)) = n := by
   have h  :=  Module.mk_finrank_eq_card_basis (@asBasis n)
-  simp_all
+  simp only [Nat.succ_eq_add_one, finrank_eq_rank, Cardinal.mk_fintype, Fintype.card_fin] at h
-  simp [FiniteDimensional.finrank]
+  exact FiniteDimensional.finrank_eq_of_rank_eq h
-  rw [h]
-  simp_all only [Cardinal.toNat_natCast]
-
 
 end BasisLinear
 

HepLean/AnomalyCancellation/PureU1/LowDim/One.lean

@@ -27,7 +27,7 @@ theorem solEqZero (S : (PureU1 1).LinSols) : S = 0 := by
   simp at hLin
   funext i
   simp at i
-  rw [show i = (0 : Fin 1) by omega]
+  rw [show i = (0 : Fin 1) from Fin.fin_one_eq_zero i]
   exact hLin
 
 end One

HepLean/AnomalyCancellation/PureU1/LowDim/Three.lean

@@ -38,7 +38,7 @@ lemma cube_for_linSol (S : (PureU1 3).LinSols) :
     (PureU1 3).cubicACC S.val = 0 := by
   rw [← cube_for_linSol']
   simp only [Fin.isValue, _root_.mul_eq_zero, OfNat.ofNat_ne_zero, false_or]
-  rw [@or_assoc]
+  exact Iff.symm or_assoc
 
 lemma three_sol_zero (S : (PureU1 3).Sols) : S.val (0 : Fin 3) = 0 ∨ S.val (1 : Fin 3) = 0
     ∨ S.val (2 : Fin 3) = 0 := (cube_for_linSol S.1.1).mpr S.cubicSol

HepLean/AnomalyCancellation/PureU1/LowDim/Two.lean

@@ -28,7 +28,7 @@ def equiv : (PureU1 2).LinSols ≃ (PureU1 2).Sols where
     simp at hLin
     erw [accCube_explicit]
     simp only [Fin.sum_univ_two, Fin.isValue]
-    rw [show S.val (0 : Fin 2) = - S.val (1 : Fin 2) by linear_combination hLin]
+    rw [show S.val (0 : Fin 2) = - S.val (1 : Fin 2) from eq_neg_of_add_eq_zero_left hLin]
     ring⟩
   invFun S := S.1.1
   left_inv S := rfl

HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean

@@ -47,13 +47,8 @@ lemma chargesMapOfSpeciesMap_toSpecies {n m : ℕ}
 def speciesFamilyProj {m n : ℕ} (h : n ≤ m) :
     (SMνSpecies m).charges →ₗ[ℚ] (SMνSpecies n).charges where
   toFun S := S ∘ Fin.castLE h
-  map_add' S T := by
+  map_add' _ _ := rfl
-    funext i
+  map_smul' _ _ := rfl
-    simp
-  map_smul' a S := by
-    funext i
-    simp [HSMul.hSMul]
-    -- rw [show Rat.cast a = a from rfl]
 
 /-- The projection of the `m`-family charges onto the first `n`-family charges.  -/
 def familyProjection {m n : ℕ} (h : n ≤ m) : (SMνCharges m).charges →ₗ[ℚ] (SMνCharges n).charges :=
@@ -82,7 +77,8 @@ def speciesEmbed (m n : ℕ) :
     by_cases hi : i.val < m
     erw [dif_pos hi, dif_pos hi]
     erw [dif_neg hi, dif_neg hi]
-    simp
+    exact Eq.symm (Rat.mul_zero a)
+
 
 /-- The embedding of the `m`-family charges onto the `n`-family charges, with all
 other charges zero.  -/
@@ -95,13 +91,8 @@ a universal manor. -/
 def speciesFamilyUniversial (n : ℕ) :
     (SMνSpecies 1).charges →ₗ[ℚ] (SMνSpecies n).charges where
   toFun S _ := S ⟨0, by simp⟩
-  map_add' S T := by
+  map_add' S T := rfl
-    funext _
+  map_smul' a S := rfl
-    simp
-  map_smul' a S := by
-    funext i
-    simp [HSMul.hSMul]
-    -- rw [show Rat.cast a = a from rfl]
 
 /-- The embedding of the `1`-family charges into the `n`-family charges in
 a universal manor. -/

HepLean/AnomalyCancellation/SMNu/Permutations.lean

@@ -37,25 +37,14 @@ instance : Group (permGroup n) := Pi.group
 @[simps!]
 def chargeMap (f : permGroup n) : (SMνCharges n).charges →ₗ[ℚ] (SMνCharges n).charges where
   toFun S := toSpeciesEquiv.symm (fun i => toSpecies i S ∘ f i )
-  map_add' S T := by
+  map_add' _ _ := rfl
-    simp only
+  map_smul' _ _ := rfl
-    rw [charges_eq_toSpecies_eq]
-    intro i
-    rw [(toSpecies i).map_add]
-    rw [toSMSpecies_toSpecies_inv, toSMSpecies_toSpecies_inv, toSMSpecies_toSpecies_inv]
-    rfl
-  map_smul' a S := by
-    simp only
-    rw [charges_eq_toSpecies_eq]
-    intro i
-    rw [(toSpecies i).map_smul, toSMSpecies_toSpecies_inv, toSMSpecies_toSpecies_inv]
-    rfl
 
 /-- The representation of `(permGroup n)` acting on the vector space of charges. -/
 @[simp]
 def repCharges {n : ℕ} : Representation ℚ (permGroup n) (SMνCharges n).charges where
   toFun f := chargeMap f⁻¹
-  map_mul' f g :=by
+  map_mul' f g := by
     simp only [permGroup, mul_inv_rev]
     apply LinearMap.ext
     intro S