diff --git a/PhysLean/ClassicalMechanics/HarmonicOscillator/Basic.lean b/PhysLean/ClassicalMechanics/HarmonicOscillator/Basic.lean
index 19275675..5d7b4a39 100644
--- a/PhysLean/ClassicalMechanics/HarmonicOscillator/Basic.lean
+++ b/PhysLean/ClassicalMechanics/HarmonicOscillator/Basic.lean
@@ -110,7 +110,6 @@ structure HarmonicOscillator where
 
 namespace HarmonicOscillator
 
-
 variable (S : HarmonicOscillator)
 
 @[simp]
diff --git a/PhysLean/ClassicalMechanics/HarmonicOscillator/ConfigurationSpace.lean b/PhysLean/ClassicalMechanics/HarmonicOscillator/ConfigurationSpace.lean
index e6b1a68b..4ae1e08d 100644
--- a/PhysLean/ClassicalMechanics/HarmonicOscillator/ConfigurationSpace.lean
+++ b/PhysLean/ClassicalMechanics/HarmonicOscillator/ConfigurationSpace.lean
@@ -3,10 +3,7 @@ Copyright (c) 2026 Nicola Bernini. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Nicola Bernini
 -/
-import Mathlib.Analysis.InnerProductSpace.Basic
 import Mathlib.Geometry.Manifold.Diffeomorph
-import Mathlib.LinearAlgebra.FiniteDimensional.Basic
-import PhysLean.SpaceAndTime.Space.Basic
 import PhysLean.SpaceAndTime.Time.Basic
 /-!
 # Configuration space of the harmonic oscillator
diff --git a/PhysLean/Mathematics/Geometry/Metric/PseudoRiemannian/Defs.lean b/PhysLean/Mathematics/Geometry/Metric/PseudoRiemannian/Defs.lean
index 8f36ce5f..c5a120a0 100644
--- a/PhysLean/Mathematics/Geometry/Metric/PseudoRiemannian/Defs.lean
+++ b/PhysLean/Mathematics/Geometry/Metric/PseudoRiemannian/Defs.lean
@@ -309,7 +309,14 @@ lemma toBilinForm_isSymm (g : PseudoRiemannianMetric E H M n I) (x : M) :
 @[simp]
 lemma toBilinForm_nondegenerate (g : PseudoRiemannianMetric E H M n I) (x : M) :
     (toBilinForm g x).Nondegenerate := by
-  intro v hv; simp_rw [toBilinForm_apply] at hv; exact g.nondegenerate x v hv
+  unfold LinearMap.BilinForm.Nondegenerate LinearMap.Nondegenerate
+    LinearMap.SeparatingLeft LinearMap.SeparatingRight
+  constructor
+  · intro v hv; simp_rw [toBilinForm_apply] at hv; exact g.nondegenerate x v hv
+  · intro v hv; simp_rw [toBilinForm_apply] at hv;
+    have hw : ∀ (w : TangentSpace I x), ((g.val x) v) w = 0 := by
+      intro w; rw [symm]; simp [hv]
+    exact g.nondegenerate x v hw
 
 /-- The inner product (or scalar product) on the tangent space at point `x`
   induced by the pseudo-Riemannian metric `g`. This is `gₓ(v, w)`. -/
