diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/ConcentratedBound.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/ConcentratedBound.lean
index f810bf2f..0edbe6c8 100644
--- a/SampCert/DifferentialPrivacy/ZeroConcentrated/ConcentratedBound.lean
+++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/ConcentratedBound.lean
@@ -75,6 +75,7 @@ theorem SG_Renyi_simplify {σ : ℝ} (h : σ ≠ 0) (μ ν : ℤ) (α : ℝ) :
   conv =>
     left
     rw [← mul_assoc]
+  rfl
 
 noncomputable def RenyiDivergence' (p q : T → ℝ) (α : ℝ) : ℝ :=
   (1 / (α - 1)) * Real.log (∑' x : T, (p x)^α  * (q x)^(1 - α))
diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/Foundations/Composition/Properties.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/Foundations/Composition/Properties.lean
index 12f7efb2..4a40224a 100644
--- a/SampCert/DifferentialPrivacy/ZeroConcentrated/Foundations/Composition/Properties.lean
+++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/Foundations/Composition/Properties.lean
@@ -18,10 +18,7 @@ theorem ENNReal_toTeal_NZ (x : ENNReal) (h1 : x ≠ 0) (h2 : x ≠ ⊤) :
   unfold ENNReal.toReal
   unfold ENNReal.toNNReal
   simp
-  intro H
-  cases H
-  . contradiction
-  . contradiction
+  constructor ; any_goals trivial
 
 theorem simp_α_1 {α : ℝ} (h : 1 < α) : 0 < α := by
   apply @lt_trans _ _ _ 1 _ _ h
@@ -82,8 +79,8 @@ theorem compose_sum_rw (nq1 nq2 : List T → SLang ℤ) (b c : ℤ) (l : List T)
     rw [A]
   rw [ENNReal.tsum_eq_add_tsum_ite b]
   simp
-  have B : ∀ x : ℤ, (@ite ℝ≥0∞ (x = b) (instDecidableEqInt x b) 0
-    (@ite ℝ≥0∞ (b = x) (instDecidableEqInt b x) (nq1 l x * ∑' (a_1 : ℤ), @ite ℝ≥0∞ (c = a_1) (instDecidableEqInt c a_1) (nq2 l a_1) 0) 0)) = 0 := by
+  have B : ∀ x : ℤ, (@ite ℝ≥0∞ (x = b) (x.instDecidableEq b) 0
+    (@ite ℝ≥0∞ (b = x) (b.instDecidableEq x) (nq1 l x * ∑' (a_1 : ℤ), @ite ℝ≥0∞ (c = a_1) (c.instDecidableEq a_1) (nq2 l a_1) 0) 0)) = 0 := by
     intro x
     split
     . simp
@@ -102,7 +99,7 @@ theorem compose_sum_rw (nq1 nq2 : List T → SLang ℤ) (b c : ℤ) (l : List T)
   congr 1
   rw [ENNReal.tsum_eq_add_tsum_ite c]
   simp
-  have C :∀ x : ℤ,  (@ite ℝ≥0∞ (x = c) (propDecidable (x = c)) 0 (@ite ℝ≥0∞ (c = x) (instDecidableEqInt c x) (nq2 l x) 0)) = 0 := by
+  have C :∀ x : ℤ,  (@ite ℝ≥0∞ (x = c) (propDecidable (x = c)) 0 (@ite ℝ≥0∞ (c = x) (c.instDecidableEq x) (nq2 l x) 0)) = 0 := by
     intro x
     split
     . simp
@@ -193,13 +190,6 @@ theorem DPCompose_NonZeroNQ {nq1 nq2 : List T → SLang ℤ} (nn1 : NonZeroNQ nq
   replace nn2 := nn2 l b
   simp [Compose]
   exists a
-  simp
-  intro H
-  cases H
-  . rename_i H
-    contradiction
-  . rename_i H
-    contradiction
 
 theorem DPCompose_NonTopNQ {nq1 nq2 : List T → SLang ℤ} (nt1 : NonTopNQ nq1) (nt2 : NonTopNQ nq2) :
   NonTopNQ (Compose nq1 nq2) := by
diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/Foundations/Mechanism/Properties.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/Foundations/Mechanism/Properties.lean
index 9b5034b5..61bdd408 100644
--- a/SampCert/DifferentialPrivacy/ZeroConcentrated/Foundations/Mechanism/Properties.lean
+++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/Foundations/Mechanism/Properties.lean
@@ -49,7 +49,7 @@ theorem NoisedQueryDP (query : List T → ℤ) (Δ ε₁ ε₂ : ℕ+) (bounded_
   . have A : (α * ↑↑ε₁ ^ 2 * (↑↑ε₂ ^ 2)⁻¹) ≤ (α * ↑↑ε₁ ^ 2 * (↑↑ε₂ ^ 2)⁻¹) := le_refl (α * ↑↑ε₁ ^ 2 * (↑↑ε₂ ^ 2)⁻¹)
     have B : 0 ≤ (α * ↑↑ε₁ ^ 2 * (↑↑ε₂ ^ 2)⁻¹) := by
       simp
-      apply @le_trans ℝ _ 0 1 α (instStrictOrderedCommRingReal.proof_3) (le_of_lt h1)
+      apply @le_trans ℝ _ 0 1 α (zero_le_one' ℝ) (le_of_lt h1)
     apply mul_le_mul A _ _ B
     . apply sq_le_sq.mpr
       simp only [abs_cast]
@@ -84,7 +84,7 @@ theorem NoisedQuery_NonTopNQ (query : List T → ℤ) (Δ ε₁ ε₂ : ℕ+) :
   rw [ENNReal.tsum_eq_add_tsum_ite (n - query l)]
   simp
   have X : ∀ x : ℤ, (@ite ℝ≥0∞ (x = n - query l) (propDecidable (x = n - query l)) 0
-    (@ite ℝ≥0∞ (n = x + query l) (instDecidableEqInt n (x + query l))
+    (@ite ℝ≥0∞ (n = x + query l) (n.instDecidableEq (x + query l))
   (ENNReal.ofReal (discrete_gaussian (↑↑Δ * ↑↑ε₂ / ↑↑ε₁) 0 ↑x)) 0)) = 0 := by
     intro x
     split
@@ -116,7 +116,7 @@ theorem NoisedQuery_NonTopSum (query : List T → ℤ) (Δ ε₁ ε₂ : ℕ+) :
   simp [NonTopSum, NoisedQuery, DiscreteGaussianGenSample]
   intro l
   have X : ∀ n: ℤ, ∀ x : ℤ, (@ite ℝ≥0∞ (x = n - query l) (propDecidable (x = n - query l)) 0
-    (@ite ℝ≥0∞ (n = x + query l) (instDecidableEqInt n (x + query l))
+    (@ite ℝ≥0∞ (n = x + query l) (n.instDecidableEq (x + query l))
     (ENNReal.ofReal (discrete_gaussian (↑↑Δ * ↑↑ε₂ / ↑↑ε₁) 0 ↑x)) 0)) = 0 := by
     intro n x
     split
@@ -158,7 +158,7 @@ theorem NoisedQuery_NonTopRDNQ (query : List T → ℤ) (Δ ε₁ ε₂ : ℕ+)
   simp [NonTopRDNQ, NoisedQuery, DiscreteGaussianGenSample]
   intro α _ l₁ l₂ _
   have A : ∀ x_1 x : ℤ, (@ite ℝ≥0∞ (x_1 = x - query l₁) (propDecidable (x_1 = x - query l₁)) 0
-  (@ite ℝ≥0∞ (x = x_1 + query l₁) (instDecidableEqInt x (x_1 + query l₁))
+  (@ite ℝ≥0∞ (x = x_1 + query l₁) (x.instDecidableEq (x_1 + query l₁))
   (ENNReal.ofReal (discrete_gaussian (↑↑Δ * ↑↑ε₂ / ↑↑ε₁) 0 ↑x_1)) 0 )) = 0 := by
     intro x y
     split
@@ -169,7 +169,7 @@ theorem NoisedQuery_NonTopRDNQ (query : List T → ℤ) (Δ ε₁ ε₂ : ℕ+)
         simp at h1
       . simp
   have B : ∀ x_1 x : ℤ, (@ite ℝ≥0∞ (x_1 = x - query l₂) (propDecidable (x_1 = x - query l₂)) 0
-    (@ite ℝ≥0∞ (x = x_1 + query l₂) (instDecidableEqInt x (x_1 + query l₂))
+    (@ite ℝ≥0∞ (x = x_1 + query l₂) (x.instDecidableEq (x_1 + query l₂))
   (ENNReal.ofReal (discrete_gaussian (↑↑Δ * ↑↑ε₂ / ↑↑ε₁) 0 ↑x_1)) 0)) = 0 := by
     intro x y
     split
diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/Foundations/Postprocessing/Properties.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/Foundations/Postprocessing/Properties.lean
index 28ffd441..2e525aac 100644
--- a/SampCert/DifferentialPrivacy/ZeroConcentrated/Foundations/Postprocessing/Properties.lean
+++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/Foundations/Postprocessing/Properties.lean
@@ -147,6 +147,7 @@ theorem δpmf_conv (nq : SLang U) (a : ℤ) (x : {n | a = f n}) (h1 : ∑' (i :
     right
     left
     left
+  rfl
 
 theorem δpmf_conv' (nq : SLang U) (f : U → ℤ) (a : ℤ) (h1 : ∑' (i : ↑{n | a = f n}), nq ↑i ≠ 0) (h2 : ∑' (i : ↑{n | a = f n}), nq ↑i ≠ ⊤) :
   (fun x : {n | a = f n} => nq x * (∑' (x : {n | a = f n}), nq x)⁻¹) = (δpmf nq f a h1 h2) := by
diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/Queries/BoundedSum/Properties.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/Queries/BoundedSum/Properties.lean
index 84f22663..e027c12e 100644
--- a/SampCert/DifferentialPrivacy/ZeroConcentrated/Queries/BoundedSum/Properties.lean
+++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/Queries/BoundedSum/Properties.lean
@@ -19,7 +19,7 @@ namespace SLang
 theorem BoundedSumQuerySensitivity (U : ℕ+) : sensitivity (BoundedSumQuery U) U := by
   simp [sensitivity, BoundedSumQuery]
   intros l₁ l₂ H
-  have A : ∀ n : ℕ, (@min ℤ instMinInt (n : ℤ) (U : ℤ) = n) ∨ (@min ℤ instMinInt n U = U) := by
+  have A : ∀ n : ℕ, (min (n : ℤ) (U : ℤ) = n) ∨ (min (n : ℤ) U = U) := by
     intro n
     simp
     exact Nat.le_total n ↑U
diff --git a/SampCert/Extractor/Extension.lean b/SampCert/Extractor/Extension.lean
index 80f4aaf2..2d502965 100644
--- a/SampCert/Extractor/Extension.lean
+++ b/SampCert/Extractor/Extension.lean
@@ -13,7 +13,7 @@ structure State where
   map : SMap Name String := {}
   decls : List String := []
   inlines : List String := []
-  glob : SMap Name MDef := {}
+  glob : SMap String MDef := {}
   deriving Inhabited
 
 def State.switch (s : State) : State :=
diff --git a/SampCert/Foundations/Auto.lean b/SampCert/Foundations/Auto.lean
index 53dc99ea..5d387f14 100644
--- a/SampCert/Foundations/Auto.lean
+++ b/SampCert/Foundations/Auto.lean
@@ -10,13 +10,9 @@ attribute [simp] Pure.pure
 attribute [simp] CoeT.coe
 attribute [simp] instCoeT
 attribute [simp] CoeHTCT.coe
-attribute [simp] instCoeHTCT_1
 attribute [simp] CoeHTC.coe
-attribute [simp] instCoeHTC_1
 attribute [simp] CoeOTC.coe
-attribute [simp] instCoeOTC_1
 attribute [simp] CoeTC.coe
-attribute [simp] instCoeTC_1
 attribute [simp] Coe.coe
 attribute [simp] optionCoe
 attribute [simp] CoeOut.coe
diff --git a/SampCert/Foundations/UniformP2.lean b/SampCert/Foundations/UniformP2.lean
index 374f0c87..8523fd14 100644
--- a/SampCert/Foundations/UniformP2.lean
+++ b/SampCert/Foundations/UniformP2.lean
@@ -88,22 +88,18 @@ theorem UniformPowerOfTwoSample_apply (n : PNat) (x : Nat) (h : x < 2 ^ (log 2 n
 @[simp]
 theorem UniformPowerOfTwoSample_apply' (n : PNat) (x : Nat) (h : x ≥ 2 ^ (log 2 n)) :
   UniformPowerOfTwoSample n x = 0 := by
-  simp only [UniformPowerOfTwoSample, Lean.Internal.coeM, Bind.bind, Pure.pure, CoeT.coe,
-    CoeHTCT.coe, CoeHTC.coe, CoeOTC.coe, CoeOut.coe, toSubPMF_apply, PMF.bind_apply,
-    uniformOfFintype_apply, Fintype.card_fin, cast_pow, cast_ofNat, PMF.pure_apply,
-    ENNReal.tsum_eq_zero, _root_.mul_eq_zero, ENNReal.inv_eq_zero, ENNReal.pow_eq_top_iff,
-    ENNReal.two_ne_top, ne_eq, log_eq_zero_iff, reduceLE, or_false, not_lt, false_and, false_or]
+  simp [UniformPowerOfTwoSample]
   intro i
   cases i
   rename_i i P
   simp only
-  split
-  . rename_i h'
-    subst h'
-    have A : x < 2 ^ log 2 ↑n ↔ ¬ x ≥ 2 ^ log 2 ↑n := by exact lt_iff_not_le
-    rw [A] at P
-    contradiction
-  . simp
+  have A : i < 2 ^ log 2 ↑n ↔ ¬ i ≥ 2 ^ log 2 ↑n := by exact lt_iff_not_le
+  rw [A] at P
+  simp at P
+  by_contra CONTRA
+  subst CONTRA
+  replace A := A.1 P
+  contradiction
 
 theorem if_simpl_up2 (n : PNat) (x x_1: Fin (2 ^ log 2 ↑n)) :
   (@ite ENNReal (x_1 = x) (propDecidable (x_1 = x)) 0 (@ite ENNReal ((@Fin.val (2 ^ log 2 ↑n) x) = (@Fin.val (2 ^ log 2 ↑n) x_1)) (propDecidable ((@Fin.val (2 ^ log 2 ↑n) x) = (@Fin.val (2 ^ log 2 ↑n) x_1))) 1 0)) = 0 := by
diff --git a/SampCert/Samplers/BernoulliNegativeExponential/Properties.lean b/SampCert/Samplers/BernoulliNegativeExponential/Properties.lean
index 3cdd5c6c..57d14870 100644
--- a/SampCert/Samplers/BernoulliNegativeExponential/Properties.lean
+++ b/SampCert/Samplers/BernoulliNegativeExponential/Properties.lean
@@ -560,7 +560,7 @@ theorem BernoulliExpNegSampleUnitAux_apply' (num : ℕ) (den : ℕ+) (n : ℕ) (
   . contradiction
   . rename_i n
     let m : ℕ+ := ⟨ succ n , by exact Fin.pos { val := n, isLt := le.refl } ⟩
-    have A : succ n = m := rfl
+    have A : n + 1 = m := rfl
     rw [A]
     rw [BernoulliExpNegSampleUnitAux_apply num den m wf]
     split
@@ -731,7 +731,7 @@ theorem mass_simpl (n : ℕ) (γ : ENNReal) (h : n ≥ 2) :
       rw [B] at A
       clear B
       rw [← A]
-      simp only [cast_mul, ENNReal.nat_cast_sub, cast_one]
+      simp only [cast_mul, ENNReal.natCast_sub, cast_one]
     . simp only [ne_eq, cast_eq_zero, ENNReal.sub_eq_top_iff, ENNReal.natCast_ne_top,
       ENNReal.one_ne_top, not_false_eq_true, and_true, or_true]
     . simp only [ne_eq, ENNReal.natCast_ne_top, not_false_eq_true, true_or]
@@ -756,10 +756,10 @@ theorem mass_simpl (n : ℕ) (γ : ENNReal) (h : n ≥ 2) :
         have OR : n = 1 ∨ n ≥ 2 := by
           clear IH γ X
           cases n
-          . simp only [zero_eq, reduceSucc, ge_iff_le, reduceLE] at h
+          . simp at h
           . rename_i n
             cases n
-            . simp only [zero_eq, reduceSucc, ge_iff_le, reduceLE, or_false]
+            . simp
             . rename_i n
               right
               exact AtLeastTwo.prop
@@ -989,6 +989,7 @@ theorem series_step_3 (γ : ENNReal) :
     right
     intro n
     rw [mass_simpl (2 * (n + 1)) γ (A n)]
+  rfl
 
 noncomputable def mass'' (n : ℕ) (γ : ℝ) := (γ^n * (((n)!) : ℝ)⁻¹)
 
diff --git a/SampCert/Samplers/Gaussian/Properties.lean b/SampCert/Samplers/Gaussian/Properties.lean
index e18492b4..0cd4f96a 100644
--- a/SampCert/Samplers/Gaussian/Properties.lean
+++ b/SampCert/Samplers/Gaussian/Properties.lean
@@ -83,9 +83,9 @@ theorem DiscreteGaussianSampleLoop_normalizes (num den t : ℕ+) :
 @[simp]
 theorem ite_simpl_1' (num den t : PNat) (x : ℤ) (n : ℤ) :
   (@ite ENNReal (x = n) (propDecidable (x = n)) 0
-  (@ite ENNReal (n = x) (Int.instDecidableEqInt n x)
-  (ENNReal.ofReal ((rexp (↑↑t)⁻¹ - 1) / (rexp (↑↑t)⁻¹ + 1) * rexp (-(|↑x| / ↑↑t))) *
-    ENNReal.ofReal (rexp (-(↑(Int.natAbs (Int.sub (|x| * ↑↑t * ↑↑den) ↑↑num)) ^ 2 / ((2 : ℕ+) * ↑↑num * ↑↑t ^ 2 * ↑↑den)))))
+  (@ite ENNReal (n = x) (n.instDecidableEq x)
+  (ENNReal.ofReal (((t : ℝ)⁻¹.exp - 1) / ((t : ℝ)⁻¹.exp + 1) * (-(@abs ℝ DistribLattice.toLattice AddGroupWithOne.toAddGroup ↑x / (t : ℝ))).exp) *
+    ENNReal.ofReal (-(((|x| * t * den).sub num).natAbs ^ 2 / ((2 : ℕ+) * num * (t : ℝ) ^ 2 * den))).exp)
   0)) = 0 := by
   split
   . simp
@@ -101,7 +101,7 @@ theorem DiscreteGaussianSampleLoop_apply_true (num den t : ℕ+) (n : ℤ) :
     = ENNReal.ofReal ((rexp (t)⁻¹ - 1) / (rexp (t)⁻¹ + 1)) * ENNReal.ofReal (rexp (-(Int.natAbs n / t)) *
     rexp (-((Int.natAbs (Int.sub (|n| * t * den) ↑↑num)) ^ 2 / ((2 : ℕ+) * num * ↑↑t ^ 2 * den)))) := by
   simp only [DiscreteGaussianSampleLoop, Bind.bind, Int.natCast_natAbs, Pure.pure, SLang.bind_apply,
-    DiscreteLaplaceSample_apply, NNReal.coe_nat_cast, PNat.one_coe, cast_one, NNReal.coe_one,
+    DiscreteLaplaceSample_apply, NNReal.coe_natCast, PNat.one_coe, cast_one, NNReal.coe_one,
     div_one, one_div, Int.cast_abs, SLang.pure_apply, Prod.mk.injEq, mul_ite,
     mul_one, mul_zero, tsum_bool, and_false, ↓reduceIte, and_true, BernoulliExpNegSample_apply_true,
     cast_pow, NNReal.coe_pow, PNat.mul_coe, PNat.pow_coe, cast_mul, NNReal.coe_mul, zero_add]
@@ -254,7 +254,7 @@ theorem DiscreteGaussianSample_apply (num : PNat) (den : PNat) (x : ℤ) :
 
   simp only [ENNReal.tsum_prod', tsum_bool, ↓reduceIte, DiscreteGaussianSampleLoop_apply_true,
     PNat.mk_coe, cast_add, cast_one, Int.ofNat_ediv, PNat.pow_coe, cast_pow, zero_add, ite_mul,
-    zero_mul, SLang.pure_apply, NNReal.coe_nat_cast, div_pow]
+    zero_mul, SLang.pure_apply, NNReal.coe_natCast, div_pow]
   rw [ENNReal.tsum_eq_add_tsum_ite x]
   conv =>
     left
@@ -372,6 +372,6 @@ theorem DiscreteGaussianSample_normalizes (num : PNat) (den : PNat) :
     apply discrete_gaussian_normalizes A
   . intro n
     apply discrete_gaussian_nonneg A 0 n
-  . apply discrete_gaussian_summable A 0
+  . apply discrete_gaussian_summable A
 
 end SLang
diff --git a/SampCert/Samplers/GaussianGen/Properties.lean b/SampCert/Samplers/GaussianGen/Properties.lean
index c14fb036..aa839278 100644
--- a/SampCert/Samplers/GaussianGen/Properties.lean
+++ b/SampCert/Samplers/GaussianGen/Properties.lean
@@ -17,7 +17,7 @@ namespace SLang
 
 theorem if_simple_GaussianGen (x_1 x μ : ℤ) :
   (@ite ENNReal (x_1 = x - μ) (propDecidable (x_1 = x - μ)) 0
-  (@ite ENNReal (x = x_1 + μ) (Int.instDecidableEqInt x (x_1 + μ))
+  (@ite ENNReal (x = x_1 + μ) (x.instDecidableEq (x_1 + μ))
   (ENNReal.ofReal (gauss_term_ℝ (↑↑num / ↑↑den) 0 ↑x_1 / ∑' (x : ℤ), gauss_term_ℝ (↑↑num / ↑↑den) 0 ↑x)) 0)) = 0 := by
   split
   . simp
diff --git a/SampCert/Samplers/Laplace/Properties.lean b/SampCert/Samplers/Laplace/Properties.lean
index 26e4d7f5..edc0beab 100644
--- a/SampCert/Samplers/Laplace/Properties.lean
+++ b/SampCert/Samplers/Laplace/Properties.lean
@@ -22,7 +22,7 @@ namespace SLang
 theorem DiscreteLaplaceSampleLoopIn1Aux_normalizes (t : PNat) :
   (∑' x : ℕ × Bool, (DiscreteLaplaceSampleLoopIn1Aux t) x) = 1 := by
   simp only [DiscreteLaplaceSampleLoopIn1Aux, Bind.bind, Pure.pure, SLang.bind_apply,
-    SLang.pure_apply, tsum_bool,  NNReal.coe_nat_cast,
+    SLang.pure_apply, tsum_bool,  NNReal.coe_natCast,
      ENNReal.tsum_prod', Prod.mk.injEq, mul_ite, mul_one, mul_zero,
     and_true, and_false, ↓reduceIte, add_zero, zero_add]
   conv =>
@@ -32,7 +32,7 @@ theorem DiscreteLaplaceSampleLoopIn1Aux_normalizes (t : PNat) :
     congr
     . rw [ENNReal.tsum_eq_add_tsum_ite a]
     . rw [ENNReal.tsum_eq_add_tsum_ite a]
-  simp only [↓reduceIte, NNReal.coe_nat_cast]
+  simp only [↓reduceIte, NNReal.coe_natCast]
   have A : forall x a, (@ite ENNReal (x = a) (Classical.propDecidable (x = a)) 0
       (if a = x then UniformSample t x * BernoulliExpNegSample x t false else 0)) = 0 := by
     intro x a
@@ -67,7 +67,7 @@ theorem DiscreteLaplaceSampleLoopIn1Aux_normalizes (t : PNat) :
       intro x
       rw [B]
   clear A B
-  simp only [ NNReal.coe_nat_cast, tsum_zero, add_zero]
+  simp only [ NNReal.coe_natCast, tsum_zero, add_zero]
   conv =>
     left
     right
@@ -94,10 +94,10 @@ theorem DiscreteLaplaceSampleLoopIn1Aux_apply_true (t : PNat) (n : ℕ) :
     right
     intro a
     rw [tsum_bool]
-  simp only [and_false, ↓reduceIte, and_true,  NNReal.coe_nat_cast,
+  simp only [and_false, ↓reduceIte, and_true,  NNReal.coe_natCast,
     zero_add, mul_ite, mul_zero]
   rw [ENNReal.tsum_eq_add_tsum_ite n]
-  have A : ∀ x, (@ite ENNReal (x = n) (Classical.propDecidable (x = n)) 0
+  have A : ∀ x, (@ite ENNReal (x = n) (propDecidable (x = n)) 0
       (@ite ENNReal (n = x) (instDecidableEqNat n x) (UniformSample t x * BernoulliExpNegSample x t true) 0)) = 0 := by
     intro x
     split
@@ -113,7 +113,7 @@ theorem DiscreteLaplaceSampleLoopIn1Aux_apply_true (t : PNat) (n : ℕ) :
     right
     intro x
     rw [A]
-  simp only [↓reduceIte, NNReal.coe_nat_cast, tsum_zero, add_zero]
+  simp only [↓reduceIte, NNReal.coe_natCast, tsum_zero, add_zero]
   rw [UniformSample_apply']
   rw [BernoulliExpNegSample_apply_true n]
   simp
@@ -129,7 +129,7 @@ theorem DiscreteLaplaceSampleLoopIn1Aux_apply_false (t : PNat) (n : ℕ) :
     right
     intro a
     rw [tsum_bool]
-  simp only [and_true,  NNReal.coe_nat_cast, and_false,
+  simp only [and_true,  NNReal.coe_natCast, and_false,
     ↓reduceIte, add_zero, mul_ite, mul_zero]
   rw [ENNReal.tsum_eq_add_tsum_ite n]
   have A : ∀ x, (@ite ENNReal (x = n) (Classical.propDecidable (x = n)) 0
@@ -148,7 +148,7 @@ theorem DiscreteLaplaceSampleLoopIn1Aux_apply_false (t : PNat) (n : ℕ) :
     right
     intro x
     rw [A]
-  simp only [↓reduceIte, NNReal.coe_nat_cast, tsum_zero,
+  simp only [↓reduceIte, NNReal.coe_natCast, tsum_zero,
     add_zero]
   rw [UniformSample_apply']
   rw [BernoulliExpNegSample_apply_false]
@@ -319,17 +319,13 @@ theorem DiscreteLaplaceSampleLoopIn2_eq (num : Nat) (den : PNat) :
 theorem DiscreteLaplaceSampleLoop_apply (num : PNat) (den : PNat) (n : ℕ) (b : Bool) :
   (DiscreteLaplaceSampleLoop num den) (b,n)
     = ENNReal.ofReal (rexp (-(↑↑den / ↑↑num))) ^ n * (1 - ENNReal.ofReal (rexp (-(↑↑den / ↑↑num)))) * ((2 : ℕ+): ENNReal)⁻¹ := by
-  simp only [DiscreteLaplaceSampleLoop, Bind.bind, DiscreteLaplaceSampleLoopIn2_eq, Pure.pure,
-    SLang.bind_apply, geometric_apply, BernoulliExpNegSample_apply_true,
-    NNReal.coe_nat_cast, BernoulliExpNegSample_apply_false, BernoulliSample_apply, cast_one,
-    one_div, SLang.pure_apply, Prod.mk.injEq, mul_ite, mul_one, mul_zero, tsum_bool, ↓reduceIte,
-    ite_mul, zero_mul]
+  simp [DiscreteLaplaceSampleLoop, tsum_bool]
   rw [ENNReal.tsum_eq_add_tsum_ite (n + 1)]
   simp only [add_eq_zero, one_ne_zero, and_false, ↓reduceIte, add_tsub_cancel_right, and_true]
   have A : ∀ x, (@ite ENNReal (x = n + 1) (Classical.propDecidable (x = n + 1)) 0
       (@ite ENNReal (x = 0) (instDecidableEqNat x 0) 0
   (ENNReal.ofReal (rexp (-(↑↑den / ↑↑num))) ^ (x - 1) * (1 - ENNReal.ofReal (rexp (-(↑↑den / ↑↑num)))) *
-    ((if b = false ∧ n = x - 1 then 1 - ((2 : ℕ+): ENNReal)⁻¹ else 0) + if b = true ∧ n = x - 1 then ((2 : ℕ+): ENNReal)⁻¹ else 0))) ) = 0 := by
+    ((@ite ENNReal (b = false ∧ n = x - 1) instDecidableAnd 2⁻¹ 0 : ENNReal) + @ite ENNReal (b = true ∧ n = x - 1) instDecidableAnd 2⁻¹ 0 : ENNReal))) ) = 0 := by
     intro x
     split
     . simp only
@@ -375,7 +371,6 @@ theorem DiscreteLaplaceSampleLoop_apply (num : PNat) (den : PNat) (n : ℕ) (b :
   split
   . rename_i h
     simp only [h, ↓reduceIte, add_zero]
-    exact ENNReal.one_sub_inv_two
   . simp only [zero_add, ite_eq_left_iff, Bool.not_eq_true]
     rename_i h1
     intro h2
@@ -451,7 +446,7 @@ theorem DiscreteLaplaceSampleLoop_normalizes (num : PNat) (den : PNat) :
   (∑' x, (DiscreteLaplaceSampleLoop num den) x) = 1 := by
   simp only [DiscreteLaplaceSampleLoop, Bind.bind, DiscreteLaplaceSampleLoopIn2_eq, Pure.pure,
     SLang.bind_apply,
-    NNReal.coe_nat_cast,  cast_one,
+    NNReal.coe_natCast,  cast_one,
     one_div, SLang.pure_apply, ite_mul, tsum_bool, ↓reduceIte, zero_mul, ENNReal.tsum_prod',
     Prod.mk.injEq, mul_ite, mul_one, mul_zero, true_and, false_and, add_zero, zero_add]
   conv =>
@@ -476,7 +471,7 @@ theorem DiscreteLaplaceSampleLoop_normalizes (num : PNat) (den : PNat) :
     simp
 
   simp only [add_tsub_cancel_right, ↓reduceIte,  add_eq_zero, one_ne_zero,
-    and_false,  NNReal.coe_nat_cast,
+    and_false,  NNReal.coe_natCast,
      cast_one, one_div, ite_mul, zero_mul]
 
   simp only [add_zero]
@@ -485,13 +480,13 @@ theorem DiscreteLaplaceSampleLoop_normalizes (num : PNat) (den : PNat) :
   rw [A]
   simp only [ge_iff_le, _root_.zero_le, tsub_eq_zero_of_le, ↓reduceIte,
     cast_one, one_div, zero_mul, ite_self,  add_eq_zero, one_ne_zero,
-    and_false, NNReal.coe_nat_cast, add_tsub_cancel_right,
+    and_false, NNReal.coe_natCast, add_tsub_cancel_right,
      zero_add]
 
   rw [ENNReal.tsum_mul_right]
   rw [ENNReal.tsum_mul_right]
   rw [← mul_add]
-  have A := BernoulliSample_normalizes' 1 2 DiscreteLaplaceSampleLoop.proof_1
+  have A := BernoulliSample_normalizes' 1 2 (by exact NeZero.one_le)
   simp only [Fintype.univ_bool, cast_one, one_div, mem_singleton,
     not_false_eq_true, sum_insert, ↓reduceIte, sum_singleton] at A
   rw [add_comm] at A
@@ -629,11 +624,11 @@ theorem DiscreteLaplaceSample_apply (num den : PNat) (x : ℤ) :
     simp (config := { contextual := true }) only [↓reduceIte, IsEmpty.forall_iff, decide_True,
       DiscreteLaplaceSampleLoop_apply, decide_eq_true_eq, Nat.cast_inj, ite_simpl_1, tsum_zero,
       add_zero, forall_true_left, decide_not, Bool.not_eq_true', decide_eq_false_iff_not, ite_not,
-      ite_mul, zero_mul, ite_simpl_4, NNReal.coe_nat_cast, inv_div, Int.cast_ofNat,
+      ite_mul, zero_mul, ite_simpl_4, NNReal.coe_natCast, inv_div, Int.cast_ofNat,
       Complex.abs_natCast]
     conv =>
       right
-      simp only [PNat.val_ofNat, reduceSucc, cast_ofNat, Int.cast_natCast, Complex.ofReal_nat_cast,
+      simp only [PNat.val_ofNat, reduceSucc, cast_ofNat, Int.cast_natCast, Complex.ofReal_natCast,
         Complex.abs_natCast]
     conv =>
       right
@@ -751,12 +746,12 @@ theorem DiscreteLaplaceSample_apply (num den : PNat) (x : ℤ) :
       DiscreteLaplaceSampleLoop_apply, decide_eq_true_eq, ne_eq, X, not_false_eq_true, ite_simpl_5,
       tsum_zero, forall_true_left, neg_inj, Nat.cast_inj, decide_not, Bool.not_eq_true',
       decide_eq_false_iff_not, ite_not, ite_mul, zero_mul, ite_simpl_1, add_zero, zero_add,
-      NNReal.coe_nat_cast, inv_div, Int.cast_neg, Int.cast_ofNat, AbsoluteValue.map_neg,
+      NNReal.coe_natCast, inv_div, Int.cast_neg, Int.cast_ofNat, AbsoluteValue.map_neg,
       Complex.abs_natCast]
     conv =>
       right
       simp only [PNat.val_ofNat, reduceSucc, cast_ofNat, Int.cast_natCast, Complex.ofReal_neg,
-        Complex.ofReal_nat_cast, map_neg_eq_map, Complex.abs_natCast]
+        Complex.ofReal_natCast, map_neg_eq_map, Complex.abs_natCast]
     conv =>
       right
       right
@@ -917,8 +912,6 @@ theorem DiscreteLaplaceSample_normalizes (num den : PNat) :
     intro _
     existsi 1
     simp
-    rw [not_or]
-    simp
     apply exp_pos (-(↑↑den / ↑↑num))
   . rw [← @ENNReal.tsum_add]
     rw [ne_iff_lt_or_gt]
diff --git a/SampCert/Util/Gaussian/DiscreteGaussian.lean b/SampCert/Util/Gaussian/DiscreteGaussian.lean
index 0118fd73..99f2566a 100644
--- a/SampCert/Util/Gaussian/DiscreteGaussian.lean
+++ b/SampCert/Util/Gaussian/DiscreteGaussian.lean
@@ -224,7 +224,7 @@ theorem discrete_gaussian_nonneg {σ : ℝ} (h : σ ≠ 0) (μ : ℝ) (n : ℤ)
   0 ≤ discrete_gaussian σ μ n := by
   apply le_of_lt (discrete_gaussian_pos h μ n)
 
-theorem discrete_gaussian_summable {σ : ℝ} (h : σ ≠ 0) (μ : ℝ) :
+theorem discrete_gaussian_summable {σ : ℝ} (h : σ ≠ 0) :
   Summable fun (n : ℤ) => discrete_gaussian σ 0 n := by
   unfold discrete_gaussian
   apply Summable.div_const
diff --git a/SampCert/Util/Gaussian/GaussPeriodicity.lean b/SampCert/Util/Gaussian/GaussPeriodicity.lean
index 379b2d5f..c44da7fd 100644
--- a/SampCert/Util/Gaussian/GaussPeriodicity.lean
+++ b/SampCert/Util/Gaussian/GaussPeriodicity.lean
@@ -11,8 +11,8 @@ theorem SGShift (μ σ : ℝ) (n : ℤ) (k : ℤ) :
   simp [gauss_term_ℝ, gauss_term_ℝ]
   ring_nf
 
-theorem SGShift' (μ ss : ℝ) (n : ℤ) (k : ℤ) :
-  (gauss_term_ℝ σ μ) (((-(n + k)) : ℤ) : ℝ) =   (gauss_term_ℝ σ (-(μ + k))) n := by
+theorem SGShift' (μ : ℝ) (n : ℤ) (k : ℤ) :
+  (gauss_term_ℝ σ μ) (((-(n + k)) : ℤ) : ℝ) = (gauss_term_ℝ σ (-(μ + k))) n := by
   simp [gauss_term_ℝ, gauss_term_ℝ]
   ring_nf
 
@@ -29,7 +29,7 @@ theorem SGSummableShift' {σ : ℝ} (h : σ ≠ 0) (μ : ℝ) (k : ℤ) :
   conv =>
     right
     intro n
-    rw [SGShift' μ σ n k]
+    rw [SGShift' μ n k]
   apply GaussConvergenceNatPos h
 
 theorem SG_1_periodic {σ : ℝ} (h : σ ≠ 0) (μ : ℝ) :
diff --git a/lake-manifest.json b/lake-manifest.json
index 5177cf4e..dc6856af 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,11 +1,11 @@
 {"version": 7,
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover/std4",
+ [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a",
-   "name": "std",
+   "rev": "f3e6d5d994e7d6a6c5bb5820068d9c7d2d004e30",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
@@ -13,7 +13,7 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "64365c656d5e1bffa127d2a1795f471529ee0178",
+   "rev": "53156671405fbbd5402ed17a79bd129b961bd8d6",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -22,25 +22,25 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "5fefb40a7c9038a7150e7edd92e43b1b94c49e79",
+   "rev": "de11e0ecf372976e6d627c210573146153090d2d",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8",
+   "rev": "e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.30",
+   "inputRev": "v0.0.36",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5",
+   "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -49,16 +49,16 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "61a79185b6582573d23bf7e17f2137cd49e7e662",
+   "rev": "35e38eb320982cfd2fcc864e0e0467ca223c8cdb",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "55659511c4da9e65833596657350420712e1b9b1",
+   "rev": "3570694dc49dfeb1c8d364aad7e3b6fcb6c6f0eb",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
diff --git a/lean-toolchain b/lean-toolchain
index 9ad30404..d8a6d7ef 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.7.0
+leanprover/lean4:v4.8.0-rc1