From cee38b7be89483d90a9f2b043d1353a83068835b Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Fri, 12 Jul 2024 11:54:50 -0400 Subject: [PATCH] chore: Bump to v4.10.0-rc1 --- .../AnomalyCancellation/PureU1/ConstAbs.lean | 6 ++-- HepLean/SpaceTime/MinkowskiMetric.lean | 8 +++-- README.md | 2 +- lake-manifest.json | 34 ++++++++++++------- lakefile.toml | 4 +-- lean-toolchain | 2 +- 6 files changed, 34 insertions(+), 22 deletions(-) diff --git a/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean b/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean index 1d3ea4a..d440305 100644 --- a/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean +++ b/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean @@ -225,7 +225,6 @@ lemma AFL_even_below (A : (PureU1 (2 * n.succ)).LinSols) (h : ConstAbsSorted A.v = A.val (0 : Fin (2*n.succ)) := by by_cases hA : A.val (0 : Fin (2*n.succ)) = 0 rw [is_zero h hA] - simp rfl exact AFL_even_below' h hA i @@ -244,10 +243,9 @@ lemma AFL_even_above' {A : (PureU1 (2 * n.succ)).LinSols} (h : ConstAbsSorted A. lemma AFL_even_above (A : (PureU1 (2 * n.succ)).LinSols) (h : ConstAbsSorted A.val) (i : Fin n.succ) : A.val (Fin.cast (split_equal n.succ) (Fin.natAdd n.succ i)) = - - A.val (0 : Fin (2*n.succ)) := by - by_cases hA : A.val (0 : Fin (2*n.succ)) = 0 + - A.val (0 : Fin (2 * n.succ)) := by + by_cases hA : A.val (0 : Fin (2 * n.succ)) = 0 rw [is_zero h hA] - simp rfl exact AFL_even_above' h hA i diff --git a/HepLean/SpaceTime/MinkowskiMetric.lean b/HepLean/SpaceTime/MinkowskiMetric.lean index d29c21d..c04e0d3 100644 --- a/HepLean/SpaceTime/MinkowskiMetric.lean +++ b/HepLean/SpaceTime/MinkowskiMetric.lean @@ -41,13 +41,17 @@ lemma sq : @minkowskiMatrix d * minkowskiMatrix = 1 := by rcases i with i | i <;> rcases j with j | j · simp only [diagonal, of_apply, Sum.inl.injEq, Sum.elim_inl, mul_one] split - · simp_all only [one_apply_eq] + · rename_i h + subst h + simp_all only [one_apply_eq] · simp_all only [ne_eq, Sum.inl.injEq, not_false_eq_true, one_apply_ne] · simp only [ne_eq, not_false_eq_true, diagonal_apply_ne, one_apply_ne] · simp only [ne_eq, not_false_eq_true, diagonal_apply_ne, one_apply_ne] · simp only [diagonal, of_apply, Sum.inr.injEq, Sum.elim_inr, mul_neg, mul_one, neg_neg] split - · simp_all only [one_apply_eq] + · rename_i h + subst h + simp_all only [one_apply_eq] · simp_all only [ne_eq, Sum.inr.injEq, not_false_eq_true, one_apply_ne] @[simp] diff --git a/README.md b/README.md index 9225176..7ef0097 100644 --- a/README.md +++ b/README.md @@ -4,7 +4,7 @@ [![](https://img.shields.io/badge/PRs-Welcome-green)](https://github.com/HEPLean/HepLean/pulls) [![](https://img.shields.io/badge/Lean-Zulip-green)](https://leanprover.zulipchat.com) [![](https://img.shields.io/badge/TODO-List-green)](https://heplean.github.io/HepLean/TODOList) -[![](https://img.shields.io/badge/Lean-v4.9.0-blue)](https://github.com/leanprover/lean4/releases/tag/v4.9.0) +[![](https://img.shields.io/badge/Lean-v4.10.0--rc1-blue)](https://github.com/leanprover/lean4/releases/tag/v4.10.0-rc1) A project to digitalize high energy physics. diff --git a/lake-manifest.json b/lake-manifest.json index b6dca83..b682f84 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,10 +1,11 @@ -{"version": "1.0.0", +{"version": "1.1.0", "packagesDir": ".lake/packages", "packages": [{"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, - "rev": "54bb04c3119f24fde14b9068c4b2e69db52a1450", + "scope": "leanprover-community", + "rev": "2ead90d24b4fac3a05c9c4294daa39bd8686fb98", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -13,6 +14,7 @@ {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, + "scope": "leanprover-community", "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6", "name": "Qq", "manifestFile": "lake-manifest.json", @@ -22,7 +24,8 @@ {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "rev": "06cca4bd36b2af743d4858c5cc31604aa9da26bc", + "scope": "leanprover-community", + "rev": "a64fe24aa94e21404940e9217363a9a1ed9a33a6", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -31,25 +34,28 @@ {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, - "rev": "87c1e7a427d8e21b6eaf8401f12897f52e2c3be9", + "scope": "leanprover-community", + "rev": "d1b33202c3a29a079f292de65ea438648123b635", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.38", + "inputRev": "v0.0.39", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, + "scope": "", "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/import-graph.git", + {"url": "https://github.com/leanprover-community/import-graph", "type": "git", "subDir": null, - "rev": "c29c3cdce415240e9dcec5c583ad5d36f83f9c71", + "scope": "leanprover-community", + "rev": "d366a602cc4a325a6f9db3a3991dfa6d6cf409c5", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -58,15 +64,17 @@ {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "rev": "f0957a7575317490107578ebaee9efaf8e62a4ab", + "scope": "", + "rev": "f5c3f06aa7f6d6c221786d2890c345a00e6341f8", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.9.0", + "inputRev": "v4.10.0-rc1", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/acmepjz/md4lean", "type": "git", "subDir": null, + "scope": "", "rev": "9148a0a7506099963925cf239c491fcda5ed0044", "name": "MD4Lean", "manifestFile": "lake-manifest.json", @@ -76,7 +84,8 @@ {"url": "https://github.com/fgdorais/lean4-unicode-basic", "type": "git", "subDir": null, - "rev": "87791b59c53be80a9a000eb2bcbf61f60a27b334", + "scope": "", + "rev": "c74a052aebee847780e165611099854de050adf7", "name": "UnicodeBasic", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,10 +94,11 @@ {"url": "https://github.com/leanprover/doc-gen4", "type": "git", "subDir": null, - "rev": "1daa0de7eea6bf8d3e1b0814156ede21a8a9e9e9", + "scope": "", + "rev": "c369436d21c583a60da62d4513c7b9ea08389074", "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", - "inputRev": "v4.9.0", + "inputRev": "v4.10.0-rc1", "inherited": false, "configFile": "lakefile.lean"}], "name": "hep_lean", diff --git a/lakefile.toml b/lakefile.toml index a035d1f..b2e4dd5 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -6,12 +6,12 @@ defaultTargets = ["HepLean"] [[require]] name = "mathlib" git = "https://github.com/leanprover-community/mathlib4.git" -rev = "v4.9.0" +rev = "v4.10.0-rc1" [[require]] name = "«doc-gen4»" git = "https://github.com/leanprover/doc-gen4" -rev = "v4.9.0" +rev = "v4.10.0-rc1" [[lean_lib]] name = "HepLean" diff --git a/lean-toolchain b/lean-toolchain index 4ef27c4..d69d1ed 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.9.0 +leanprover/lean4:v4.10.0-rc1