Merge pull request #17 from HEPLean/Workflows

Update Lean & MathLib versions

.lake/lakefile.olean.trace

@@ -1,4 +1,4 @@
 {"platform": "aarch64-apple-darwin",
  "options": {"env": "dev"},
- "leanHash": "6fce8f7d5cd18a4419bca7fd51780c71c9b1cc5a",
+ "leanHash": "dcccfb73cb247e9478220375ab7de03f7c67e505",
  "configHash": "17439028364340488343"}

HepLean/AnomalyCancellation/PureU1/BasisLinear.lean

@@ -88,7 +88,7 @@ lemma sum_of_vectors {n : ℕ} (f : Fin k → (PureU1 n).LinSols) (j : Fin n) :
   induction k
   simp
   rfl
-  rename_i k l hl
+  rename_i _ l hl
   rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]
   have hlt := hl (f ∘ Fin.castSucc)
   erw [← hlt]

HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean

@@ -64,7 +64,7 @@ lemma lineInPlaneCond_eq_last' {S : (PureU1 (n.succ.succ)).LinSols} (hS : lineIn
   have h1 (i : Fin n) : S.val i.castSucc.castSucc =
       - (S.val ((Fin.last n).castSucc) +  (S.val ((Fin.last n).succ))) / 2 := by
     have h1S := hS (Fin.last n).castSucc ((Fin.last n).succ) i.castSucc.castSucc
-      (by simp; rw [Fin.ext_iff]; simp; omega)
+      (by simp; rw [Fin.ext_iff]; simp)
       (by simp; rw [Fin.ext_iff]; simp; omega)
       (by simp; rw [Fin.ext_iff]; simp; omega)
     simp_all

HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean

@@ -228,7 +228,6 @@ def tolinearParametersQNeqZero (S : {S : linearParameters //  S.Q' ≠  0 ∧ S.
     by
       simp only [ne_eq, neg_add_rev, neg_sub]
       field_simp
-      rw [not_or]
       ring_nf
       simp only [neg_eq_zero, mul_eq_zero, OfNat.ofNat_ne_zero, or_false]
       exact S.2⟩

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "e840c18f7334c751efbd4cfe531476e10c943cdb",
+   "rev": "789020bc2f7fbc330e33818075a94381da04de4e",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,7 +13,7 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "64365c656d5e1bffa127d2a1795f471529ee0178",
+   "rev": "53156671405fbbd5402ed17a79bd129b961bd8d6",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "5fefb40a7c9038a7150e7edd92e43b1b94c49e79",
+   "rev": "0a21a48c286c4a4703c0be6ad2045f601f31b1d0",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -31,16 +31,16 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8",
+   "rev": "fe1eff53bd0838c657aa6126fe4dd75ad9939d9a",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.30",
+   "inputRev": "v0.0.35",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5",
+   "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -49,16 +49,16 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "61a79185b6582573d23bf7e17f2137cd49e7e662",
+   "rev": "7cec59317b9e4f2abbacb986c904614a113e8507",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "0924a3d4e9b4a3950b43673d4b93bbbf6d34c9a6",
+   "rev": "6a170326b1113dfb32dc5623c2b9a00a0e7d543f",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -67,7 +67,7 @@
   {"url": "https://github.com/xubaiw/CMark.lean",
    "type": "git",
    "subDir": null,
-   "rev": "0077cbbaa92abf855fc1c0413e158ffd8195ec77",
+   "rev": "ba7b47bd773954b912ecbf5b1c9993c71a166f05",
    "name": "CMark",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -76,7 +76,7 @@
   {"url": "https://github.com/fgdorais/lean4-unicode-basic",
    "type": "git",
    "subDir": null,
-   "rev": "6a350f4ec7323a4e8ad6bf50736f779853d441e9",
+   "rev": "8b53cc65534bc2c6888c3d4c53a3439648213f74",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -94,7 +94,7 @@
   {"url": "https://github.com/leanprover/doc-gen4",
    "type": "git",
    "subDir": null,
-   "rev": "a34d3c1f7b72654c08abe5741d94794db40dbb2e",
+   "rev": "2756f6603c992f133c1157bfc07ab11b5a7a6738",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.7.0
+leanprover/lean4:v4.8.0-rc1