From b0db05a208aca00352a3d3292a52c76f1f30df55 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Fri, 7 Jun 2024 08:41:49 -0400 Subject: [PATCH] chore: Update to Lean 4.9-rc1 --- .../AnomalyCancellation/PureU1/ConstAbs.lean | 4 ++-- .../PureU1/Even/BasisLinear.lean | 12 +++++----- .../PureU1/Odd/BasisLinear.lean | 10 ++++----- .../FlavorPhysics/CKMMatrix/PhaseFreedom.lean | 4 ++-- lake-manifest.json | 22 +++++++++---------- lean-toolchain | 2 +- 6 files changed, 27 insertions(+), 27 deletions(-) diff --git a/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean b/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean index c3cacd1..c62cb02 100644 --- a/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean +++ b/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean @@ -114,12 +114,12 @@ lemma boundary_split (k : Fin n) : k.succ.val + (n.succ - k.succ.val) = n.succ lemma boundary_accGrav' (k : Fin n) : accGrav n.succ S = ∑ i : Fin (k.succ.val + (n.succ - k.succ.val)), S (Fin.cast (boundary_split k) i) := by simp [accGrav] - erw [Finset.sum_equiv (Fin.castIso (boundary_split k)).toEquiv] + erw [Finset.sum_equiv (Fin.castOrderIso (boundary_split k)).toEquiv] intro i simp only [Fin.val_succ, mem_univ, RelIso.coe_fn_toEquiv] intro i simp - rfl + lemma boundary_accGrav'' (k : Fin n) (hk : boundary S k) : accGrav n.succ S = (2 * ↑↑k + 1 - ↑n) * S (0 : Fin n.succ) := by diff --git a/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean b/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean index f8edd17..dca885b 100644 --- a/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean +++ b/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean @@ -71,9 +71,9 @@ lemma ext_δ (S T : Fin (2 * n.succ) → ℚ) (h1 : ∀ i, S (δ₁ i) = T (δ lemma sum_δ₁_δ₂ (S : Fin (2 * n.succ) → ℚ) : ∑ i, S i = ∑ i : Fin n.succ, ((S ∘ δ₁) i + (S ∘ δ₂) i) := by have h1 : ∑ i, S i = ∑ i : Fin (n.succ + n.succ), S (Fin.cast (split_equal n.succ) i) := by - rw [Finset.sum_equiv (Fin.castIso (split_equal n.succ)).symm.toEquiv] + rw [Finset.sum_equiv (Fin.castOrderIso (split_equal n.succ)).symm.toEquiv] intro i - simp only [mem_univ, Fin.symm_castIso, RelIso.coe_fn_toEquiv, Fin.castIso_apply] + simp only [mem_univ, Fin.symm_castOrderIso, RelIso.coe_fn_toEquiv] intro i simp rw [h1] @@ -83,9 +83,9 @@ lemma sum_δ₁_δ₂ (S : Fin (2 * n.succ) → ℚ) : lemma sum_δ₁_δ₂' (S : Fin (2 * n.succ) → ℚ) : ∑ i, S i = ∑ i : Fin n.succ, ((S ∘ δ₁) i + (S ∘ δ₂) i) := by have h1 : ∑ i, S i = ∑ i : Fin (n.succ + n.succ), S (Fin.cast (split_equal n.succ) i) := by - rw [Finset.sum_equiv (Fin.castIso (split_equal n.succ)).symm.toEquiv] + rw [Finset.sum_equiv (Fin.castOrderIso (split_equal n.succ)).symm.toEquiv] intro i - simp only [mem_univ, Fin.symm_castIso, RelIso.coe_fn_toEquiv, Fin.castIso_apply] + simp only [mem_univ, Fin.symm_castOrderIso, RelIso.coe_fn_toEquiv] intro i simp rw [h1] @@ -95,9 +95,9 @@ lemma sum_δ₁_δ₂' (S : Fin (2 * n.succ) → ℚ) : lemma sum_δ!₁_δ!₂ (S : Fin (2 * n.succ) → ℚ) : ∑ i, S i = S δ!₃ + S δ!₄ + ∑ i : Fin n, ((S ∘ δ!₁) i + (S ∘ δ!₂) i) := by have h1 : ∑ i, S i = ∑ i : Fin (1 + ((n + n) + 1)), S (Fin.cast (n_cond₂ n) i) := by - rw [Finset.sum_equiv (Fin.castIso (n_cond₂ n)).symm.toEquiv] + rw [Finset.sum_equiv (Fin.castOrderIso (n_cond₂ n)).symm.toEquiv] intro i - simp only [mem_univ, Fin.symm_castIso, RelIso.coe_fn_toEquiv, Fin.castIso_apply] + simp only [mem_univ, Fin.symm_castOrderIso, RelIso.coe_fn_toEquiv] intro i simp rw [h1] diff --git a/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean b/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean index 30c7570..a6a9834 100644 --- a/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean +++ b/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean @@ -75,7 +75,7 @@ def δa₄ (j : Fin n.succ) : Fin (2 * n.succ + 1) := Fin.cast (split_adda n) (Fin.natAdd ((1+n)+1) j) lemma δa₁_δ₁ : @δa₁ n = δ₁ 0 := by - rfl + exact Fin.rev_inj.mp rfl lemma δa₁_δ!₃ : @δa₁ n = δ!₃ := by rfl @@ -115,9 +115,9 @@ lemma δ₂_δ!₂ (j : Fin n) : δ₂ j = δ!₂ j := by lemma sum_δ (S : Fin (2 * n + 1) → ℚ) : ∑ i, S i = S δ₃ + ∑ i : Fin n, ((S ∘ δ₁) i + (S ∘ δ₂) i) := by have h1 : ∑ i, S i = ∑ i : Fin (n + 1 + n), S (Fin.cast (split_odd n) i) := by - rw [Finset.sum_equiv (Fin.castIso (split_odd n)).symm.toEquiv] + rw [Finset.sum_equiv (Fin.castOrderIso (split_odd n)).symm.toEquiv] intro i - simp only [mem_univ, Fin.symm_castIso, RelIso.coe_fn_toEquiv, Fin.castIso_apply] + simp only [mem_univ, Fin.symm_castOrderIso, RelIso.coe_fn_toEquiv] intro i simp rw [h1] @@ -131,9 +131,9 @@ lemma sum_δ (S : Fin (2 * n + 1) → ℚ) : lemma sum_δ! (S : Fin (2 * n + 1) → ℚ) : ∑ i, S i = S δ!₃ + ∑ i : Fin n, ((S ∘ δ!₁) i + (S ∘ δ!₂) i) := by have h1 : ∑ i, S i = ∑ i : Fin ((1+n)+n), S (Fin.cast (split_odd! n) i) := by - rw [Finset.sum_equiv (Fin.castIso (split_odd! n)).symm.toEquiv] + rw [Finset.sum_equiv (Fin.castOrderIso (split_odd! n)).symm.toEquiv] intro i - simp only [mem_univ, Fin.symm_castIso, RelIso.coe_fn_toEquiv, Fin.castIso_apply] + simp only [mem_univ, Fin.castOrderIso, RelIso.coe_fn_toEquiv] intro i simp rw [h1] diff --git a/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean b/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean index 30bd98b..035936b 100644 --- a/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean +++ b/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean @@ -235,7 +235,7 @@ lemma fstRowThdColRealCond_holds_up_to_equiv (V : CKMMatrix) : (- arg [V]ud ) (- arg [V]us) (τ - arg [V]ud - arg [V]us - arg [V]cb - arg [V]tb) - have hUV : ⟦U⟧ = ⟦V⟧ := by + have hUV : Quotient.mk CKMMatrixSetoid U = ⟦V⟧ := by simp only [Quotient.eq] symm exact phaseShiftApply.equiv _ _ _ _ _ _ _ @@ -268,7 +268,7 @@ lemma ubOnePhaseCond_hold_up_to_equiv_of_ub_one {V : CKMMatrix} (hb : ¬ ([V]ud let U : CKMMatrix := phaseShiftApply V 0 0 (- Real.pi + arg [V]cd + arg [V]cs + arg [V]ub) (Real.pi - arg [V]cd ) (- arg [V]cs) (- arg [V]ub ) use U - have hUV : ⟦U⟧ = ⟦V⟧ := by + have hUV : Quotient.mk CKMMatrixSetoid U= ⟦V⟧ := by simp only [Quotient.eq] symm exact phaseShiftApply.equiv _ _ _ _ _ _ _ diff --git a/lake-manifest.json b/lake-manifest.json index 3eb4e69..317bab9 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,31 +1,31 @@ -{"version": 7, +{"version": "1.0.0", "packagesDir": ".lake/packages", "packages": [{"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, - "rev": "14f258593e8c261d8834f13c6edc7b970c253ee8", + "rev": "af2dda22771c59db026c48ac0aabc73b72b7a4de", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "nightly-testing", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, - "rev": "53156671405fbbd5402ed17a79bd129b961bd8d6", + "rev": "44f57616b0d9b8f9e5606f2c58d01df54840eba7", "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "nightly-testing", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "rev": "f617e0673845925e612b62141ff54c4b7980dc63", + "rev": "f744aab6fc4e06553464e6ae66730a3b14b8e615", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "nightly-testing", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/ProofWidgets4", @@ -49,7 +49,7 @@ {"url": "https://github.com/leanprover-community/import-graph.git", "type": "git", "subDir": null, - "rev": "35e38eb320982cfd2fcc864e0e0467ca223c8cdb", + "rev": "7983e959f8f4a79313215720de3ef1eca2d6d474", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -58,7 +58,7 @@ {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "rev": "b1087dd1d2d0075153f5ecffd8848d43cf02c042", + "rev": "1df6b982d827c6f6e335f594f5db66e3624abaf2", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, @@ -76,7 +76,7 @@ {"url": "https://github.com/fgdorais/lean4-unicode-basic", "type": "git", "subDir": null, - "rev": "8b53cc65534bc2c6888c3d4c53a3439648213f74", + "rev": "effd8b8771cfd7ece69db99448168078e113c61f", "name": "UnicodeBasic", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -94,7 +94,7 @@ {"url": "https://github.com/leanprover/doc-gen4", "type": "git", "subDir": null, - "rev": "b91fea210b7b6b451f19c6344d1f82765b9607af", + "rev": "1cae40a2dd0dca57030385ff53d72c3aa7b27f2b", "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lean-toolchain b/lean-toolchain index d8a6d7e..0ba3faf 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.8.0-rc1 +leanprover/lean4:v4.9.0-rc1