chore: Update Lean to v4.34.1

SampCert.lean

@@ -18,8 +18,17 @@ import Init.Data.UInt.Lemmas
 
 open SLang PMF
 
-def combineConcentrated := @privNoisedBoundedMean_DP zCDPSystem
-def combinePure := @privNoisedBoundedMean_DP PureDPSystem
+theorem combineConcentrated [dpn : DPNoise (zCDPSystem (T := ℕ))] (U ε₁ ε₂ : ℕ+) (ε : NNReal)
+    (h : dpn.noise_priv ε₁ (2 * ε₂) (ε / 2)) :
+    @DPSystem.prop ℕ (zCDPSystem (T := ℕ)) ℚ
+      (@privNoisedBoundedMean (zCDPSystem (T := ℕ)) dpn U ε₁ ε₂) ε :=
+  @privNoisedBoundedMean_DP (zCDPSystem (T := ℕ)) dpn U ε₁ ε₂ ε h
+
+theorem combinePure [dpn : DPNoise (PureDPSystem (T := ℕ))] (U ε₁ ε₂ : ℕ+) (ε : NNReal)
+    (h : dpn.noise_priv ε₁ (2 * ε₂) (ε / 2)) :
+    @DPSystem.prop ℕ (PureDPSystem (T := ℕ)) ℚ
+      (@privNoisedBoundedMean (PureDPSystem (T := ℕ)) dpn U ε₁ ε₂) ε :=
+  @privNoisedBoundedMean_DP (PureDPSystem (T := ℕ)) dpn U ε₁ ε₂ ε h
 
 /-
 ##  Example: execute the histogram mean on a list

SampCert/DifferentialPrivacy/Abstract.lean

@@ -102,11 +102,9 @@ end DPSystem
 
 lemma DPSystem_prop_ext [dps : DPSystem T] {ε₁ ε₂ : NNReal} (m : Mechanism T U) (Hε : ε₁ = ε₂) (H : dps.prop m ε₁) :
     dps.prop m ε₂ := by
-  rw [<- Hε]
-  assumption
+  rwa [← Hε]
 
 
-@[simp]
 lemma bind_bind_indep (p : Mechanism T U) (q : Mechanism T V) (h : U → V → PMF A) :
     (fun l => (p l) >>= (fun a : U => (q l) >>= fun b : V => h a b)) =
     fun l => (privCompose p q l) >>= (fun z => h z.1 z.2) := by

SampCert/DifferentialPrivacy/Neighbours.lean

@@ -26,7 +26,7 @@ inductive Neighbour (l₁ l₂ : List T) : Prop where
 /--
 Neighbour relation is symmetric.
 -/
-def Neighbour_symm (l₁ l₂ : List T) (H : Neighbour l₁ l₂) : Neighbour l₂ l₁ := by
+theorem Neighbour_symm (l₁ l₂ : List T) (H : Neighbour l₁ l₂) : Neighbour l₂ l₁ := by
   cases H
   · rename_i _ _ _ Hl1 Hl2
     exact Neighbour.Deletion Hl2 Hl1

SampCert/DifferentialPrivacy/Pure/AdaptiveComposition.lean

@@ -7,7 +7,7 @@ import SampCert.DifferentialPrivacy.Generic
 import SampCert.DifferentialPrivacy.Pure.DP
 import Mathlib.Data.Set.Defs
 import Mathlib.Data.Set.Prod
-import Mathlib.Logic.IsEmpty.Basic
+import Mathlib.Basic.IsEmpty.Basic
 
 noncomputable section
 

SampCert/DifferentialPrivacy/Queries/AboveThresh/Properties.lean

