diff --git a/HepLean/AnomalyCancellation/Basic.lean b/HepLean/AnomalyCancellation/Basic.lean
index b5f6d14..e88bbfc 100644
--- a/HepLean/AnomalyCancellation/Basic.lean
+++ b/HepLean/AnomalyCancellation/Basic.lean
@@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.Mathematics.LinearMaps
 import Mathlib.Algebra.Module.Basic
-import Mathlib.LinearAlgebra.FiniteDimensional
+import Mathlib.LinearAlgebra.FiniteDimensional.Defs
 /-!
 # Basic set up for anomaly cancellation conditions
 
@@ -96,7 +96,7 @@ instance linSolsAddCommMonoid (χ : ACCSystemLinear) :
   zero := ⟨χ.chargesAddCommMonoid.zero, fun _ ↦ (χ.linearACCs _).map_zero⟩
   zero_add S := LinSols.ext (χ.chargesAddCommMonoid.zero_add _)
   add_zero S := LinSols.ext (χ.chargesAddCommMonoid.add_zero _)
-  nsmul n S := ⟨n • S.val, fun _ ↦ by simp [nsmul_eq_smul_cast ℚ, (χ.linearACCs _).map_smul,
+  nsmul n S := ⟨n • S.val, fun _ ↦ by simp [Nat.cast_smul_eq_nsmul ℚ, (χ.linearACCs _).map_smul,
     S.linearSol _]⟩
   nsmul_zero n := rfl
   nsmul_succ n S := LinSols.ext (χ.chargesAddCommMonoid.nsmul_succ _ _)
diff --git a/HepLean/AnomalyCancellation/PureU1/Basic.lean b/HepLean/AnomalyCancellation/PureU1/Basic.lean
index e5a459b..3da6962 100644
--- a/HepLean/AnomalyCancellation/PureU1/Basic.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.AnomalyCancellation.Basic
-import Mathlib.Algebra.Module.Equiv
+import Mathlib.Algebra.Module.Equiv.Basic
 import Mathlib.Algebra.BigOperators.Ring
 import Mathlib.Algebra.BigOperators.Fin
 /-!
diff --git a/HepLean/FeynmanDiagrams/Basic.lean b/HepLean/FeynmanDiagrams/Basic.lean
index 6695f91..48c62b1 100644
--- a/HepLean/FeynmanDiagrams/Basic.lean
+++ b/HepLean/FeynmanDiagrams/Basic.lean
@@ -14,7 +14,7 @@ import Mathlib.CategoryTheory.Limits.Shapes.Terminal
 import Mathlib.Data.Fintype.Prod
 import Mathlib.Data.Fintype.Perm
 import Mathlib.Combinatorics.SimpleGraph.Basic
-import Mathlib.Combinatorics.SimpleGraph.Connectivity
+import Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkCounting
 import Mathlib.SetTheory.Cardinal.Basic
 /-!
 # Feynman diagrams
diff --git a/HepLean/FlavorPhysics/CKMMatrix/Relations.lean b/HepLean/FlavorPhysics/CKMMatrix/Relations.lean
index 073875a..de38ddb 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/Relations.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/Relations.lean
@@ -189,7 +189,6 @@ lemma conj_Vtb_cross_product {V : CKMMatrix} {τ : ℝ}
   simp only [← exp_conj, _root_.map_mul, conj_ofReal, conj_I, mul_neg, Fin.isValue, neg_mul]
   field_simp
   ring_nf
-  simp
 
 end crossProduct
 
@@ -199,8 +198,6 @@ lemma conj_Vtb_mul_Vud {V : CKMMatrix} {τ : ℝ}
     [V]cs * (normSq [V]ud + normSq [V]us) + [V]cb * conj [V]ub * [V]us := by
   rw [conj_Vtb_cross_product hτ]
   simp [exp_neg]
-  have h1 := exp_ne_zero (τ * I)
-  field_simp
   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
@@ -215,8 +212,6 @@ lemma conj_Vtb_mul_Vus {V : CKMMatrix} {τ : ℝ}
     - ([V]cd * (normSq [V]ud + normSq [V]us) + [V]cb * conj ([V]ub) * [V]ud) := by
   rw [conj_Vtb_cross_product hτ]
   simp [exp_neg]
-  have h1 := exp_ne_zero (τ * I)
-  field_simp
   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
diff --git a/HepLean/FlavorPhysics/CKMMatrix/Rows.lean b/HepLean/FlavorPhysics/CKMMatrix/Rows.lean
index 16dcec0..5bf92c6 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/Rows.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/Rows.lean
@@ -6,6 +6,7 @@ Authors: Joseph Tooby-Smith
 import HepLean.FlavorPhysics.CKMMatrix.Basic
 import Mathlib.Analysis.SpecialFunctions.Complex.Arg
 import Mathlib.LinearAlgebra.CrossProduct
+import Mathlib.LinearAlgebra.FiniteDimensional
 /-!
 # Rows for the CKM Matrix
 
diff --git a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean
index 77f1d0d..7785c21 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean
@@ -359,8 +359,7 @@ lemma mulExpδ₁₃_on_param_eq_zero_iff (V : CKMMatrix) (δ₁₃ : ℝ) :
   rw [mulExpδ₁₃_on_param_δ₁₃]
   simp only [mul_eq_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, pow_eq_zero_iff,
     ofReal_zero]
-  have h1 := exp_ne_zero (I * δ₁₃)
-  simp_all
+  simp only [exp_ne_zero, or_false]
   aesop
 
 lemma mulExpδ₁₃_on_param_abs (V : CKMMatrix) (δ₁₃ : ℝ) :
diff --git a/HepLean/SpaceTime/Basic.lean b/HepLean/SpaceTime/Basic.lean
index 621d27b..ad87c17 100644
--- a/HepLean/SpaceTime/Basic.lean
+++ b/HepLean/SpaceTime/Basic.lean
@@ -6,7 +6,6 @@ Authors: Joseph Tooby-Smith
 import Mathlib.Data.Complex.Exponential
 import Mathlib.Geometry.Manifold.SmoothManifoldWithCorners
 import Mathlib.Analysis.InnerProductSpace.PiL2
-import Mathlib.LinearAlgebra.Matrix.DotProduct
 /-!
 # Space time
 
diff --git a/README.md b/README.md
index 8a499e0..f2de335 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.10.0--rc2-blue)](https://github.com/leanprover/lean4/releases/tag/v4.10.0-rc2)
+[![](https://img.shields.io/badge/Lean-v4.10.0-blue)](https://github.com/leanprover/lean4/releases/tag/v4.10.0)
 
 A project to digitalize high energy physics.
 
diff --git a/lake-manifest.json b/lake-manifest.json
index 837bdcd..115db29 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c0efc1fd2a0bec51bd55c5b17348af13d7419239",
+   "rev": "0f3e143dffdc3a591662f3401ce1d7a3405227c0",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6",
+   "rev": "01ad33937acd996ee99eb74eefb39845e4e4b9f5",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "deb5bd446a108da8aa8c1a1b62dd50722b961b73",
+   "rev": "209712c78b16c795453b6da7f7adbda4589a8f21",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,27 +35,27 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d1b33202c3a29a079f292de65ea438648123b635",
+   "rev": "c87908619cccadda23f71262e6898b9893bffa36",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.39",
+   "inputRev": "v0.0.40",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
+   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "68b518c9b352fbee16e6d632adcb7a6d0760e2b7",
+   "rev": "543725b3bfed792097fc134adca628406f6145f5",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,17 +65,17 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "984c68d7773ac133c74543b99b82c33e53baea6b",
+   "rev": "a719ba5c3115d47b68bf0497a9dd1bcbb21ea663",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.10.0-rc2",
+   "inputRev": "v4.10.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/acmepjz/md4lean",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "9148a0a7506099963925cf239c491fcda5ed0044",
+   "rev": "5e95f4776be5e048364f325c7e9d619bb56fb005",
    "name": "MD4Lean",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,20 +85,30 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "c74a052aebee847780e165611099854de050adf7",
+   "rev": "5c11428272fe190b7e726ebe448f93437d057b74",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
+  {"url": "https://github.com/dupuisf/BibtexQuery",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "bd8747df9ee72fca365efa5bd3bd0d8dcd083b9f",
+   "name": "BibtexQuery",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/doc-gen4",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "c369436d21c583a60da62d4513c7b9ea08389074",
+   "rev": "593ac5bd2ca98c5294675b5cccf3d89b300a76eb",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.10.0-rc1",
+   "inputRev": "v4.10.0",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "hep_lean",
diff --git a/lakefile.toml b/lakefile.toml
index 275ff94..d75251e 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.10.0-rc2"
+rev = "v4.10.0"
 
 [[require]]
 name = "«doc-gen4»"
 git = "https://github.com/leanprover/doc-gen4"
-rev = "v4.10.0-rc1"
+rev = "v4.10.0"
 
 [[lean_lib]]
 name = "HepLean"
diff --git a/lean-toolchain b/lean-toolchain
index 6a4259f..7f0ea50 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.10.0-rc2
+leanprover/lean4:v4.10.0