chore: bump toolchain to v4.15.0

#281 adapt code to v4.15.0 and fix long heartbeats, e.g., toDualRep_apply_eq_contrOneTwoLeft. --------- Co-authored-by: jstoobysmith <[email protected]>
HEPLean · Jan 20, 2025 · 656a3e4 · 656a3e4
1 parent 6e31281
commit 656a3e4
Show file tree

Hide file tree

Showing 49 changed files with 484 additions and 472 deletions.
diff --git a/Archive/Papers/1907_00514.lean b/Archive/Papers/1907_00514.lean
@@ -17,6 +17,7 @@ import Mathlib.Tactic.FieldSimp
 import Mathlib.Tactic.Linarith
 import Mathlib.NumberTheory.FLT.Basic
 import Mathlib.Algebra.QuadraticDiscriminant
+import Mathlib.Tactic.LinearCombination'
 /-!
 DO NOT USE THIS FILE AS AN IMPORT.
 
@@ -81,7 +82,7 @@ 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]
-      exact Mathlib.Tactic.LinearCombination.add_pf (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]
@@ -625,7 +626,6 @@ def bijection : linearParameters ≃ (SMNoGrav 1).LinSols where
     rw [asLinear_val]
     funext j
     have hj : j = (0 : Fin 1) := by
-      simp only [Fin.isValue]
       ext
       simp
     subst hj