@@ -608,10 +615,19 @@ lemma cotangentMetricVal_nondegenerate (g : PseudoRiemannianMetric E H M n I) (x
 @[simp]
 lemma cotangentToBilinForm_nondegenerate (g : PseudoRiemannianMetric E H M n I) (x : M) :
     (cotangentToBilinForm g x).Nondegenerate := by
-  intro ω hω
-  apply cotangentMetricVal_nondegenerate g x ω
-  intro v
-  exact hω v
+  unfold LinearMap.BilinForm.Nondegenerate LinearMap.Nondegenerate
+    LinearMap.SeparatingLeft LinearMap.SeparatingRight
+  constructor
+  · intro ω hω
+    apply cotangentMetricVal_nondegenerate g x ω
+    intro v
+    exact hω v
+  · intro ω hω
+    apply cotangentMetricVal_nondegenerate g x ω
+    intro v
+    have hv : ∀ (y : TangentSpace I x →L[ℝ] ℝ), ((g.cotangentToBilinForm x) ω) y = 0 := by
+      intro y; rw [LinearMap.BilinForm.isSymm_def.mp (cotangentToBilinForm_isSymm g x)]; simp [hω]
+    exact hv v
 
 end Cotangent
 
diff --git a/PhysLean/Meta/Basic.lean b/PhysLean/Meta/Basic.lean
index 8b32180b..00964ea5 100644
--- a/PhysLean/Meta/Basic.lean
+++ b/PhysLean/Meta/Basic.lean
@@ -4,8 +4,7 @@ Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
 import Mathlib.Lean.Expr.Basic
-import Lean.Elab.PreDefinition.Structural.BRecOn
-import ImportGraph.RequiredModules
+import ImportGraph.Imports.RequiredModules
 /-!
 
 ## Basic Lean meta programming commands
diff --git a/PhysLean/Particles/BeyondTheStandardModel/TwoHDM/Potential.lean b/PhysLean/Particles/BeyondTheStandardModel/TwoHDM/Potential.lean
index 11b2090a..edb9fa7e 100644
--- a/PhysLean/Particles/BeyondTheStandardModel/TwoHDM/Potential.lean
+++ b/PhysLean/Particles/BeyondTheStandardModel/TwoHDM/Potential.lean
@@ -216,7 +216,7 @@ def stabilityCounterExample : PotentialParameters := {(0 : PotentialParameters)
     𝓵₆ := -2
     𝓵₇ := -2}
 
-lemma stabilityCounterExample_ξ  :
+lemma stabilityCounterExample_ξ :
     stabilityCounterExample.ξ = fun
       | Sum.inl 0 => 0
       | Sum.inr 0 => 0
diff --git a/PhysLean/QuantumMechanics/OneDimension/Operators/Parity.lean b/PhysLean/QuantumMechanics/OneDimension/Operators/Parity.lean
index 072ba6d4..75234b10 100644
--- a/PhysLean/QuantumMechanics/OneDimension/Operators/Parity.lean
+++ b/PhysLean/QuantumMechanics/OneDimension/Operators/Parity.lean
@@ -58,11 +58,11 @@ def parityOperatorSchwartz : 𝓢(ℝ, ℂ) →L[ℂ] 𝓢(ℝ, ℂ) := by
     | 0 => simp
     | 1 =>
       rw [iteratedFDeriv_succ_eq_comp_right]
-      simp
+      simp [ContinuousLinearMap.norm_id]
     | .succ (.succ n) =>
       rw [iteratedFDeriv_succ_eq_comp_right]
-      simp only [Nat.succ_eq_add_one, fderiv_id', Function.comp_apply, LinearIsometryEquiv.norm_map,
-        ge_iff_le]
+      simp only [Nat.succ_eq_add_one, fderiv_id', Function.comp_apply,
+        LinearIsometryEquiv.norm_map, ge_iff_le]
       rw [iteratedFDeriv_const_of_ne]
       simp only [Pi.zero_apply, norm_zero]
       apply add_nonneg
diff --git a/PhysLean/Relativity/Tensors/ComplexTensor/OfRat.lean b/PhysLean/Relativity/Tensors/ComplexTensor/OfRat.lean
index d9d49c2f..34f7da5a 100644
--- a/PhysLean/Relativity/Tensors/ComplexTensor/OfRat.lean
+++ b/PhysLean/Relativity/Tensors/ComplexTensor/OfRat.lean
@@ -38,12 +38,10 @@ noncomputable def ofRat {n : ℕ} {c : Fin n → complexLorentzTensor.Color} :
     apply (Tensor.basis _).repr.injective
     ext b
     simp
-    rfl
   map_smul' r f := by
     apply (Tensor.basis _).repr.injective
     ext b
     simp
-    rfl
 
 @[simp]
 lemma ofRat_basis_repr_apply {n : ℕ} {c : Fin n → complexLorentzTensor.Color}
@@ -51,7 +49,6 @@ lemma ofRat_basis_repr_apply {n : ℕ} {c : Fin n → complexLorentzTensor.Color
     (b :(ComponentIdx c)) :
   (Tensor.basis c).repr (ofRat f) b = toComplexNum (f b) := by
   simp [ofRat]
-  rfl
 
 lemma basis_eq_ofRat {n : ℕ} {c : Fin n → complexLorentzTensor.Color}
     (b : (ComponentIdx c)) :
diff --git a/PhysLean/Relativity/Tensors/RealTensor/ToComplex.lean b/PhysLean/Relativity/Tensors/RealTensor/ToComplex.lean
index a1f1ba53..5cd280b2 100644
--- a/PhysLean/Relativity/Tensors/RealTensor/ToComplex.lean
+++ b/PhysLean/Relativity/Tensors/RealTensor/ToComplex.lean
@@ -5,7 +5,6 @@ Authors: Joseph Tooby-Smith
 -/
 import PhysLean.Meta.Linters.Sorry
 import PhysLean.Relativity.Tensors.ComplexTensor.Basic
-import PhysLean.Relativity.Tensors.Evaluation
 /-!
 
 # Complex Lorentz tensors from real Lorentz tensors
diff --git a/PhysLean/SpaceAndTime/Space/Norm.lean b/PhysLean/SpaceAndTime/Space/Norm.lean
index 55a37f6a..1fcbc477 100644
--- a/PhysLean/SpaceAndTime/Space/Norm.lean
+++ b/PhysLean/SpaceAndTime/Space/Norm.lean
@@ -1057,7 +1057,8 @@ lemma distDiv_inv_pow_eq_dim {d : ℕ} :
             | 1 =>
               use 0, 1
               intro x
-              simp [fderiv_smul_const, iteratedFDeriv_succ_eq_comp_right]
+              simp [fderiv_smul_const, iteratedFDeriv_succ_eq_comp_right,
+                ContinuousLinearMap.norm_id]
             | n' + 1 + 1 =>
               use 0, 0
               intro x
diff --git a/PhysLean/SpaceAndTime/Time/TimeTransMan.lean b/PhysLean/SpaceAndTime/Time/TimeTransMan.lean
index 50c9ce44..8847d7ed 100644
--- a/PhysLean/SpaceAndTime/Time/TimeTransMan.lean
+++ b/PhysLean/SpaceAndTime/Time/TimeTransMan.lean
@@ -336,7 +336,6 @@ lemma neg_eq_negMetric (zero : TimeTransMan) (x : TimeUnit) (t : TimeTransMan) :
 ### The map from TimeTransMan to Time
 
 -/
-
 /-- With a choice of zero `zero : TimeTransMan` and a choice of units `x : TimeUnit`,
   `toTime` is the homeomorphism between the type `TimeTransMan` and `Time`. -/
 noncomputable def toTime (zero : TimeTransMan) (x : TimeUnit) : TimeTransMan ≃ₜ Time where
@@ -355,7 +354,13 @@ noncomputable def toTime (zero : TimeTransMan) (x : TimeUnit) : TimeTransMan ≃
       ext
       simp [valHomeomorphism, addTime_val]
     rw [h1]
-    fun_prop
+    · apply Continuous.add
+      · apply Continuous.fun_mul
+        · fun_prop
+        · apply Differentiable.continuous (𝕜 := ℝ)
+          fun_prop
+      · fun_prop
+
   continuous_toFun := by
     rw [← Homeomorph.comp_continuous_iff Time.toRealCLE.toHomeomorph]
     have h1 : (⇑Time.toRealCLE.toHomeomorph ∘ (fun t => ⟨diff x t zero⟩)) = fun t =>
diff --git a/README.md b/README.md
index 74931232..28e2cfcc 100644
--- a/README.md
+++ b/README.md
@@ -20,7 +20,7 @@
 [![](https://img.shields.io/badge/PhysLean-Online-purple)](https://live.physlean.com)
 
 [![](https://img.shields.io/badge/View_The-Stats-blue)](https://physlean.com/Stats)
-[![](https://img.shields.io/badge/Lean-v4.27.0-blue)](https://github.com/leanprover/lean4/releases/tag/v4.27.0)
+[![](https://img.shields.io/badge/Lean-v4.28.0-blue)](https://github.com/leanprover/lean4/releases/tag/v4.28.0)
 [![Gitpod Ready-to-Code](https://img.shields.io/badge/Gitpod-ready--to--code-blue?logo=gitpod)](https://gitpod.io/#https://github.com/HEPLean/HepLean)
 [![Ask DeepWiki](https://deepwiki.com/badge.svg)](https://deepwiki.com/HEPLean/PhysLean)
 [![api_docs](https://img.shields.io/badge/doc-API_docs-blue)](https://physlean.com/docs/)
diff --git a/lake-manifest.json b/lake-manifest.json
index 922193ad..60641765 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,27 +5,27 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "417747790f580618f991d0b30373a0e4d19868a2",
+   "rev": "a41d5ebebfa77afe737fec8de8ad03fc8b08fdff",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.27.0",
+   "inputRev": "v4.28.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a3a10db0e9d66acbebf76c5e6a135066525ac900",
+   "rev": "8f9d9cff6bd728b17a24e163c9402775d9e6a365",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.27.0",
+   "inputRev": "v4.28.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "28e0856d4424863a85b18f38868c5420c55f9bae",
+   "rev": "4f10f47646cb7d5748d6f423f4a07f98f7bbcc9e",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "8668e1ab7c987fb8ed1349f14c3b7b60bd5f27b6",
+   "rev": "ff04f5c424e50e23476d3539c7c0cc4956e971ad",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "1c5c543d2637aebf90c80aead2d401ae88db13cc",
+   "rev": "058ada3acad7dd0d55657476bf292c8e02a2f650",
    "name": "BibtexQuery",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "92a0bac89cf9f9f7cb813484506e3fb7f7350ad4",
+   "rev": "7e097e9a076d5fbe48aa39aceee871af0d011101",
    "name": "MD4Lean",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "009dc1e6f2feb2c96c081537d80a0905b2c6498f",
+   "rev": "55c8532eb21ec9f6d565d51d96b8ca50bd1fbef3",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28",
+   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8f497d55985a189cea8020d9dc51260af1e41ad2",
+   "rev": "85b59af46828c029a9168f2f9c35119bd0721e6e",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,17 +95,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c04225ee7c0585effbd933662b3151f01b600e40",
+   "rev": "be3b2e63b1bbf496c478cef98b86972a37c1417d",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.85",
+   "inputRev": "v0.0.87",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "cb837cc26236ada03c81837bebe0acd9c70ced7d",
+   "rev": "f642a64c76df8ba9cb53dba3b919425a0c2aeaf1",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -115,7 +115,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "bd58c9efe2086d56ca361807014141a860ddbf8c",
+   "rev": "b8f98e9087e02c8553945a2c5abf07cec8e798c3",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -125,7 +125,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b25b36a7caf8e237e7d1e6121543078a06777c8a",
+   "rev": "495c008c3e3f4fb4256ff5582ddb3abf3198026f",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/lakefile.toml b/lakefile.toml
index 2fff152b..173fd112 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -11,12 +11,12 @@ warn.sorry = false
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4.git"
-rev = "v4.27.0"
+rev = "v4.28.0"
 
 [[require]]
 name = "«doc-gen4»"
 git = "https://github.com/leanprover/doc-gen4"
-rev = "v4.27.0"
+rev = "v4.28.0"
 
 [[lean_lib]]
 name = "PhysLean"
diff --git a/lean-toolchain b/lean-toolchain
index 2bb276aa..ea6ca7ff 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.27.0
\ No newline at end of file
+leanprover/lean4:v4.28.0
\ No newline at end of file