Merge pull request #14 from HEPLean/Workflows

feat: Update mathlib and std
HEPLean · Apr 29, 2024 · 22d784b · 22d784b
2 parents cee6082 + 2094044
commit 22d784b
Show file tree

Hide file tree

Showing 6 changed files with 23 additions and 20 deletions.
diff --git a/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean b/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
@@ -260,11 +260,10 @@ def bijectionLinearParameters :
     field_simp
     ring_nf
     field_simp [hQ, hE]
-    ring
+    ring_nf
     field_simp
     ring_nf
     field_simp [hQ, hE]
-    ring
 
 /-- The bijection between `linearParametersQENeqZero` and `LinSols` with `Q` and `E` non-zero. -/
 def bijection : linearParametersQENeqZero ≃

diff --git a/HepLean/FlavorPhysics/CKMMatrix/Relations.lean b/HepLean/FlavorPhysics/CKMMatrix/Relations.lean
@@ -206,8 +206,8 @@ lemma conj_Vtb_mul_Vud {V : CKMMatrix} {τ : ℝ}
   simp [exp_neg]
   have h1 := exp_ne_zero (τ * I)
   field_simp
-  have h2 : cexp (τ * I) * ([V]cs * [V]ud - [V]us * [V]cd) * conj [V]ud = cexp (τ * I) * [V]cs
-      * [V]ud * conj [V]ud - cexp (τ * I) * [V]us * ([V]cd * conj [V]ud) := by
+  have h2 : ([V]cs * [V]ud - [V]us * [V]cd) * conj [V]ud =  [V]cs
+      * [V]ud * conj [V]ud - [V]us * ([V]cd * conj [V]ud) := by
     ring
   rw [h2, V.Vcd_mul_conj_Vud]
   rw [normSq_eq_conj_mul_self, normSq_eq_conj_mul_self]
@@ -222,8 +222,8 @@ lemma conj_Vtb_mul_Vus {V : CKMMatrix} {τ : ℝ}
   simp [exp_neg]
   have h1 := exp_ne_zero (τ * I)
   field_simp
-  have h2 : cexp (τ * I) * ([V]cs * [V]ud - [V]us * [V]cd) * conj [V]us = cexp (τ * I) * ([V]cs
-      * conj [V]us) * [V]ud - cexp (τ * I) * [V]us * [V]cd * conj [V]us := by
+  have h2 :  ([V]cs * [V]ud - [V]us * [V]cd) * conj [V]us = ([V]cs
+      * conj [V]us) * [V]ud - [V]us * [V]cd * conj [V]us := by
     ring
   rw [h2, V.Vcs_mul_conj_Vus]
   rw [normSq_eq_conj_mul_self, normSq_eq_conj_mul_self]

diff --git a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean
@@ -424,16 +424,16 @@ lemma on_param_cos_θ₁₂_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.c
   simp only [mul_zero, add_zero, neg_inj]
   field_simp
   ring
-  ring
+  ring_nf
   field_simp
-  ring
+  ring_nf
   change _ = _ + _ * 0
   simp only [mul_zero, add_zero]
   field_simp
   ring
-  ring
+  ring_nf
   field_simp
-  ring
+
 
 lemma on_param_cos_θ₂₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.cos (θ₂₃ ⟦V⟧) = 0) :
     standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by
@@ -450,7 +450,7 @@ lemma on_param_cos_θ₂₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.c
   simp only [mul_zero, add_zero]
   ring
   field_simp
-  ring
+
 
 lemma on_param_sin_θ₁₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.sin (θ₁₃ ⟦V⟧) = 0) :
     standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by
@@ -478,16 +478,16 @@ lemma on_param_sin_θ₁₂_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.s
   simp only [mul_zero, add_zero, neg_inj]
   ring
   field_simp
-  ring
+  ring_nf
   field_simp
-  ring
+  ring_nf
   change _ = _ + _ * 0
   simp only [mul_zero, add_zero, neg_inj]
-  ring
+  ring_nf
   field_simp
-  ring
+  ring_nf
   field_simp
-  ring
+
 
 
 lemma on_param_sin_θ₂₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.sin (θ₂₃ ⟦V⟧) = 0) :
@@ -505,7 +505,7 @@ lemma on_param_sin_θ₂₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.s
   ring
   ring
   field_simp
-  ring
+
 
 
 

diff --git a/README.md b/README.md
@@ -15,7 +15,7 @@
 
 - Watch this overview of HepLean:
 
-  https://www.youtube.com/watch?v=W2cObnopqas&t=3s
+  https://www.youtube.com/watch?v=W2cObnopqas
 - A list of 'Frequently asked questions' can be found on the Wiki for this project: 
 
   https://github.com/HEPLean/HepLean/wiki/The-answers-to-some-questions

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a",
+   "rev": "e840c18f7334c751efbd4cfe531476e10c943cdb",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,7 +58,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "85a47191abb7957cdc53c5c2b59aef219bd8f6d9",
+   "rev": "0924a3d4e9b4a3950b43673d4b93bbbf6d34c9a6",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,

diff --git a/scripts/update-lean-mathlib.sh b/scripts/update-lean-mathlib.sh
@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+
+lake update 
+