chore: bump to v4.16.0

HepLean/Lorentz/Weyl/Basic.lean

@@ -52,7 +52,7 @@ lemma leftBasis_ρ_apply (M : SL(2,ℂ)) (i j : Fin 2) :
   rw [LinearMap.toMatrix_apply]
   simp only [leftBasis, Basis.coe_ofEquivFun, Basis.ofEquivFun_repr_apply]
   change (M.1 *ᵥ (Pi.single j 1)) i = _
-  simp only [mulVec_single, mul_one]
+  simp only [mulVec_single, MulOpposite.op_one, Pi.smul_apply, transpose_apply, one_smul]
 
 @[simp]
 lemma leftBasis_toFin2ℂ (i : Fin 2) : (leftBasis i).toFin2ℂ = Pi.single i 1 := by
@@ -97,7 +97,7 @@ lemma altLeftBasis_ρ_apply (M : SL(2,ℂ)) (i j : Fin 2) :
   rw [LinearMap.toMatrix_apply]
   simp only [altLeftBasis, Basis.coe_ofEquivFun, Basis.ofEquivFun_repr_apply, transpose_apply]
   change ((M.1⁻¹)ᵀ *ᵥ (Pi.single j 1)) i = _
-  simp only [mulVec_single, transpose_apply, mul_one]
+  simp only [mulVec_single, MulOpposite.op_one, transpose_transpose, Pi.smul_apply, one_smul]
 
 /-- The vector space ℂ^2 carrying the conjugate representation of SL(2,C).
   In index notation corresponds to a Weyl fermion with indices ψ^{dot a}. -/
@@ -134,7 +134,7 @@ lemma rightBasis_ρ_apply (M : SL(2,ℂ)) (i j : Fin 2) :
   rw [LinearMap.toMatrix_apply]
   simp only [rightBasis, Basis.coe_ofEquivFun, Basis.ofEquivFun_repr_apply, transpose_apply]
   change (M.1.map star *ᵥ (Pi.single j 1)) i = _
-  simp only [mulVec_single, transpose_apply, mul_one]
+  simp [mulVec_single, transpose_apply, mul_one]
 
 /-- The vector space ℂ^2 carrying the representation of SL(2,C) given by
     M → (M⁻¹)^†.
@@ -176,7 +176,7 @@ lemma altRightBasis_ρ_apply (M : SL(2,ℂ)) (i j : Fin 2) :
   rw [LinearMap.toMatrix_apply]
   simp only [altRightBasis, Basis.coe_ofEquivFun, Basis.ofEquivFun_repr_apply, transpose_apply]
   change ((M.1⁻¹).conjTranspose *ᵥ (Pi.single j 1)) i = _
-  simp only [mulVec_single, transpose_apply, mul_one]
+  simp [mulVec_single, transpose_apply, mul_one]
 
 /-!
 

HepLean/Lorentz/Weyl/Metric.lean

@@ -108,7 +108,7 @@ def leftMetric : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ leftHanded ⊗ leftHanded where
       not_false_eq_true, mul_nonsing_inv, transpose_one, mul_one]
 
 lemma leftMetric_apply_one : leftMetric.hom (1 : ℂ) = leftMetricVal := by
-  change leftMetric.hom.hom.toFun (1 : ℂ) = leftMetricVal
+  change (1 : ℂ) • leftMetricVal = leftMetricVal
   simp only [leftMetric, one_smul]
 
 /-- The metric `εₐₐ` as an element of `(altLeftHanded ⊗ altLeftHanded).V`. -/
@@ -155,7 +155,7 @@ def altLeftMetric : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altLeftHanded ⊗ altLeftHande
       not_false_eq_true, mul_nonsing_inv, mul_one]
 
 lemma altLeftMetric_apply_one : altLeftMetric.hom (1 : ℂ) = altLeftMetricVal := by
-  change altLeftMetric.hom.hom.toFun (1 : ℂ) = altLeftMetricVal
+  change (1 : ℂ) • altLeftMetricVal = altLeftMetricVal
   simp only [altLeftMetric, one_smul]
 
 /-- The metric `ε^{dot a}^{dot a}` as an element of `(rightHanded ⊗ rightHanded).V`. -/
@@ -209,7 +209,7 @@ def rightMetric : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ rightHanded ⊗ rightHanded wher
       rfl
 
 lemma rightMetric_apply_one : rightMetric.hom (1 : ℂ) = rightMetricVal := by