@@ -784,13 +784,13 @@ lemma cubic_v_zero (S : linearParametersQENeqZero) (h : accCube (bijection S).1.
   have h' : (S.w + 1) * (1 * S.w * S.w + (-1) * S.w + 1) = 0 := by
     ring_nf
     exact add_eq_zero_iff_neg_eq.mpr (id (Eq.symm h))
-  have h'' : (1 * S.w * S.w + (-1) * S.w + 1) ≠ 0 := by
+  have h'' : (1 * (S.w * S.w) + (-1) * S.w + 1) ≠ 0 := by
     refine quadratic_ne_zero_of_discrim_ne_sq ?_ S.w
     intro s
     by_contra hn
     have h : s ^ 2 < 0 := by
       rw [← hn]
-      rfl
+      decide +kernel
     nlinarith
   simp_all
   exact eq_neg_of_add_eq_zero_left h'
@@ -802,13 +802,13 @@ lemma cube_w_zero (S : linearParametersQENeqZero) (h : accCube (bijection S).1.v
   have h' : (S.v + 1) * (1 * S.v * S.v + (-1) * S.v + 1) = 0 := by
     ring_nf
     exact add_eq_zero_iff_neg_eq.mpr (id (Eq.symm h))
-  have h'' : (1 * S.v * S.v + (-1) * S.v + 1) ≠ 0 := by
+  have h'' : (1 * (S.v * S.v) + (-1) * S.v + 1) ≠ 0 := by
     refine quadratic_ne_zero_of_discrim_ne_sq ?_ S.v
     intro s
     by_contra hn
     have h : s ^ 2 < 0 := by
       rw [← hn]
-      rfl
+      decide +kernel
     nlinarith
   simp_all
   exact eq_neg_of_add_eq_zero_left h'

diff --git a/HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean b/HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean
@@ -116,7 +116,6 @@ theorem generic_case {S : (PureU1 (2 * n.succ)).Sols} (h : GenericCase S) :
   rw [parameterization]
   apply ACCSystem.Sols.ext
   rw [parameterizationAsLinear_val]
-  change S.val = _ • (_ • P g + _• P! f)
   rw [anomalyFree_param _ _ hS]
   rw [neg_neg, ← smul_add, smul_smul, inv_mul_cancel₀, one_smul]
   · exact hS

diff --git a/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean b/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.AnomalyCancellation.PureU1.ConstAbs
+import Mathlib.Tactic.FieldSimp
 /-!
 # Line in plane condition
 

diff --git a/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean b/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean
@@ -515,7 +515,6 @@ lemma Pa_zero (f g : Fin n.succ → ℚ) (h : Pa f g = 0) :
   have h₃ := Pa_oddShiftShiftZero f g
   rw [h] at h₃
   change 0 = _ at h₃
-  simp only at h₃
   intro i
   have hinduc (iv : ℕ) (hiv : iv < n.succ) : f ⟨iv, hiv⟩ = 0 := by
     induction iv

diff --git a/HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean b/HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean
@@ -118,7 +118,6 @@ theorem generic_case {S : (PureU1 (2 * n.succ + 1)).Sols} (h : GenericCase S) :
   rw [parameterization]
   apply ACCSystem.Sols.ext
   rw [parameterizationAsLinear_val]
-  change S.val = _ • (_ • P g + _• P! f)
   rw [anomalyFree_param _ _ hS, neg_neg, ← smul_add, smul_smul, inv_mul_cancel₀, one_smul]
   · exact hS
   · simpa only [Nat.succ_eq_add_one, accCubeTriLinSymm_toFun_apply_apply, ne_eq,

diff --git a/HepLean/AnomalyCancellation/PureU1/Permutations.lean b/HepLean/AnomalyCancellation/PureU1/Permutations.lean
@@ -5,6 +5,7 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.AnomalyCancellation.PureU1.Basic
 import HepLean.AnomalyCancellation.GroupActions
+import Mathlib.Logic.Equiv.Fintype
 /-!
 # Permutations of Pure U(1) ACC
 

diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSol.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSol.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.AnomalyCancellation.SMNu.PlusU1.Basic
+import Mathlib.Tactic.FieldSimp
 /-!
 # Properties of Quad Sols for SM with RHN
 

diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSolToSol.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSolToSol.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.AnomalyCancellation.SMNu.PlusU1.BMinusL
+import Mathlib.Tactic.FieldSimp
 /-!
 # Solutions from quad solutions
 

diff --git a/HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean b/HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean
@@ -51,14 +51,14 @@ variable (P : Potential) (Φ1 Φ2 : HiggsField)
 
 /-- The potential of the two Higgs doublet model. -/
 def toFun (Φ1 Φ2 : HiggsField) (x : SpaceTime) : ℝ :=
-  P.m₁₁2 * ‖Φ1‖_H ^ 2 x + P.m₂₂2 * ‖Φ2‖_H ^ 2 x -
+  P.m₁₁2 * ‖Φ1‖_H^2 x + P.m₂₂2 * ‖Φ2‖_H^2 x -
   (P.m₁₂2 * ⟪Φ1, Φ2⟫_H x + conj P.m₁₂2 * ⟪Φ2, Φ1⟫_H x).re
-  + 1/2 * P.𝓵₁ * ‖Φ1‖_H ^ 2 x * ‖Φ1‖_H ^ 2 x + 1/2 * P.𝓵₂ * ‖Φ2‖_H ^ 2 x * ‖Φ2‖_H ^ 2 x
-  + P.𝓵₃ * ‖Φ1‖_H ^ 2 x * ‖Φ2‖_H ^ 2 x
+  + 1/2 * P.𝓵₁ * ‖Φ1‖_H^2 x * ‖Φ1‖_H^2 x + 1/2 * P.𝓵₂ * ‖Φ2‖_H^2 x * ‖Φ2‖_H^2 x
+  + P.𝓵₃ * ‖Φ1‖_H^2 x * ‖Φ2‖_H^2 x
   + P.𝓵₄ * ‖⟪Φ1, Φ2⟫_H x‖ ^ 2
   + (1/2 * P.𝓵₅ * ⟪Φ1, Φ2⟫_H x ^ 2 + 1/2 * conj P.𝓵₅ * ⟪Φ2, Φ1⟫_H x ^ 2).re
-  + (P.𝓵₆ * ‖Φ1‖_H ^ 2 x * ⟪Φ1, Φ2⟫_H x + conj P.𝓵₆ * ‖Φ1‖_H ^ 2 x * ⟪Φ2, Φ1⟫_H x).re
-  + (P.𝓵₇ * ‖Φ2‖_H ^ 2 x * ⟪Φ1, Φ2⟫_H x + conj P.𝓵₇ * ‖Φ2‖_H ^ 2 x * ⟪Φ2, Φ1⟫_H x).re
+  + (P.𝓵₆ * ‖Φ1‖_H^2 x * ⟪Φ1, Φ2⟫_H x + conj P.𝓵₆ * ‖Φ1‖_H^2 x * ⟪Φ2, Φ1⟫_H x).re
+  + (P.𝓵₇ * ‖Φ2‖_H^2 x * ⟪Φ1, Φ2⟫_H x + conj P.𝓵₇ * ‖Φ2‖_H^2 x * ⟪Φ2, Φ1⟫_H x).re
 
 /-- The potential where all parameters are zero. -/
 def zero : Potential := ⟨0, 0, 0, 0, 0, 0, 0, 0, 0, 0⟩

diff --git a/HepLean/Lorentz/ComplexTensor/Basic.lean b/HepLean/Lorentz/ComplexTensor/Basic.lean
@@ -187,12 +187,66 @@ def complexLorentzTensor : TensorSpecies where
     | Color.down => Lorentz.contrCoUnit_symm
   contr_metric := fun c =>
     match c with
-    | Color.upL => by simpa using Fermion.leftAltContraction_apply_metric
-    | Color.downL => by simpa using Fermion.altLeftContraction_apply_metric
-    | Color.upR => by simpa using Fermion.rightAltContraction_apply_metric
-    | Color.downR => by simpa using Fermion.altRightContraction_apply_metric
-    | Color.up => by simpa using Lorentz.contrCoContraction_apply_metric
-    | Color.down => by simpa using Lorentz.coContrContraction_apply_metric
+    | Color.upL => by
+      simp only [Discrete.functor_obj_eq_as, Action.instMonoidalCategory_tensorObj_V,
+        Action.instMonoidalCategory_tensorUnit_V, Action.instMonoidalCategory_whiskerLeft_hom,
+        Action.instMonoidalCategory_leftUnitor_hom_hom, Monoidal.tensorUnit_obj,
+        Discrete.natTrans_app, Action.instMonoidalCategory_whiskerRight_hom,
+        Action.instMonoidalCategory_associator_inv_hom,
+        Action.instMonoidalCategory_associator_hom_hom, Equivalence.symm_inverse,
+        Action.functorCategoryEquivalence_functor,
+        Action.FunctorCategoryEquivalence.functor_obj_obj]
+      exact Fermion.leftAltContraction_apply_metric
+    | Color.downL => by
+      simp only [Discrete.functor_obj_eq_as, Action.instMonoidalCategory_tensorObj_V,
+        Action.instMonoidalCategory_tensorUnit_V, Action.instMonoidalCategory_whiskerLeft_hom,
+        Action.instMonoidalCategory_leftUnitor_hom_hom, Monoidal.tensorUnit_obj,
+        Discrete.natTrans_app, Action.instMonoidalCategory_whiskerRight_hom,
+        Action.instMonoidalCategory_associator_inv_hom,
+        Action.instMonoidalCategory_associator_hom_hom, Equivalence.symm_inverse,
+        Action.functorCategoryEquivalence_functor,
+        Action.FunctorCategoryEquivalence.functor_obj_obj]
+      exact Fermion.altLeftContraction_apply_metric
+    | Color.upR => by
+      simp only [Discrete.functor_obj_eq_as, Action.instMonoidalCategory_tensorObj_V,
+        Action.instMonoidalCategory_tensorUnit_V, Action.instMonoidalCategory_whiskerLeft_hom,
+        Action.instMonoidalCategory_leftUnitor_hom_hom, Monoidal.tensorUnit_obj,
+        Discrete.natTrans_app, Action.instMonoidalCategory_whiskerRight_hom,
+        Action.instMonoidalCategory_associator_inv_hom,
+        Action.instMonoidalCategory_associator_hom_hom, Equivalence.symm_inverse,
+        Action.functorCategoryEquivalence_functor,
+        Action.FunctorCategoryEquivalence.functor_obj_obj]
+      exact Fermion.rightAltContraction_apply_metric
+    | Color.downR => by
+      simp only [Discrete.functor_obj_eq_as, Action.instMonoidalCategory_tensorObj_V,
+        Action.instMonoidalCategory_tensorUnit_V, Action.instMonoidalCategory_whiskerLeft_hom,
+        Action.instMonoidalCategory_leftUnitor_hom_hom, Monoidal.tensorUnit_obj,
+        Discrete.natTrans_app, Action.instMonoidalCategory_whiskerRight_hom,
+        Action.instMonoidalCategory_associator_inv_hom,
+        Action.instMonoidalCategory_associator_hom_hom, Equivalence.symm_inverse,
+        Action.functorCategoryEquivalence_functor,
+        Action.FunctorCategoryEquivalence.functor_obj_obj]
+      exact Fermion.altRightContraction_apply_metric
+    | Color.up => by
+      simp only [Discrete.functor_obj_eq_as, Action.instMonoidalCategory_tensorObj_V,
+        Action.instMonoidalCategory_tensorUnit_V, Action.instMonoidalCategory_whiskerLeft_hom,
+        Action.instMonoidalCategory_leftUnitor_hom_hom, Monoidal.tensorUnit_obj,
+        Discrete.natTrans_app, Action.instMonoidalCategory_whiskerRight_hom,
+        Action.instMonoidalCategory_associator_inv_hom,
+        Action.instMonoidalCategory_associator_hom_hom, Equivalence.symm_inverse,
+        Action.functorCategoryEquivalence_functor,
+        Action.FunctorCategoryEquivalence.functor_obj_obj]
+      exact Lorentz.contrCoContraction_apply_metric
+    | Color.down => by
+      simp only [Discrete.functor_obj_eq_as, Action.instMonoidalCategory_tensorObj_V,
+        Action.instMonoidalCategory_tensorUnit_V, Action.instMonoidalCategory_whiskerLeft_hom,
+        Action.instMonoidalCategory_leftUnitor_hom_hom, Monoidal.tensorUnit_obj,
+        Discrete.natTrans_app, Action.instMonoidalCategory_whiskerRight_hom,
+        Action.instMonoidalCategory_associator_inv_hom,
+        Action.instMonoidalCategory_associator_hom_hom, Equivalence.symm_inverse,
+        Action.functorCategoryEquivalence_functor,
+        Action.FunctorCategoryEquivalence.functor_obj_obj]
+      exact Lorentz.coContrContraction_apply_metric
 
 namespace complexLorentzTensor
 

diff --git a/HepLean/Lorentz/ComplexVector/Contraction.lean b/HepLean/Lorentz/ComplexVector/Contraction.lean
@@ -73,8 +73,8 @@ def contrContrCoBi : complexCo →ₗ[ℂ] complexContr →ₗ[ℂ] ℂ where
     standard basis (i.e. the dot product).
     In terms of index notation this is the contraction is ψⁱ φᵢ. -/
 def contrCoContraction : complexContr ⊗ complexCo ⟶ 𝟙_ (Rep ℂ SL(2,ℂ)) where
-  hom := TensorProduct.lift contrCoContrBi
-  comm M := TensorProduct.ext' fun ψ φ => by
+  hom := ModuleCat.ofHom <| TensorProduct.lift contrCoContrBi
+  comm M := ModuleCat.hom_ext <| TensorProduct.ext' fun ψ φ => by
     change ((LorentzGroup.toComplex (SL2C.toLorentzGroup M)) *ᵥ ψ.toFin13ℂ) ⬝ᵥ
       ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ *ᵥ φ.toFin13ℂ) = ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂ
     rw [dotProduct_mulVec, vecMul_transpose, mulVec_mulVec]
@@ -113,8 +113,8 @@ lemma contrCoContraction_basis' (i j : Fin 1 ⊕ Fin 3) :
     standard basis (i.e. the dot product).
     In terms of index notation this is the contraction is φᵢ ψⁱ. -/
 def coContrContraction : complexCo ⊗ complexContr ⟶ 𝟙_ (Rep ℂ SL(2,ℂ)) where
-  hom := TensorProduct.lift contrContrCoBi
-  comm M := TensorProduct.ext' fun φ ψ => by
+  hom := ModuleCat.ofHom <| TensorProduct.lift contrContrCoBi
+  comm M := ModuleCat.hom_ext <| TensorProduct.ext' fun φ ψ => by
     change ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ *ᵥ φ.toFin13ℂ) ⬝ᵥ
       ((LorentzGroup.toComplex (SL2C.toLorentzGroup M)) *ᵥ ψ.toFin13ℂ) = φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂ
     rw [dotProduct_mulVec, mulVec_transpose, vecMul_vecMul]

diff --git a/HepLean/Lorentz/ComplexVector/Metric.lean b/HepLean/Lorentz/ComplexVector/Metric.lean
@@ -42,7 +42,7 @@ lemma contrMetricVal_expand_tmul : contrMetricVal =
 /-- The metric `ηᵃᵃ` as a morphism `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ complexContr`,
   making its invariance under the action of `SL(2,ℂ)`. -/
 def contrMetric : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ complexContr where
-  hom := {
+  hom := ModuleCat.ofHom {
     toFun := fun a =>
       let a' : ℂ := a
       a' • contrMetricVal,
@@ -52,13 +52,13 @@ def contrMetric : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ complexContr wh
       simp only [smul_smul]
       rfl}
   comm M := by
-    ext x : 2
+    refine ModuleCat.hom_ext ?_
+    refine LinearMap.ext fun x : ℂ => ?_
     simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
-      Action.tensorUnit_ρ', CategoryTheory.Category.id_comp, Action.tensor_ρ', ModuleCat.coe_comp,
+      Action.tensorUnit_ρ', CategoryTheory.Category.id_comp, Action.tensor_ρ', ModuleCat.hom_comp,
       Function.comp_apply]
-    let x' : ℂ := x
-    change x' • contrMetricVal =
-      (TensorProduct.map (complexContr.ρ M) (complexContr.ρ M)) (x' • contrMetricVal)
+    change x • contrMetricVal =
+      (TensorProduct.map (complexContr.ρ M) (complexContr.ρ M)) (x • contrMetricVal)
     simp only [Action.instMonoidalCategory_tensorObj_V, _root_.map_smul]
     apply congrArg
     simp only [Action.instMonoidalCategory_tensorObj_V, contrMetricVal]
@@ -67,9 +67,8 @@ def contrMetric : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ complexContr wh
     simp only [LorentzGroup.toComplex_mul_minkowskiMatrix_mul_transpose]
 
 lemma contrMetric_apply_one : contrMetric.hom (1 : ℂ) = contrMetricVal := by
-  change contrMetric.hom.toFun (1 : ℂ) = contrMetricVal
-  simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
-    contrMetric, AddHom.toFun_eq_coe, AddHom.coe_mk, one_smul]
+  change contrMetric.hom.hom.toFun (1 : ℂ) = contrMetricVal
+  simp only [contrMetric, one_smul]
 
 /-- The metric `ηᵢᵢ` as an element of `(complexCo ⊗ complexCo).V`. -/
 def coMetricVal : (complexCo ⊗ complexCo).V :=
@@ -95,7 +94,7 @@ lemma coMetricVal_expand_tmul : coMetricVal =
 /-- The metric `ηᵢᵢ` as a morphism `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexCo ⊗ complexCo`,
   making its invariance under the action of `SL(2,ℂ)`. -/
 def coMetric : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexCo ⊗ complexCo where
-  hom := {
+  hom := ModuleCat.ofHom {
     toFun := fun a =>
       let a' : ℂ := a
       a' • coMetricVal,
@@ -105,13 +104,13 @@ def coMetric : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexCo ⊗ complexCo where
       simp only [smul_smul]
       rfl}
   comm M := by
-    ext x : 2
+    refine ModuleCat.hom_ext ?_
+    refine LinearMap.ext fun x : ℂ => ?_
     simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
-      Action.tensorUnit_ρ', CategoryTheory.Category.id_comp, Action.tensor_ρ', ModuleCat.coe_comp,
+      Action.tensorUnit_ρ', CategoryTheory.Category.id_comp, Action.tensor_ρ', ModuleCat.hom_comp,
       Function.comp_apply]
-    let x' : ℂ := x
-    change x' • coMetricVal =
-      (TensorProduct.map (complexCo.ρ M) (complexCo.ρ M)) (x' • coMetricVal)
+    change x • coMetricVal =
+      (TensorProduct.map (complexCo.ρ M) (complexCo.ρ M)) (x • coMetricVal)
     simp only [Action.instMonoidalCategory_tensorObj_V, _root_.map_smul]
     apply congrArg
     simp only [Action.instMonoidalCategory_tensorObj_V, coMetricVal]
@@ -122,9 +121,8 @@ def coMetric : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexCo ⊗ complexCo where
       LorentzGroup.toComplex_transpose_mul_minkowskiMatrix_mul_self]
 
 lemma coMetric_apply_one : coMetric.hom (1 : ℂ) = coMetricVal := by
-  change coMetric.hom.toFun (1 : ℂ) = coMetricVal
-  simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
-    coMetric, AddHom.toFun_eq_coe, AddHom.coe_mk, one_smul]
+  change coMetric.hom.hom.toFun (1 : ℂ) = coMetricVal
+  simp only [coMetric, one_smul]
 
 /-!