@@ -333,7 +333,6 @@ lemma sv1_loop_ub (qs : sv_query sv_T) (T τ : ℤ) (ε₁ ε₂ : ℕ+) (l : Li
         conv =>
           enter [1, a]
           rw [← ENNReal.tsum_mul_right]
-          simp
         rw [ENNReal.tsum_comm]
         enter [1, b]
 
@@ -761,31 +760,34 @@ def sv4_loop (qs : sv_query sv_T) (T : ℤ) (ε₁ ε₂ : ℕ+) (τ : ℤ) (l :
   let v <- probWhileCut (sv4_aboveThreshC qs T τ l) sv4_aboveThreshF (point + 1) (init, presamples)
   return v.1
 
+omit dps dpn in
 /-- Total mass of a point distribution restricted to the states with a given
 first component. -/
 lemma tsum_indicator_pure (X : sv4_state) (fs : sv1_state) (h : fs = X.1) :
     (∑' (a : sv4_state), if fs = a.1 then probPure X a else 0) = 1 := by
-  rw [tsum_eq_single X (fun b hb => by simp [SLang.pure_apply_of_ne _ _ hb, hb])]
-  simp [h, SLang.pure_apply_self]
+  rw [tsum_eq_single X (fun b hb => by simp [hb])]
+  simp [h]
 
+omit dps dpn in
 /-- When `sv4`'s loop condition fails the loop halts immediately. -/
 lemma sv4_probWhileCut_succ_false (qs : sv_query sv_T) (T τ : ℤ) (l : List sv_T) (n : ℕ)
     (s : sv1_state) (ps : List ℤ) (h : ¬ sv1_aboveThreshC qs T τ l s = true) :
     probWhileCut (sv4_aboveThreshC qs T τ l) sv4_aboveThreshF (n + 1) (s, ps) =
     probPure (s, ps) := by
   have hC : ¬ sv4_aboveThreshC qs T τ l (s, ps) = true := h
   simp only [probWhileCut, probWhileFunctional]
-  rw [if_neg hC]
+  rw [ite_eq_right hC]
   rfl
 
+omit dps dpn in
 /-- One step of `sv4`'s loop: when the condition holds, the head presample is
 consumed and the state advances. -/
 lemma sv4_probWhileCut_succ (qs : sv_query sv_T) (T τ : ℤ) (l : List sv_T) (n : ℕ)
     (s : sv1_state) (p : ℤ) (ps : List ℤ) (h : sv1_aboveThreshC qs T τ l s = true) :
     probWhileCut (sv4_aboveThreshC qs T τ l) sv4_aboveThreshF (n + 1) (s, p :: ps) =
     probWhileCut (sv4_aboveThreshC qs T τ l) sv4_aboveThreshF n ((s.1 ++ [s.2], p), ps) := by
   have hC : sv4_aboveThreshC qs T τ l (s, p :: ps) = true := h
-  simp only [probWhileCut, probWhileFunctional, hC, if_true, sv4_aboveThreshF,
+  simp only [probWhileCut, probWhileFunctional, hC, ite_true, sv4_aboveThreshF,
     Bind.bind, Pure.pure]
   exact SLang.pure_bind _ _
 
@@ -856,7 +858,7 @@ lemma sv4_presample_eval (ε₁ ε₂ : ℕ+) (n : ℕ) (s : { l : List ℤ // L
       rw [← HF]
       rw [← this]
       rw [mul_comm]
-    haveI : RightCommutative F := by
+    have : RightCommutative F := by
       subst HF
       exact ⟨fun b a₁ a₂ => mul_right_comm _ _ _⟩
     rw [← List.foldl_cons]
@@ -920,6 +922,7 @@ lemma sv4_presample_split' (ε₁ ε₂ : ℕ+) (point : ℕ) (z : ℤ) (p : { l
       trivial
 
 
+omit dps dpn in
 lemma foldl_mul_left (g : ℤ → ENNReal) (a : ENNReal) (l : List ℤ) :
     List.foldl (fun acc b => acc * g b) a l = a * List.foldl (fun acc b => acc * g b) 1 l := by
   induction l generalizing a with
@@ -934,7 +937,7 @@ lemma sv4_presample_split'' (ε₁ ε₂ : ℕ+) (point : ℕ) (z : ℤ) (p : {
     sv4_presample ε₁ ε₂ (point + 1) ⟨ (p.1 ++ [z]), HP ⟩ := by rw [sv4_presample_split']
 
 -- Splits and rearranges the functions
-def sv4_presample_split (ε₁ ε₂ : ℕ+) (point : ℕ) :
+theorem sv4_presample_split (ε₁ ε₂ : ℕ+) (point : ℕ) :
     sv4_presample ε₁ ε₂ (point + 1) =
     (do
       let presample_1 <- sv4_presample ε₁ ε₂ 1
@@ -965,7 +968,7 @@ def sv4_presample_split (ε₁ ε₂ : ℕ+) (point : ℕ) :
   simp_all [len_list_append_rev]
 
   -- Join the sv4_presamples
-  simp only [mul_ite, mul_zero, sv4_presample_split']
+  simp only [sv4_presample_split']
   rw [vector_sum_merge]
   rw [vector_sum_merge]
 
@@ -983,14 +986,14 @@ def sv4_presample_split (ε₁ ε₂ : ℕ+) (point : ℕ) :
   · simp
     intro A B C
     right
-    apply if_neg
+    apply ite_eq_right
     intro K
     apply C
     subst K
     apply Subtype.ext
     exact (cons_headI_tail (by intro K'; subst K'; simp at B)).symm
 
-  rw [ENNReal.tsum_eq_add_tsum_ite ⟨[vsm_last final_state] ++ (vsm_init final_state), by simp [(vsm_init final_state).2, Nat.add_comm] ⟩ ]
+  rw [ENNReal.tsum_eq_add_tsum_ite ⟨[vsm_last final_state] ++ (vsm_init final_state), by simp [(vsm_init final_state).2] ⟩ ]
   refine Eq.trans (zero_add _).symm ?_
   conv =>
     rhs
@@ -999,7 +1002,7 @@ def sv4_presample_split (ε₁ ε₂ : ℕ+) (point : ℕ) :
   · symm
     simp
     intro A B C
-    apply if_neg
+    apply ite_eq_right
     intro K
     apply C
     subst K
@@ -1208,7 +1211,7 @@ lemma sv3_sv4_loop_eq_zero (qs : sv_query sv_T) (T τ : ℤ) (ε₁ ε₂ : ℕ+
       show (if sv1_aboveThreshC qs T τ l init = true then
               ((sv4_aboveThreshF (init, ([] : List ℤ))).probBind fun _ => probZero)
             else probPure (init, ([] : List ℤ))) i = 0
-      rw [if_neg hcond]
+      rw [ite_eq_right hcond]
       apply pure_apply_of_ne
       intro HK
       apply hk2
@@ -1258,8 +1261,6 @@ theorem sv3_sv4_loop_eq (qs : sv_query sv_T) (T : ℤ) (ε₁ ε₂ : ℕ+) (τ
     unfold sv4_loop
     conv =>
       enter [2]
-      unfold probWhileCut
-      unfold probWhileFunctional
       unfold sv4_aboveThreshC
 
     split
@@ -1290,10 +1291,6 @@ theorem sv3_sv4_loop_eq (qs : sv_query sv_T) (T : ℤ) (ε₁ ε₂ : ℕ+) (τ
       match vs1, Hvs1 with
       | [], Hvs1 => exact absurd Hvs1 (by simp)
       | vs1 :: vs_emp, Hvs1 =>
-      conv =>
-        enter [2, 1, a, 1]
-        unfold sv4_aboveThreshF
-        simp [len_list_append_rev]
       have Hemp : vs_emp = [] := by cases vs_emp <;> simp_all
       subst Hemp
       show probWhileCut (sv4_aboveThreshC qs T τ l) sv4_aboveThreshF (point + 1)
@@ -1434,7 +1431,7 @@ lemma sv5_sv6_loop_base_case (qs :  sv_query sv_T) (T : ℤ) (τ : ℤ) (l : Lis
   unfold probWhileFunctional
   split
   · next h =>
-    simp [probWhileCut, sv6_loop]
+    simp [sv6_loop]
     rw [h]
     simp
   · next h =>
@@ -1448,7 +1445,7 @@ lemma sv5_sv6_loop_base_case (qs :  sv_query sv_T) (T : ℤ) (τ : ℤ) (l : Lis
     have Hpt : point = sv1_threshold (past, pres) := by
       simp [sv1_threshold]
       omega
-    rw [if_pos Hpt]
+    rw [ite_eq_left Hpt]
     conv =>
       lhs; rw [← add_zero (1 : ENNReal)]
     congr 1
@@ -1827,9 +1824,9 @@ lemma sv1_lb_advance (τ : ℤ) (ε₁ ε₂ : ℕ+) (l : List sv_T) (cut : ℕ)
   rw [Hunroll]
   unfold probWhileFunctional
   by_cases hcond : sv1_aboveThreshC qs T τ l (H, v) = true
-  · rw [if_pos hcond]
+  · rw [ite_eq_left hcond]
     simp
-  · rw [if_neg hcond]
+  · rw [ite_eq_right hcond]
     simp
     apply ENNReal.tsum_lb_single (List.length H)
     apply ENNReal.tsum_lb_single (H, v)
@@ -1863,7 +1860,7 @@ lemma sv1_lb_advance (τ : ℤ) (ε₁ ε₂ : ℕ+) (l : List sv_T) (cut : ℕ)
       enter [1, b]
       rw [X b]
     clear X
-    simp [sv1_aboveThreshF, probBind]
+    simp [sv1_aboveThreshF]
     apply le_trans
     · apply ENNReal.tsum_le_tsum
       intro a
@@ -2155,7 +2152,7 @@ lemma sv1_lb (lucky_guess : has_lucky qs T) ε₁ ε₂ l :
       show (∑' (a : { t // PLucky t }), (privNoiseGuess ε₁ ε₂) ↑a) = _
       congr 1
       ext a
-      rw [if_pos (by simp [sv1_threshold])]
+      rw [ite_eq_left (by simp [sv1_threshold])]
       rcases a with ⟨a, Ha⟩
       have hcond : sv1_aboveThreshC qs T τ l (H ++ [v], a) = false := by
         simp [sv1_aboveThreshC, sv1_noise, sv1_threshold]

SampCert/DifferentialPrivacy/Queries/Histogram/Code.lean

@@ -28,7 +28,7 @@ variable (numBins : ℕ+)
 
 def predBins : ℕ := numBins.natPred
 
-def predBins_lt_numBins : predBins numBins < numBins := by
+theorem predBins_lt_numBins : predBins numBins < numBins := by
   rw [predBins]
   cases numBins
   rename_i v Hv

SampCert/DifferentialPrivacy/RenyiDivergence.lean

@@ -278,7 +278,7 @@ theorem Renyi_Jensen_strict_real [t2 : MeasurableSingletonClass T] [tcount : Cou
   have A := strictConvexOn_rpow h
   have B := continuousOn_rpow_Ici_of_one_lt h
   have C : IsClosed (Set.Ici (0 : ℝ)) := isClosed_Ici
-  haveI : IsProbabilityMeasure (PMF.toMeasure q) := PMF.toMeasure.isProbabilityMeasure q
+  have : IsProbabilityMeasure (PMF.toMeasure q) := PMF.toMeasure.isProbabilityMeasure q
   have D := @StrictConvexOn.ae_eq_const_or_map_average_lt T ℝ t1 _ _ _ (PMF.toMeasure q)
     (Set.Ici 0) f (fun (x : ℝ) => x ^ α) inferInstance A B C
     (MeasureTheory.ae_of_all (PMF.toMeasure q) h2)
@@ -306,7 +306,7 @@ theorem Renyi_Jensen_strict_real [t2 : MeasurableSingletonClass T] [tcount : Cou
         show f x = ∑' y : T, (q y).toReal * f y
         simpa using Heqx
       · -- `q x` is nonzero but the indicator forces it to vanish — contradiction.
-        simp only [Set.mem_setOf_eq, Set.indicator_apply, if_pos Heqx] at Hx
+        simp only [Set.mem_ofPred_eq, Set.indicator_apply, ite_eq_left Heqx] at Hx
         exact absurd Hx (HT_nz x)
     · -- Case: strict Jensen gave `(∫ f)^α < ∫ f^α`.
       left
@@ -355,42 +355,42 @@ lemma Renyi_Jensen_f_MemLp [MeasurableSpace T] [MeasurableSingletonClass T] [Cou
     (Hspecial : ∀ x : T, ¬(p x = ⊤ ∧ q x ≠ 0 ∧ q x ≠ ⊤))
     (Hnts : ∑' (a : T), (p a / q a) ^ α * q a ≠ ⊤) :
     MemLp (Renyi_Jensen_f p q) (ENNReal.ofReal α) (PMF.toMeasure q) := by
-  haveI : DiscreteMeasurableSpace T := MeasurableSingletonClass.toDiscreteMeasurableSpace
+  have : DiscreteMeasurableSpace T := MeasurableSingletonClass.toDiscreteMeasurableSpace
   have HRJf_nonneg (a : T) : 0 ≤ Renyi_Jensen_f p q a := toReal_nonneg
   have HRJf_nt := Renyi_Jensen_div_ne_top p q H Hspecial
-  refine ⟨?_, ?_⟩
+  have hp_ne_zero : ENNReal.ofReal α ≠ 0 := by simp; linarith
+  have hp_ne_top : ENNReal.ofReal α ≠ ⊤ := by simp
+  rw [memLp_iff]
+  rw [eLpNorm_eq_lintegral_rpow_enorm_toReal hp_ne_zero hp_ne_top]
+  rw [toReal_ofReal (le_of_lt (lt_trans zero_lt_one h))]
+  apply ENNReal.rpow_lt_top_of_nonneg (by positivity)
+  rw [MeasureTheory.lintegral_countable']
+  have Hsummand_eq : ∀ a : T,
+      ‖Renyi_Jensen_f p q a‖ₑ ^ α * (PMF.toMeasure q) {a} = (p a / q a) ^ α * q a := by
+    intro a
+    congr 1
+    · show (‖Renyi_Jensen_f p q a‖₊ : ENNReal) ^ α = (p a / q a) ^ α
+      rw [← Real.toNNReal_eq_nnnorm_of_nonneg (HRJf_nonneg a)]
+      show (ENNReal.ofReal (Renyi_Jensen_f p q a)) ^ α = (p a / q a) ^ α
+      rw [show Renyi_Jensen_f p q a = (p a / q a).toReal from rfl,
+          ENNReal.ofReal_toReal (HRJf_nt a)]
+    · exact PMF.toMeasure_apply_singleton _ _ (measurableSet_singleton _)
+  simp_rw [Hsummand_eq]
+  exact Hnts
   · apply MeasureTheory.StronglyMeasurable.aestronglyMeasurable
     apply Measurable.stronglyMeasurable
     apply Measurable.ennreal_toReal
     show Measurable (fun x => p x / q x)
     simp_rw [division_def]
     exact (Measurable.of_discrete).mul ((Measurable.of_discrete).inv)
-  · have hp_ne_zero : ENNReal.ofReal α ≠ 0 := by simp; linarith
-    have hp_ne_top : ENNReal.ofReal α ≠ ⊤ := by simp
-    rw [eLpNorm_eq_lintegral_rpow_enorm_toReal hp_ne_zero hp_ne_top]
-    rw [toReal_ofReal (le_of_lt (lt_trans zero_lt_one h))]
-    apply ENNReal.rpow_lt_top_of_nonneg (by positivity)
-    rw [MeasureTheory.lintegral_countable']
-    have Hsummand_eq : ∀ a : T,
-        ‖Renyi_Jensen_f p q a‖ₑ ^ α * (PMF.toMeasure q) {a} = (p a / q a) ^ α * q a := by
-      intro a
-      congr 1
-      · show (‖Renyi_Jensen_f p q a‖₊ : ENNReal) ^ α = (p a / q a) ^ α
-        rw [← Real.toNNReal_eq_nnnorm_of_nonneg (HRJf_nonneg a)]
-        show (ENNReal.ofReal (Renyi_Jensen_f p q a)) ^ α = (p a / q a) ^ α
-        rw [show Renyi_Jensen_f p q a = (p a / q a).toReal from rfl,
-            ENNReal.ofReal_toReal (HRJf_nt a)]
-      · exact PMF.toMeasure_apply_singleton _ _ (measurableSet_singleton _)
-    simp_rw [Hsummand_eq]
-    exact Hnts
 
 /--
 Jensen's inequality applied to ENNReals, in the case that q is nonzero.
 -/
 lemma Renyi_Jensen_ENNReal_reduct [MeasurableSpace T] [MeasurableSingletonClass T] [Countable T]
   (p q : PMF T) {α : ℝ} (h : 1 < α) (H : AbsCts p q) :
   (∑' x : T, (p x / q x) * q x) ^ α ≤ (∑' x : T, (p x / q x) ^ α * q x) := by
-  haveI : DiscreteMeasurableSpace T := MeasurableSingletonClass.toDiscreteMeasurableSpace
+  have : DiscreteMeasurableSpace T := MeasurableSingletonClass.toDiscreteMeasurableSpace
   by_cases Hnts : ∑' (a : T), (p a / q a) ^ α * q a = ⊤
   · rw [Hnts]; exact OrderTop.le_top _
   by_cases Hspecial : ∀ x : T, ¬(p x = ⊤ ∧ q x ≠ 0 ∧ q x ≠ ⊤)
@@ -452,7 +452,7 @@ lemma Renyi_Jensen_ENNReal_converse_reduct [MeasurableSpace T] [MeasurableSingle
   (p q : PMF T) {α : ℝ} (h : 1 < α) (H : AbsCts p q) (Hq : ∀ t, q t ≠ 0)
   (Hsumeq : (∑' x : T, (p x / q x) * q x) ^ α = (∑' x : T, (p x / q x) ^ α * q x)) :
   (p = q) := by
-  haveI : DiscreteMeasurableSpace T := MeasurableSingletonClass.toDiscreteMeasurableSpace
+  have : DiscreteMeasurableSpace T := MeasurableSingletonClass.toDiscreteMeasurableSpace
   by_cases Hnts : ∑' (a : T), (p a / q a) ^ α * q a = ⊤
   · -- One of the series is Top, so the other series is too
     rw [Hnts] at Hsumeq

SampCert/DifferentialPrivacy/ZeroConcentrated/AdaptiveComposition.lean

@@ -151,10 +151,11 @@ theorem privComposeAdaptive_zCDPBound {nq1 : List T → PMF U} {nq2 : U -> List
     exact _root_.add_le_add (h1 α Hα l₁ l₂ Hneighbours) conditional_ub
   exact privComposeAdaptive_renyi_bound Hα Hneighbours HAC1 HAC2
 
+omit HU HU_meas HU_discr HU_count [MeasurableSpace V] [MeasurableSingletonClass V] [Countable V] in
 /--
 Adaptive composition preserves absolute continuity
 -/
-def privComposeAdaptive_AC (nq1 : Mechanism T U) (nq2 : U -> Mechanism T V) (Hac1 : ACNeighbour nq1) (Hac2 : ∀ u, ACNeighbour (nq2 u)) :
+theorem privComposeAdaptive_AC (nq1 : Mechanism T U) (nq2 : U -> Mechanism T V) (Hac1 : ACNeighbour nq1) (Hac2 : ∀ u, ACNeighbour (nq2 u)) :
     ACNeighbour (privComposeAdaptive nq1 nq2) := by
   simp only [ACNeighbour]
   simp [privComposeAdaptive]

SampCert/DifferentialPrivacy/ZeroConcentrated/Const.lean

@@ -33,10 +33,11 @@ theorem privConst_zCDPBound {u : U} : zCDPBound (privConst u : Mechanism T U) 0
   refine (RenyiDivergence_aux_zero (PMF.pure u) (PMF.pure u) ?G1 fun x a => a).mp rfl
   linarith
 
+omit [MeasurableSpace U] [MeasurableSingletonClass U] [Countable U] in
 /--
 Constant query satisfies absolute continuity
 -/
-def privConst_AC {u : U} : ACNeighbour (privConst u : Mechanism T U) := by
+theorem privConst_AC {u : U} : ACNeighbour (privConst u : Mechanism T U) := by
   simp [ACNeighbour, AbsCts, privConst]
 
 /--

SampCert/DifferentialPrivacy/ZeroConcentrated/DP.lean

@@ -467,9 +467,9 @@ lemma ApproximateDP_of_zCDP_pos_lt_one [Countable U] (m : Mechanism T U)
   have HK (x : U) : (1 : ENNReal) = (if (z x < ENNReal.ofReal ε') then 1 else 0) + (if (z x ≥ ENNReal.ofReal ε') then 1 else 0) := by
     by_cases h : z x < ENNReal.ofReal ε'
     · have h2 : ¬ (z x ≥ ENNReal.ofReal ε') := not_le.mpr h
-      rw [if_pos h, if_neg h2]; simp
+      rw [ite_eq_left h, ite_eq_right h2]; simp
     · have h2 : z x ≥ ENNReal.ofReal ε' := le_of_not_gt h
-      rw [if_neg h, if_pos h2]; simp
+      rw [ite_eq_right h, ite_eq_left h2]; simp
   conv =>
     enter [1, 1, a]
     rw [<- mul_one (_ * _)]
@@ -1156,7 +1156,7 @@ lemma B_eval_false (Hε : 0 < ε) (Hqp : ∀ x, ENNReal.ofReal (Real.exp (-ε))
   · simp [Function.Injective]
   · intro x Hx
     simp [Function.support] at Hx
-    simp_all only [Subtype.range_coe_subtype, Function.mem_support, ne_eq, Set.mem_setOf_eq, not_false_eq_true]
+    simp_all only [Subtype.range_coe_subtype, Function.mem_support, ne_eq, Set.mem_ofPred_eq, not_false_eq_true]
   · simp [Function.support]
     intros x _
     rw [PMF_mul_mul_inv_eq_mul_cancel p q Hac x]

SampCert/DifferentialPrivacy/ZeroConcentrated/Mechanism/Properties.lean

@@ -108,7 +108,7 @@ lemma discrete_gaussian_shift {σ : ℝ} (h : σ ≠ 0) (μ : ℝ) (τ x : ℤ)
 /--
 privNoisedQuery preserves absolute continuity between neighbours
 -/
-def privNoisedQuery_AC (query : List T -> ℤ) (Δ ε₁ ε₂ : ℕ+) : ACNeighbour (privNoisedQuery query Δ ε₁ ε₂) := by
+theorem privNoisedQuery_AC (query : List T -> ℤ) (Δ ε₁ ε₂ : ℕ+) : ACNeighbour (privNoisedQuery query Δ ε₁ ε₂) := by
   simp only [ACNeighbour]
   intro l₁ l₂ _
   rw [AbsCts]