-  change rightMetric.hom.hom.toFun (1 : ℂ) = rightMetricVal
+  change (1 : ℂ) • rightMetricVal = rightMetricVal
   simp only [rightMetric, one_smul]
 
 /-- The metric `ε_{dot a}_{dot a}` as an element of `(altRightHanded ⊗ altRightHanded).V`. -/
@@ -267,7 +267,7 @@ def altRightMetric : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altRightHanded ⊗ altRightHa
       rfl
 
 lemma altRightMetric_apply_one : altRightMetric.hom (1 : ℂ) = altRightMetricVal := by
-  change altRightMetric.hom.hom.toFun (1 : ℂ) = altRightMetricVal
+  change (1 : ℂ) • altRightMetricVal = altRightMetricVal
   simp only [altRightMetric, one_smul]
 
 /-!

HepLean/Lorentz/Weyl/Unit.lean

@@ -61,7 +61,7 @@ def leftAltLeftUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ leftHanded ⊗ altLeftHanded
     simp
 
 lemma leftAltLeftUnit_apply_one : leftAltLeftUnit.hom (1 : ℂ) = leftAltLeftUnitVal := by
-  change leftAltLeftUnit.hom.hom.toFun (1 : ℂ) = leftAltLeftUnitVal
+  change (1 : ℂ) • leftAltLeftUnitVal = leftAltLeftUnitVal
   simp only [leftAltLeftUnit, one_smul]
 
 /-- The alt-left-left unit `δₐᵃ` as an element of `(altLeftHanded ⊗ leftHanded).V`. -/
@@ -106,7 +106,7 @@ def altLeftLeftUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altLeftHanded ⊗ leftHanded
 
 /-- Applying the morphism `altLeftLeftUnit` to `1` returns `altLeftLeftUnitVal`. -/
 lemma altLeftLeftUnit_apply_one : altLeftLeftUnit.hom (1 : ℂ) = altLeftLeftUnitVal := by
-  change altLeftLeftUnit.hom.hom.toFun (1 : ℂ) = altLeftLeftUnitVal
+  change (1 : ℂ) • altLeftLeftUnitVal = altLeftLeftUnitVal
   simp only [altLeftLeftUnit, one_smul]
 
 /-- The right-alt-right unit `δ^{dot a}_{dot a}` as an element of
@@ -157,7 +157,7 @@ def rightAltRightUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ rightHanded ⊗ altRightHa
     simp
 
 lemma rightAltRightUnit_apply_one : rightAltRightUnit.hom (1 : ℂ) = rightAltRightUnitVal := by
-  change rightAltRightUnit.hom.hom.toFun (1 : ℂ) = rightAltRightUnitVal
+  change (1 : ℂ) • rightAltRightUnitVal  = rightAltRightUnitVal
   simp only [rightAltRightUnit, one_smul]
 
 /-- The alt-right-right unit `δ_{dot a}^{dot a}` as an element of
@@ -206,7 +206,7 @@ def altRightRightUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altRightHanded ⊗ rightHa
     simp
 
 lemma altRightRightUnit_apply_one : altRightRightUnit.hom (1 : ℂ) = altRightRightUnitVal := by
-  change altRightRightUnit.hom.hom.toFun (1 : ℂ) = altRightRightUnitVal
+  change (1 : ℂ) • altRightRightUnitVal = altRightRightUnitVal
   simp only [altRightRightUnit, one_smul]
 
 /-!
@@ -236,7 +236,7 @@ lemma contr_altLeftLeftUnit (x : leftHanded) :
   erw [h1, h1, h1, h1]
   repeat rw [leftAltContraction_basis]
   simp only [Fin.isValue, leftUnitor, ModuleCat.MonoidalCategory.leftUnitor, ModuleCat.of_coe,
-    CategoryTheory.Iso.trans_hom, LinearEquiv.toModuleIso_hom_hom, ModuleCat.ofSelfIso_hom,
+    CategoryTheory.Iso.trans_hom, ModuleCat.ofSelfIso_hom,
     CategoryTheory.Category.comp_id, Action.instMonoidalCategory_tensorUnit_V, Fin.val_zero,
     ↓reduceIte, Fin.val_one, one_ne_zero, zero_tmul, map_zero, smul_zero, add_zero, zero_ne_one,
     zero_add]