diff --git a/SampCert/DifferentialPrivacy/Pure/Composition.lean b/SampCert/DifferentialPrivacy/Pure/Composition.lean
index 75148fea..6554b28d 100644
--- a/SampCert/DifferentialPrivacy/Pure/Composition.lean
+++ b/SampCert/DifferentialPrivacy/Pure/Composition.lean
@@ -63,7 +63,6 @@ theorem privCompose_DP_bound {nq1 : Mechanism T U} {nq2 : Mechanism T V} {ε₁
             simp_all
             simp [division_def] at h1a
             rw [ENNReal.mul_top Hz''] at h1a
-            skip
             simp_all
         · cases (Classical.em (nq2 l₁ y = 0))
           · rename_i Hz''
@@ -73,7 +72,6 @@ theorem privCompose_DP_bound {nq1 : Mechanism T U} {nq2 : Mechanism T V} {ε₁
             simp_all
             simp [division_def] at h2a
             rw [ENNReal.mul_top Hz''] at h2a
-            skip
             simp_all
       · have A : nq1 l₁ x * nq2 l₁ y / (nq1 l₂ x * nq2 l₂ y) = (nq1 l₁ x / nq1 l₂ x) * (nq2 l₁ y / nq2 l₂ y) := by
           rw [division_def]
diff --git a/SampCert/DifferentialPrivacy/RenyiDivergence.lean b/SampCert/DifferentialPrivacy/RenyiDivergence.lean
index 24eb5248..0a83339e 100644
--- a/SampCert/DifferentialPrivacy/RenyiDivergence.lean
+++ b/SampCert/DifferentialPrivacy/RenyiDivergence.lean
@@ -107,13 +107,8 @@ theorem RenyiDivergenceExpectation (p q : T → ENNReal) {α : ℝ} (h : 1 < α)
   ext x
   rw [AbsCts] at H
   generalize Hvq : q x = vq
-  cases vq <;> simp
-  · -- q x = ⊤
-    rw [ENNReal.zero_rpow_of_pos ?H]
-    case H => linarith
-    simp
-    right
-    apply h
+  cases vq <;> try simp_all
+  · linarith
   · rename_i vq'
     cases (Classical.em (vq' = 0))
     · -- q x = 0
@@ -128,7 +123,7 @@ theorem RenyiDivergenceExpectation (p q : T → ENNReal) {α : ℝ} (h : 1 < α)
     · -- q x ∈ ℝ+
       rename_i Hvq'
       generalize Hvp : p x = vp
-      cases vp <;> simp
+      cases vp
       · -- q x ∈ ℝ+, p x = ⊤
         rw [ENNReal.top_rpow_of_pos ?H]
         case H => linarith
@@ -142,10 +137,12 @@ theorem RenyiDivergenceExpectation (p q : T → ENNReal) {α : ℝ} (h : 1 < α)
           cases Hcont'
           · simp_all only [some_eq_coe, none_eq_top, zero_ne_top]
           · simp_all only [some_eq_coe, none_eq_top, top_rpow_of_neg, coe_ne_top, sub_neg, and_true]
-        · rw [top_mul']
-          split
-          · simp_all only [some_eq_coe, none_eq_top, zero_ne_top]
-          · rfl
+        · simp_all
+          rw [top_rpow_def]
+          split <;> try simp_all
+          split <;> try simp_all
+          · linarith
+          · linarith
       · rename_i vp
         cases (Classical.em (vq' = 0))
         · -- q x ∈ ℝ+, p x = 0
@@ -337,10 +334,10 @@ theorem Renyi_Jensen_strict_real (f : T → ℝ) (q : PMF T) (α : ℝ) (h : 1 <
       right
       simp at HR
       -- Because T is discrete, almost-everywhere equality should become equality
-      have HR' := @Filter.EventuallyEq.eventually _ _ (q.toMeasure.ae) f (Function.const T (⨍ (x : T), f x ∂q.toMeasure)) HR
+      have HR' := @Filter.EventuallyEq.eventually _ _ (ae q.toMeasure) f (Function.const T (⨍ (x : T), f x ∂q.toMeasure)) HR
       simp [Filter.Eventually] at HR'
       -- The measure of the compliment of the set in HR' is zero
-      simp [MeasureTheory.Measure.ae] at HR'
+      simp [ae] at HR'
       rw [PMF.toMeasure_apply _ _ ?Hmeas] at HR'
       case Hmeas =>
         apply (@measurableSet_discrete _ _ ?DM)
diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/Composition.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/Composition.lean
index fdba32e3..17d55f0c 100644
--- a/SampCert/DifferentialPrivacy/ZeroConcentrated/Composition.lean
+++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/Composition.lean
@@ -43,7 +43,6 @@ theorem privCompose_zCDPBound {nq1 : Mechanism T U} {nq2 : Mechanism T V} {ε₁
   rw [DFunLike.coe]
   rw [PMF.instFunLike]
   simp
-  repeat rw [SLang.toPMF]
   have CG1 (b : U) : (nq1 l₂).val b ≠ ⊤ := by
     have H := PMF.apply_ne_top (nq1 l₂) b
     simp [DFunLike.coe, PMF.instFunLike] at H
diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/ConcentratedBound.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/ConcentratedBound.lean
index 9d360b3c..93e17a72 100644
--- a/SampCert/DifferentialPrivacy/ZeroConcentrated/ConcentratedBound.lean
+++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/ConcentratedBound.lean
@@ -538,7 +538,6 @@ theorem Renyi_Gauss_divergence_bound' {σ α : ℝ} (h : σ ≠ 0) (h' : 1 < α)
     unfold RenyiDivergence
     unfold RenyiDivergence_def
     unfold RenyiDivergence'
-    congr
     simp
     unfold discrete_gaussian_pmf
 
@@ -658,7 +657,6 @@ theorem discrete_GaussianGenSample_ZeroConcentrated {α : ℝ} (h : 1 < α) (num
           simp
     rw [X]
     rw [ENNReal.ofReal_div_of_pos]
-    congr
     simp
 
 end SLang
diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/Mechanism/Properties.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/Mechanism/Properties.lean
index 642e981a..3b540197 100644
--- a/SampCert/DifferentialPrivacy/ZeroConcentrated/Mechanism/Properties.lean
+++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/Mechanism/Properties.lean
@@ -212,9 +212,8 @@ theorem privNoisedQuery_zCDP (query : List T → ℤ) (Δ ε₁ ε₂ : ℕ+) (b
   simp [zCDP]
   apply And.intro
   · exact privNoisedQuery_AC query Δ ε₁ ε₂
-  · repeat any_goals constructor
-    . apply privNoisedQuery_zCDPBound
-      exact bounded_sensitivity
+  · apply privNoisedQuery_zCDPBound
+    exact bounded_sensitivity
 
 
 end SLang
diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/Postprocessing.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/Postprocessing.lean
index 5485e5f3..96691991 100644
--- a/SampCert/DifferentialPrivacy/ZeroConcentrated/Postprocessing.lean
+++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/Postprocessing.lean
@@ -188,7 +188,7 @@ theorem privPostPocess_DP_pre_reduct {U : Type} [m2 : MeasurableSpace U] [count
 
   -- Eliminate elements with probability zero
   split
-  case h.inl =>
+  case h.isTrue =>
     rename_i H
     repeat rw [condition_to_subset]
     rw [H]
diff --git a/SampCert/Util/Log.lean b/SampCert/Util/Log.lean
index 34a3e03f..bbc38156 100644
--- a/SampCert/Util/Log.lean
+++ b/SampCert/Util/Log.lean
@@ -143,15 +143,8 @@ lemma EReal_isReal_cases (w : EReal) : w = ⊥ ∨ w = ⊤ ∨ (∃ v : ℝ, w =
   cases w
   · left
     rfl
-  rename_i w'
-  cases w'
-  · right
-    left
-    rfl
-  rename_i wR
-  right
-  right
-  exists wR
+  simp_all
+  tauto
 
 syntax "case_EReal_isReal" term : tactic
 macro_rules
@@ -427,31 +420,24 @@ lemma elog_eexp {x : ENNReal} : eexp (elog x) = x := by
         simp
         rw [Hk]
 
+
 @[simp]
 lemma eexp_elog {w : EReal} : (elog (eexp w)) = w := by
   cases w
   · simp [eexp, elog]
-    rfl
-  · simp [eexp, elog]
+  · simp only [eexp, elog]
     rename_i v'
-    cases v'
-    · simp
-      rfl
-    · simp
-      rename_i v''
-      simp [ENNReal.ofReal]
-      split
-      · rename_i Hcont
-        have Hcont' : 0 < rexp v'' := by exact exp_pos v''
+    simp [Real.toEReal, ENNReal.ofReal]
+    split
+    · rename_i Hcont
+      have Hcont' : 0 < rexp v' := by exact exp_pos v'
+      linarith
+    · rename_i H
+      have RW : (max (rexp v') 0) = (rexp v') := by
+        apply max_eq_left_iff.mpr
         linarith
-      · rename_i H
-        have RW : (max (rexp v'') 0) = (rexp v'') := by
-          apply max_eq_left_iff.mpr
-          linarith
-        simp [RW]
-        clear RW
-        simp [Real.toEReal]
-
+      simp [RW]
+  · simp [eexp, elog]
 
 lemma elog_ENNReal_ofReal_of_pos {x : ℝ} (H : 0 < x) : (ENNReal.ofReal x).elog = x.log.toEReal := by
   simp [ENNReal.ofReal, ENNReal.elog, ENNReal.toEReal]
@@ -501,27 +487,24 @@ lemma eexp_injective {w z : EReal} : eexp w = eexp z -> w = z := by
   intro H
   cases w <;> cases z <;> try tauto
   · rename_i v
-    cases v <;> simp at *
-    rename_i v'
-    have Hv' := exp_pos v'
+    simp [Real.toEReal] at H
+    exfalso
+    have Hv' := exp_pos v
     linarith
   · rename_i v
-    cases v <;> simp at *
-    rename_i v'
-    have Hv' := exp_pos v'
+    simp [Real.toEReal] at H
+    have Hv' := exp_pos v
     linarith
   · rename_i v₁ v₂
-    cases v₁ <;> cases v₂ <;> simp at *
     congr
-    rename_i v₁' v₂'
-    simp [ENNReal.ofReal] at H
+    simp [Real.toEReal, ENNReal.ofReal] at H
     apply NNReal.coe_inj.mpr at H
     simp at H
     have RW (r : ℝ) : (max (rexp r) 0) = (rexp r) := by
       apply max_eq_left_iff.mpr
       exact exp_nonneg r
-    rw [RW v₁'] at H
-    rw [RW v₂'] at H
+    rw [RW v₁] at H
+    rw [RW v₂] at H
     exact exp_eq_exp.mp H
 
 
@@ -677,7 +660,6 @@ lemma mul_mul_inv_le_mul_cancel {x y : ENNReal} : (x * y⁻¹) * y ≤ x := by
   cases (Classical.em (y' = 0))
   · simp_all
   rename_i Hy'
-  simp
   rw [← coe_inv Hy']
   rw [← coe_mul]
   rw [← coe_mul]
@@ -697,7 +679,6 @@ lemma mul_mul_inv_eq_mul_cancel {x y : ENNReal} (H : y = 0 -> x = 0) (H2 : ¬(x
   cases (Classical.em (y' = 0))
   · simp_all
   rename_i Hy'
-  simp
   rw [← coe_inv Hy']
   rw [← coe_mul]
   rw [← coe_mul]
@@ -705,77 +686,48 @@ lemma mul_mul_inv_eq_mul_cancel {x y : ENNReal} (H : y = 0 -> x = 0) (H2 : ¬(x
   rw [mul_inv_cancel_right₀ Hy' x']
 
 lemma ereal_smul_le_left {w z : EReal} (s : EReal) (Hr1 : 0 < s) (Hr2 : s < ⊤) (H : s * w ≤ s * z) : w ≤ z := by
-  have defTop : some none = (⊤ : EReal) := by simp [Top.top]
-  have defBot : none = (⊥ : EReal) := by simp [Bot.bot]
-
   cases s
   · exfalso
-    rw [defBot] at Hr1
-    simp_all only [not_lt_bot]
-  rename_i s_nnr
-  cases s_nnr
-  · rw [defTop] at Hr2
-    exfalso
-    simp_all only [EReal.zero_lt_top, lt_self_iff_false]
-  rename_i s_R
-  have Hsr : some (some s_R) = Real.toEReal s_R := by simp [Real.toEReal]
-  rw [Hsr] at H
-  rw [Hsr] at Hr1
-  rw [Hsr] at Hr2
-  clear Hsr
-
-  cases w
-  · apply left_eq_inf.mp
-    rfl
-  rename_i w_nnr
-  cases w_nnr
-  · simp [defTop] at H
-    rw [EReal.mul_top_of_pos Hr1] at H
-    have X1 : z = ⊤ := by
-      cases z
-      · exfalso
-        simp at H
-        rw [defBot] at H
-        rw [EReal.mul_bot_of_pos] at H
-        · cases H
-        · apply Hr1
-      rename_i z_nnr
-      cases z_nnr
-      · simp [Top.top]
-      exfalso
-      apply top_le_iff.mp at H
-      rename_i z_R
-      have Hzr : some (some z_R) = Real.toEReal z_R := by simp [Real.toEReal]
-      rw [Hzr] at H
-      rw [<- EReal.coe_mul] at H
-      cases H
-    rw [defTop, X1]
-  rename_i w_R
-  cases z
-  · simp [defBot] at H
-    rw [EReal.mul_bot_of_pos] at H
-    apply le_bot_iff.mp at H
-    · rw [defBot]
-      have Hwr : some (some w_R) = Real.toEReal w_R := by simp [Real.toEReal]
-      rw [Hwr] at H
-      rw [<- EReal.coe_mul] at H
-      cases H
-    · apply Hr1
-  rename_i z_nnr
-  cases z_nnr
-  · exact right_eq_inf.mp rfl
-  rename_i z_R
-  have Hwr : some (some w_R) = Real.toEReal w_R := by simp [Real.toEReal]
-  have Hzr : some (some z_R) = Real.toEReal z_R := by simp [Real.toEReal]
-  rw [Hwr, Hzr] at H
-  rw [Hwr, Hzr]
-  clear Hwr
-  clear Hzr
-  apply EReal.coe_le_coe_iff.mpr
-  repeat rw [<- EReal.coe_mul] at H
-  apply EReal.coe_le_coe_iff.mp at H
-  apply le_of_mul_le_mul_left H
-  exact EReal.coe_pos.mp Hr1
+    simp at Hr1
+  · rename_i s_R
+    have Hsr : some (some s_R) = Real.toEReal s_R := by simp [Real.toEReal]
+    rw [<- Hsr] at H
+    rw [<- Hsr] at Hr1
+    rw [<- Hsr] at Hr2
+    clear Hsr
+
+    cases w
+    · apply left_eq_inf.mp
+      rfl
+    rename_i w_R
+    cases z
+    · rw [EReal.mul_bot_of_pos] at H
+      apply le_bot_iff.mp at H
+      · have Hwr : some (some s_R) = Real.toEReal s_R := by simp [Real.toEReal]
+        rw [Hwr] at H
+        rw [<- EReal.coe_mul] at H
+        cases H
+      · apply Hr1
+    rename_i z_R
+    have Hsr : some (some s_R) = Real.toEReal s_R := by simp [Real.toEReal]
+    rw [Hsr] at H
+
+    apply EReal.coe_le_coe_iff.mpr
+    repeat rw [<- EReal.coe_mul] at H
+    apply EReal.coe_le_coe_iff.mp at H
+    · apply le_of_mul_le_mul_left H
+      exact EReal.coe_pos.mp Hr1
+    · exact OrderTop.le_top w_R.toEReal
+    · rw [EReal.mul_top_of_pos] at H
+      · simp_all
+        case_EReal_isReal z
+        · rw [EReal.mul_bot_of_pos] at H
+          · cases H
+          · exact Hr1
+        · simp [Real.toEReal] at H
+          cases H
+      · exact Hr1
+  · simp at Hr2
 
 lemma ereal_smul_eq_left {w z : EReal} (s : EReal) (Hr1 : 0 < s) (Hr2 : s < ⊤) (H : s * w = s * z) : w = z := by
   apply LE.le.antisymm
diff --git a/lake-manifest.json b/lake-manifest.json
index 73b1d418..066019ea 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,10 +1,10 @@
-{"version": 7,
+{"version": "1.0.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "7b3c48b58fa0ae1c8f27889bdb086ea5e4b27b06",
+   "rev": "54bb04c3119f24fde14b9068c4b2e69db52a1450",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,7 +13,7 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "53156671405fbbd5402ed17a79bd129b961bd8d6",
+   "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "e8c8a42642ceb5af33708b79ae8a3148b681c236",
+   "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": "35e38eb320982cfd2fcc864e0e0467ca223c8cdb",
+   "rev": "c29c3cdce415240e9dcec5c583ad5d36f83f9c71",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,46 +58,10 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "dfedb0f929c2a8336ca48766c2902651313864ba",
+   "rev": "f0957a7575317490107578ebaee9efaf8e62a4ab",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": null,
-   "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/xubaiw/CMark.lean",
-   "type": "git",
-   "subDir": null,
-   "rev": "ba7b47bd773954b912ecbf5b1c9993c71a166f05",
-   "name": "CMark",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
-   "type": "git",
-   "subDir": null,
-   "rev": "effd8b8771cfd7ece69db99448168078e113c61f",
-   "name": "UnicodeBasic",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/hargonix/LeanInk",
-   "type": "git",
-   "subDir": null,
-   "rev": "f1f904e00d79a91ca6a76dec6e318531a7fd2a0f",
-   "name": "leanInk",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "doc-gen",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/doc-gen4",
-   "type": "git",
-   "subDir": null,
-   "rev": "b334278bbe691cb41af3e472ea0a85b6be81e98e",
-   "name": "«doc-gen4»",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.9.0",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "sampcert",
diff --git a/lakefile.lean b/lakefile.lean
index 6e93a044..9e875fae 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -5,7 +5,7 @@ package «sampcert» where
   -- add any package configuration options here
 
 require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git"
+  "https://github.com/leanprover-community/mathlib4.git" @ "v4.9.0"
 
 @[default_target]
 lean_lib «SampCert» where
@@ -14,6 +14,6 @@ lean_lib «FastExtract» where
 
 lean_lib «VMC» where
 
--- From doc-gen4 
-meta if get_config? env = some "doc" then 
+-- From doc-gen4
+meta if get_config? env = some "doc" then
 require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"
diff --git a/lean-toolchain b/lean-toolchain
index ef1f67e9..4ef27c47 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.8.0
+leanprover/lean4:v4.9.0