diff --git a/.lake/lakefile.olean b/.lake/lakefile.olean
deleted file mode 100644
index ceaa1e7..0000000
Binary files a/.lake/lakefile.olean and /dev/null differ
diff --git a/.lake/lakefile.olean.lock b/.lake/lakefile.olean.lock
deleted file mode 100644
index e69de29..0000000
diff --git a/.lake/lakefile.olean.trace b/.lake/lakefile.olean.trace
deleted file mode 100644
index bfb3860..0000000
--- a/.lake/lakefile.olean.trace
+++ /dev/null
@@ -1,4 +0,0 @@
-{"platform": "aarch64-apple-darwin",
- "options": {"env": "dev"},
- "leanHash": "dcccfb73cb247e9478220375ab7de03f7c67e505",
- "configHash": "17439028364340488343"}
diff --git a/HepLean/AnomalyCancellation/MSSMNu/Basic.lean b/HepLean/AnomalyCancellation/MSSMNu/Basic.lean
index 8b5d687..cbf418d 100644
--- a/HepLean/AnomalyCancellation/MSSMNu/Basic.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/Basic.lean
@@ -538,7 +538,6 @@ def dot  : BiLinearSymm MSSMCharges.Charges := BiLinearSymm.mk₂
     intro S1 S2 T
     simp only [MSSMSpecies_numberCharges, toSMSpecies_apply, Fin.isValue,
       ACCSystemCharges.chargesAddCommMonoid_add, map_add, Hd_apply, Fin.reduceFinMk, Hu_apply]
-    repeat erw [AddHom.map_add]
     rw [Fin.sum_univ_three, Fin.sum_univ_three, Fin.sum_univ_three]
     simp only [Fin.isValue]
     ring)
diff --git a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean
index 4ac3197..a871c11 100644
--- a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean
@@ -152,7 +152,6 @@ lemma lineQuad_smul (R : MSSMACC.AnomalyFreePerp) (a b c d : ℚ) :
   change _ = (d • planeY₃B₃ R _ _ _).val
   rw [← planeY₃B₃_smul]
   rw [lineQuad_val]
-  congr 2
   ring_nf
 
 /-- A helper function to simplify following expressions. -/
@@ -193,7 +192,6 @@ lemma lineCube_smul (R : MSSMACC.AnomalyFreePerp) (a b c d : ℚ) :
   change _ = (d • planeY₃B₃ R _ _ _).val
   rw [← planeY₃B₃_smul]
   change (planeY₃B₃ R _ _ _).val = (planeY₃B₃ R _ _ _).val
-  congr 2
   ring_nf
 
 lemma lineCube_cube (R : MSSMACC.AnomalyFreePerp) (a₁ a₂ a₃ : ℚ) :
@@ -210,7 +208,6 @@ lemma lineCube_quad (R : MSSMACC.AnomalyFreePerp) (a₁ a₂ a₃ : ℚ) :
   rw [α₁, α₂, α₃]
   ring
 
-
 section proj
 
 lemma α₃_proj  (T : MSSMACC.Sols) : α₃ (proj T.1.1) =
diff --git a/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean b/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
index f708255..43ddbd0 100644
--- a/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
+++ b/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
@@ -121,13 +121,11 @@ def bijection : linearParameters ≃ (SMNoGrav 1).LinSols where
   left_inv S := by
     apply linearParameters.ext
     rfl
-    repeat erw [speciesVal]
     simp only [Fin.isValue]
     repeat erw [speciesVal]
     simp only [asCharges, neg_add_rev]
     ring
     simp only [toSpecies_apply]
-    repeat erw [speciesVal]
     rfl
   right_inv S := by
     simp only [Fin.isValue, toSpecies_apply]
@@ -257,7 +255,6 @@ def bijectionLinearParameters :
     field_simp
     ring_nf
     field_simp [hQ, hE]
-    ring_nf
     field_simp
     ring_nf
     field_simp [hQ, hE]
diff --git a/HepLean/SpaceTime/MinkowskiMetric.lean b/HepLean/SpaceTime/MinkowskiMetric.lean
index aba0497..884945e 100644
--- a/HepLean/SpaceTime/MinkowskiMetric.lean
+++ b/HepLean/SpaceTime/MinkowskiMetric.lean
@@ -63,7 +63,6 @@ lemma det_eq_neg_one_pow_d : (@minkowskiMatrix d).det = (- 1) ^ d := by
 lemma as_block :  @minkowskiMatrix d =  (
     Matrix.fromBlocks (1 : Matrix (Fin 1) (Fin 1) ℝ) 0 0 (-1 : Matrix (Fin d) (Fin d) ℝ)) := by
   rw [minkowskiMatrix]
-  congr
   simp [LieAlgebra.Orthogonal.indefiniteDiagonal]
   rw [← fromBlocks_diagonal]
   refine fromBlocks_inj.mpr ?_
diff --git a/README.md b/README.md
index e0fbd2c..f2e2ca1 100644
--- a/README.md
+++ b/README.md
@@ -3,7 +3,7 @@
 [![](https://img.shields.io/badge/Read_The-Docs-green)](https://heplean.github.io/HepLean/)
 [![](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/Lean-v4.9.0--rc3-blue)](https://github.com/leanprover/lean4/releases/tag/v4.9.0-rc3)
+[![](https://img.shields.io/badge/Lean-v4.9.0-blue)](https://github.com/leanprover/lean4/releases/tag/v4.9.0)
 
 A project to digitalize high energy physics.
 
diff --git a/lake-manifest.json b/lake-manifest.json
index 2e0a53e..b6dca83 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "47e4cc5c5800c07d9bf232173c9941fa5bf68589",
+   "rev": "54bb04c3119f24fde14b9068c4b2e69db52a1450",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "882561b77bd2aaa98bd8665a56821062bdb3034c",
+   "rev": "06cca4bd36b2af743d4858c5cc31604aa9da26bc",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -31,10 +31,10 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5",
+   "rev": "87c1e7a427d8e21b6eaf8401f12897f52e2c3be9",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.36",
+   "inputRev": "v0.0.38",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
@@ -49,7 +49,7 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "1588be870b9c76fe62286e8f42f0b4dafa154c96",
+   "rev": "c29c3cdce415240e9dcec5c583ad5d36f83f9c71",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,10 +58,10 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "cd7c51790cac1a32c321373d45700290b3e8496c",
+   "rev": "f0957a7575317490107578ebaee9efaf8e62a4ab",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": null,
+   "inputRev": "v4.9.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/acmepjz/md4lean",
@@ -85,10 +85,10 @@
   {"url": "https://github.com/leanprover/doc-gen4",
    "type": "git",
    "subDir": null,
-   "rev": "1f51169609a3a7c448558c3d3eb353fb355c7025",
+   "rev": "1daa0de7eea6bf8d3e1b0814156ede21a8a9e9e9",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.9.0",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "hep_lean",
diff --git a/lakefile.toml b/lakefile.toml
index b29acd2..f873798 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -6,11 +6,12 @@ defaultTargets = ["HepLean"]
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4.git"
+rev = "v4.9.0"
 
 [[require]]
 name = "«doc-gen4»"
 git = "https://github.com/leanprover/doc-gen4"
-rev = "main"
+rev = "v4.9.0"
 
 [[lean_lib]]
 name = "HepLean"
diff --git a/lean-toolchain b/lean-toolchain
index e5ea660..4ef27c4 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.9.0-rc3
+leanprover/lean4:v4.9.0