diff --git a/TestingLowerBounds/Divergences/Hellinger.lean b/TestingLowerBounds/Divergences/Hellinger.lean
index f54f010e..0146e47c 100644
--- a/TestingLowerBounds/Divergences/Hellinger.lean
+++ b/TestingLowerBounds/Divergences/Hellinger.lean
@@ -202,25 +202,20 @@ lemma convexOn_hellingerFun (ha_pos : 0 ≤ a) : ConvexOn ℝ (Set.Ici 0) (helli
     simp only [(lt_of_le_of_lt hx hxy).ne', ↓reduceIte, zero_sub,
       (gt_trans hyz <| lt_of_le_of_lt hx hxy).ne', sub_self, zero_div, div_nonpos_iff,
       Left.nonneg_neg_iff, tsub_le_iff_right, zero_add, Left.neg_nonpos_iff, sub_nonneg]
-    right
-    exact ⟨by positivity, by linarith⟩
+    exact Or.inr ⟨by positivity, by linarith⟩
   replace ha_pos := ha_pos.lt_of_ne fun h ↦ ha_zero h.symm
   rcases (lt_trichotomy a 1) with (ha | ha | ha)
   · have : hellingerFun a = - (fun x ↦ (1 - a)⁻¹ • (x ^ a - 1)) := by
       ext x
-      simp only [Pi.neg_apply]
-      rw [hellingerFun_of_ne_zero_of_ne_one ha_pos.ne' ha.ne, smul_eq_mul, ← neg_mul, neg_inv, neg_sub]
+      rw [Pi.neg_apply, hellingerFun_of_ne_zero_of_ne_one ha_pos.ne' ha.ne, smul_eq_mul, ← neg_mul,
+        neg_inv, neg_sub]
     rw [this]
-    refine ConcaveOn.neg ?_
     exact ((Real.concaveOn_rpow ha_pos.le ha.le).sub (convexOn_const _ (convex_Ici 0))).smul
-      (by simp [ha.le])
+      (by simp [ha.le]) |>.neg
   · simp only [hellingerFun, ha, one_ne_zero, ↓reduceIte]
     exact convexOn_mul_log
-  · have h := convexOn_rpow ha.le
-    unfold hellingerFun
-    simp_rw [← smul_eq_mul, if_neg ha_pos.ne', if_neg ha.ne']
-    refine ConvexOn.smul (by simp [ha.le]) ?_
-    exact h.sub (concaveOn_const _ (convex_Ici 0))
+  · simp_rw [hellingerFun, ← smul_eq_mul, if_neg ha_pos.ne', if_neg ha.ne']
+    exact (convexOn_rpow ha.le).sub (concaveOn_const _ (convex_Ici 0)) |>.smul (by simp [ha.le])
 
 lemma tendsto_rightDeriv_hellingerFun_atTop_of_one_lt (ha : 1 < a) :
     Tendsto (rightDeriv (hellingerFun a)) atTop atTop := by
@@ -236,9 +231,8 @@ lemma derivAtTop_hellingerFun_of_one_lt (ha : 1 < a) : derivAtTop (hellingerFun
 lemma derivAtTop_hellingerFun_of_one_le (ha : 1 ≤ a) :
     derivAtTop (hellingerFun a) = ⊤ := by
   by_cases ha_eq : a = 1
-  · simp only [hellingerFun, ha, ha_eq, one_ne_zero, ↓reduceIte]
-    exact derivAtTop_mul_log
-  · exact derivAtTop_hellingerFun_of_one_lt <| lt_of_le_of_ne ha fun ha ↦ ha_eq ha.symm
+  · simp only [hellingerFun, ha, ha_eq, one_ne_zero, ↓reduceIte, derivAtTop_mul_log]
+  · exact derivAtTop_hellingerFun_of_one_lt <| lt_of_le_of_ne ha fun h ↦ ha_eq h.symm
 
 lemma derivAtTop_hellingerFun_of_lt_one (ha : a < 1) :
     derivAtTop (hellingerFun a) = 0 :=
@@ -253,9 +247,7 @@ lemma integrable_hellingerFun_iff_integrable_rpow (ha_one : a ≠ 1) [IsFiniteMe
       Pi.one_comp]
     refine (integrable_indicator_iff ?_).mpr ?_
     · apply measurableSet_eq_fun <;> fun_prop
-    · apply integrableOn_const.mpr
-      right
-      exact measure_lt_top ν _
+    · exact integrableOn_const.mpr (Or.inr (measure_lt_top ν _))
   rw [hellingerFun_of_ne_zero_of_ne_one ha_zero ha_one, integrable_const_mul_iff]
   swap; · simp [sub_eq_zero, ha_one]
   simp_rw [sub_eq_add_neg, integrable_add_const_iff]
@@ -320,7 +312,7 @@ lemma hellingerDiv_zero' (μ ν : Measure α) [SigmaFinite μ] :
   simp [ENNReal.toReal_eq_zero_iff, hx.ne]
 
 lemma hellingerDiv_zero'' (μ ν : Measure α) [SigmaFinite μ] [IsFiniteMeasure ν] :
-    hellingerDiv 0 μ ν = ν Set.univ - ν {x | 0 < (∂μ/∂ν) x} := by
+    hellingerDiv 0 μ ν = ν .univ - ν {x | 0 < (∂μ/∂ν) x} := by
   have h : {x | μ.rnDeriv ν x = 0} = {x | 0 < μ.rnDeriv ν x}ᶜ := by
     ext x
     simp only [Set.mem_setOf_eq, Set.mem_compl_iff, not_lt, nonpos_iff_eq_zero, eq_comm]
@@ -330,9 +322,8 @@ lemma hellingerDiv_zero'' (μ ν : Measure α) [SigmaFinite μ] [IsFiniteMeasure
   exact fun _ _ ↦ trivial
 
 lemma hellingerDiv_zero_toReal (μ ν : Measure α) [SigmaFinite μ] [IsFiniteMeasure ν] :
-    (hellingerDiv 0 μ ν).toReal = (ν Set.univ).toReal - (ν {x | 0 < (∂μ/∂ν) x}).toReal := by
-  rw [hellingerDiv_zero'']
-  rw [EReal.toReal_sub]
+    (hellingerDiv 0 μ ν).toReal = (ν .univ).toReal - (ν {x | 0 < (∂μ/∂ν) x}).toReal := by
+  rw [hellingerDiv_zero'', EReal.toReal_sub]
   all_goals simp [measure_ne_top]
 
 lemma hellingerDiv_zero_ne_top (μ ν : Measure α) [IsFiniteMeasure ν] :
@@ -346,7 +337,7 @@ lemma hellingerDiv_zero_ne_top (μ ν : Measure α) [IsFiniteMeasure ν] :
 
 @[simp]
 lemma hellingerDiv_zero_measure_left (ν : Measure α) [IsFiniteMeasure ν] :
-    hellingerDiv a 0 ν = (1 - a)⁻¹ * ν Set.univ := by
+    hellingerDiv a 0 ν = (1 - a)⁻¹ * ν .univ := by
   rw [hellingerDiv, fDiv_zero_measure, hellingerFun_apply_zero]
 
 @[simp]
@@ -481,7 +472,7 @@ lemma hellingerDiv_eq_integral_of_ne_top [IsFiniteMeasure μ] [SigmaFinite ν]
 This lemma is not true for `a = 0`, because `0 ^ 0 = 1`. -/
 lemma hellingerDiv_eq_integral_of_ne_top' (ha_ne_zero : a ≠ 0) (ha_ne_one : a ≠ 1)
     [IsFiniteMeasure μ] [IsFiniteMeasure ν] (h : hellingerDiv a μ ν ≠ ⊤) :
-    hellingerDiv a μ ν = (a - 1)⁻¹ * ∫ x, ((∂μ/∂ν) x).toReal ^ a ∂ν - (a - 1)⁻¹ * ν Set.univ := by
+    hellingerDiv a μ ν = (a - 1)⁻¹ * ∫ x, ((∂μ/∂ν) x).toReal ^ a ∂ν - (a - 1)⁻¹ * ν .univ := by
   rw [hellingerDiv_eq_integral_of_ne_top h]
   simp_rw [hellingerFun_of_ne_zero_of_ne_one ha_ne_zero ha_ne_one, integral_mul_left]
   rw [integral_sub _ (integrable_const _), integral_const, smul_eq_mul, mul_one, mul_sub,
@@ -498,14 +489,14 @@ lemma hellingerDiv_eq_integral_of_ne_top'' (ha_ne_zero : a ≠ 0) (ha_ne_one : a
 
 lemma hellingerDiv_eq_integral_of_lt_one' (ha_pos : 0 < a) (ha : a < 1) (μ ν : Measure α)
     [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
-    hellingerDiv a μ ν = (a - 1)⁻¹ * ∫ x, ((∂μ/∂ν) x).toReal ^ a ∂ν - (a - 1)⁻¹ * ν Set.univ :=
+    hellingerDiv a μ ν = (a - 1)⁻¹ * ∫ x, ((∂μ/∂ν) x).toReal ^ a ∂ν - (a - 1)⁻¹ * ν .univ :=
   hellingerDiv_eq_integral_of_ne_top' ha_pos.ne.symm ha.ne
     (hellingerDiv_ne_top_of_lt_one ha_pos.le ha μ ν)
 
 lemma hellingerDiv_toReal_of_lt_one (ha_pos : 0 < a) (ha : a < 1) (μ ν : Measure α)
     [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
     (hellingerDiv a μ ν).toReal
-      = (a - 1)⁻¹ * ∫ x, ((∂μ/∂ν) x).toReal ^ a ∂ν - (a - 1)⁻¹ * (ν Set.univ).toReal := by
+      = (a - 1)⁻¹ * ∫ x, ((∂μ/∂ν) x).toReal ^ a ∂ν - (a - 1)⁻¹ * (ν .univ).toReal := by
   rw [hellingerDiv_eq_integral_of_lt_one' ha_pos ha, EReal.toReal_sub]
   · simp [EReal.toReal_mul]
   · exact EReal.coe_mul _ _ ▸ EReal.coe_ne_top _
@@ -518,14 +509,14 @@ lemma hellingerDiv_of_mutuallySingular_of_one_le (ha : 1 ≤ a) [NeZero μ]
     hellingerDiv a μ ν = ⊤ := by
   have := fDiv_of_mutuallySingular hμν (f := hellingerFun a)
   rw [hellingerDiv, this, derivAtTop_hellingerFun_of_one_le ha,
-    EReal.top_mul_ennreal_coe (NeZero.ne' (μ Set.univ)).symm]
+    EReal.top_mul_ennreal_coe (NeZero.ne' (μ .univ)).symm]
   apply EReal.add_top_of_ne_bot
   rw [ne_eq, EReal.mul_eq_bot, hellingerFun_apply_zero]
   simp [measure_ne_top]
 
 lemma hellingerDiv_of_mutuallySingular_of_lt_one (ha : a < 1)
     [SigmaFinite μ] [IsFiniteMeasure ν] (hμν : μ ⟂ₘ ν) :
-    hellingerDiv a μ ν = (1 - a)⁻¹ * ν Set.univ  := by
+    hellingerDiv a μ ν = (1 - a)⁻¹ * ν .univ  := by
   rw [hellingerDiv, fDiv_of_mutuallySingular hμν, derivAtTop_hellingerFun_of_lt_one ha,
     hellingerFun_apply_zero, zero_mul, add_zero]
 
@@ -534,7 +525,7 @@ end HellingerEq
 --Maybe we could write something like this for the conditional case? Would it be useful?
 lemma hellingerDiv_le_of_lt_one (ha_nonneg : 0 ≤ a) (ha : a < 1) (μ ν : Measure α)
     [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
-    hellingerDiv a μ ν ≤ (1 - a)⁻¹ * ν Set.univ := by
+    hellingerDiv a μ ν ≤ (1 - a)⁻¹ * ν .univ := by
   by_cases h_zero : a = 0
   · rw [h_zero, hellingerDiv_zero']
     simp only [inv_one, EReal.coe_one, one_mul, EReal.coe_ennreal_le_coe_ennreal_iff, sub_zero]
@@ -547,7 +538,7 @@ lemma hellingerDiv_le_of_lt_one (ha_nonneg : 0 ≤ a) (ha : a < 1) (μ ν : Meas
   simp only [zero_sub, mul_neg, mul_one, zero_mul, add_zero, zero_rpow h_zero]
   rw [neg_inv, neg_sub]
 
-lemma hellingerDiv_symm' (ha_pos : 0 < a) (ha : a < 1) (h_eq : μ Set.univ = ν Set.univ)
+lemma hellingerDiv_symm' (ha_pos : 0 < a) (ha : a < 1) (h_eq : μ .univ = ν .univ)
     [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
     (1 - a) * hellingerDiv a μ ν = a * hellingerDiv (1 - a) ν μ := by
   rw [hellingerDiv_eq_integral_of_lt_one' ha_pos ha, hellingerDiv_eq_integral_of_lt_one']
@@ -589,15 +580,15 @@ which appears in the definition of the Renyi divergence. -/
 
 lemma meas_univ_add_mul_hellingerDiv_eq (ha_ne_zero : a ≠ 0) (ha_ne_one : a ≠ 1)
     [IsFiniteMeasure μ] [IsFiniteMeasure ν] (h : hellingerDiv a μ ν ≠ ⊤) :
-    ↑(ν Set.univ) + (a - 1) * hellingerDiv a μ ν = ∫ x, ((∂μ/∂ν) x).toReal ^ a ∂ν := by
+    ↑(ν .univ) + (a - 1) * hellingerDiv a μ ν = ∫ x, ((∂μ/∂ν) x).toReal ^ a ∂ν := by
   rw_mod_cast [hellingerDiv_eq_integral_of_ne_top' ha_ne_zero ha_ne_one h,
-    ← ENNReal.ofReal_toReal (measure_ne_top ν Set.univ), EReal.coe_ennreal_ofReal,
+    ← ENNReal.ofReal_toReal (measure_ne_top ν .univ), EReal.coe_ennreal_ofReal,
     max_eq_left ENNReal.toReal_nonneg, ← mul_sub, ← mul_assoc, mul_inv_cancel₀ _]
   ring_nf
   exact sub_ne_zero_of_ne ha_ne_one
 
 lemma meas_univ_add_mul_hellingerDiv_zero_eq (ha : a = 0) [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
-    ↑(ν Set.univ) + (a - 1) * hellingerDiv a μ ν = ν {x | 0 < (∂μ/∂ν) x} := by
+    ↑(ν .univ) + (a - 1) * hellingerDiv a μ ν = ν {x | 0 < (∂μ/∂ν) x} := by
   simp only [ha, EReal.coe_zero, zero_sub, hellingerDiv_zero'', neg_mul, one_mul, rpow_zero,
     integral_const, smul_eq_mul, mul_one]
   rw [EReal.neg_sub, ← add_assoc, ← sub_eq_add_neg, EReal.sub_self, zero_add]
@@ -605,16 +596,16 @@ lemma meas_univ_add_mul_hellingerDiv_zero_eq (ha : a = 0) [IsFiniteMeasure μ] [
 
 lemma meas_univ_add_mul_hellingerDiv_nonneg_of_le_one (ha_nonneg : 0 ≤ a) (ha : a ≤ 1)
     (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
-    0 ≤ ↑(ν Set.univ) + (a - 1) * hellingerDiv a μ ν := by
+    0 ≤ ↑(ν .univ) + (a - 1) * hellingerDiv a μ ν := by
   by_cases h_one : a = 1
   · have : (1 - 1 : EReal) = 0 := EReal.sub_self (ne_of_beq_false rfl) (ne_of_beq_false rfl)
     simp [h_one, add_zero, zero_mul, this, EReal.coe_ennreal_nonneg]
   replace ha : a < 1 := ha.lt_of_ne h_one
   calc
-    _ = (ν Set.univ) - (1 - ↑a) * hellingerDiv a μ ν := by
+    _ = (ν .univ) - (1 - ↑a) * hellingerDiv a μ ν := by
       congr
       rw [← neg_mul, EReal.neg_sub _ _, add_comm, sub_eq_add_neg] <;> simp
-    _ ≥ (ν Set.univ) - (1 - ↑a) * ((1 - a)⁻¹ * ν Set.univ) := by
+    _ ≥ (ν .univ) - (1 - ↑a) * ((1 - a)⁻¹ * ν .univ) := by
       simp_rw [sub_eq_add_neg]
       gcongr
       rw [EReal.neg_le_neg_iff]
@@ -622,7 +613,7 @@ lemma meas_univ_add_mul_hellingerDiv_nonneg_of_le_one (ha_nonneg : 0 ≤ a) (ha
       · norm_cast
         simp only [le_add_neg_iff_add_le, zero_add, ha.le]
       · exact hellingerDiv_le_of_lt_one ha_nonneg ha μ ν
-    _ = (ν Set.univ) - (ν Set.univ) := by
+    _ = (ν .univ) - (ν .univ) := by
       norm_cast
       rw [← mul_assoc, ← EReal.coe_mul, mul_inv_cancel₀ (by linarith), EReal.coe_one, one_mul]
     _ ≥ _ := by
@@ -631,7 +622,7 @@ lemma meas_univ_add_mul_hellingerDiv_nonneg_of_le_one (ha_nonneg : 0 ≤ a) (ha
 
 lemma meas_univ_add_mul_hellingerDiv_nonneg_of_one_lt (ha : 1 < a) (μ ν : Measure α)
     [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
-    0 ≤ ↑(ν Set.univ) + (a - 1) * hellingerDiv a μ ν := by
+    0 ≤ ↑(ν .univ) + (a - 1) * hellingerDiv a μ ν := by
   by_cases h_top : hellingerDiv a μ ν = ⊤
   · rw [h_top, EReal.mul_top_of_pos, EReal.add_top_of_ne_bot (EReal.coe_ennreal_ne_bot _)]
     · exact OrderTop.le_top 0
@@ -643,7 +634,7 @@ lemma meas_univ_add_mul_hellingerDiv_nonneg_of_one_lt (ha : 1 < a) (μ ν : Meas
 
 lemma meas_univ_add_mul_hellingerDiv_nonneg (ha_nonneg : 0 ≤ a) (μ ν : Measure α)
     [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
-    0 ≤ ↑(ν Set.univ) + (a - 1) * hellingerDiv a μ ν := by
+    0 ≤ ↑(ν .univ) + (a - 1) * hellingerDiv a μ ν := by
   by_cases h_le_one : a ≤ 1
   · exact meas_univ_add_mul_hellingerDiv_nonneg_of_le_one ha_nonneg h_le_one μ ν
   · exact meas_univ_add_mul_hellingerDiv_nonneg_of_one_lt
@@ -651,7 +642,7 @@ lemma meas_univ_add_mul_hellingerDiv_nonneg (ha_nonneg : 0 ≤ a) (μ ν : Measu
 
 lemma meas_univ_add_mul_hellingerDiv_eq_zero_iff (ha_ne_one : a ≠ 1)
     [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
-  ↑(ν Set.univ) + (a - 1) * hellingerDiv a μ ν = 0 ↔ μ ⟂ₘ ν ∧ hellingerDiv a μ ν ≠ ⊤ := by
+  ↑(ν .univ) + (a - 1) * hellingerDiv a μ ν = 0 ↔ μ ⟂ₘ ν ∧ hellingerDiv a μ ν ≠ ⊤ := by
   by_cases h_top : hellingerDiv a μ ν = ⊤
   · simp only [h_top, ne_eq, not_true_eq_false, and_false, iff_false]
     rcases (lt_or_gt_of_ne ha_ne_one) with ha | ha
@@ -674,7 +665,7 @@ lemma meas_univ_add_mul_hellingerDiv_eq_zero_iff (ha_ne_one : a ≠ 1)
 
 lemma meas_univ_add_mul_hellingerDiv_eq_zero_iff_of_lt_one (ha : a < 1)
     [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
-    ↑(ν Set.univ) + (a - 1) * hellingerDiv a μ ν = 0 ↔ μ ⟂ₘ ν  := by
+    ↑(ν .univ) + (a - 1) * hellingerDiv a μ ν = 0 ↔ μ ⟂ₘ ν  := by
   rw [meas_univ_add_mul_hellingerDiv_eq_zero_iff ha.ne, and_iff_left_iff_imp]
   intro hμν
   rw [hellingerDiv_of_mutuallySingular_of_lt_one ha hμν, ne_eq, EReal.mul_eq_top]
@@ -682,7 +673,7 @@ lemma meas_univ_add_mul_hellingerDiv_eq_zero_iff_of_lt_one (ha : a < 1)
 
 lemma meas_univ_add_mul_hellingerDiv_eq_zero_iff_of_one_lt (ha : 1 < a)
     [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
-    ↑(ν Set.univ) + (a - 1) * hellingerDiv a μ ν = 0 ↔ μ = 0 := by
+    ↑(ν .univ) + (a - 1) * hellingerDiv a μ ν = 0 ↔ μ = 0 := by
   rw [meas_univ_add_mul_hellingerDiv_eq_zero_iff ha.ne', hellingerDiv_ne_top_iff_of_one_le ha.le]
   refine ⟨fun ⟨h, _, h'⟩ ↦ Measure.eq_zero_of_absolutelyContinuous_of_mutuallySingular h' h,
     fun h ↦ ?_⟩
@@ -694,19 +685,19 @@ lemma meas_univ_add_mul_hellingerDiv_eq_zero_iff_of_one_lt (ha : 1 < a)
 
 lemma toENNReal_meas_univ_add_mul_hellingerDiv_eq_zero_iff_of_lt_one
     (ha_nonneg : 0 ≤ a) (ha : a < 1) [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
-    (↑(ν Set.univ) + (a - 1) * (hellingerDiv a μ ν)).toENNReal = 0 ↔ μ ⟂ₘ ν  := by
+    (↑(ν .univ) + (a - 1) * (hellingerDiv a μ ν)).toENNReal = 0 ↔ μ ⟂ₘ ν  := by
   rw [← meas_univ_add_mul_hellingerDiv_eq_zero_iff_of_lt_one ha, EReal.toENNReal_eq_zero_iff]
   exact LE.le.le_iff_eq (meas_univ_add_mul_hellingerDiv_nonneg ha_nonneg μ ν)
 
 lemma toENNReal_meas_univ_add_mul_hellingerDiv_eq_zero_iff_of_one_lt (ha : 1 < a)
     [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
-    (↑(ν Set.univ) + (a - 1) * (hellingerDiv a μ ν)).toENNReal = 0 ↔ μ = 0  := by
+    (↑(ν .univ) + (a - 1) * (hellingerDiv a μ ν)).toENNReal = 0 ↔ μ = 0  := by
   rw [← meas_univ_add_mul_hellingerDiv_eq_zero_iff_of_one_lt ha (ν := ν),
     EReal.toENNReal_eq_zero_iff]
   exact LE.le.le_iff_eq (meas_univ_add_mul_hellingerDiv_nonneg (by positivity) μ ν)
 
 lemma meas_univ_add_mul_hellingerDiv_ne_top_of_lt_one (ha : a < 1) [IsFiniteMeasure ν] :
-    ↑(ν Set.univ) + (a - 1) * hellingerDiv a μ ν ≠ ⊤ := by
+    ↑(ν .univ) + (a - 1) * hellingerDiv a μ ν ≠ ⊤ := by
   apply EReal.add_ne_top
   · simp [measure_ne_top]
   · rw [ne_eq, EReal.mul_eq_top]
@@ -717,7 +708,7 @@ lemma meas_univ_add_mul_hellingerDiv_ne_top_of_lt_one (ha : a < 1) [IsFiniteMeas
 
 lemma meas_univ_add_mul_hellingerDiv_eq_top_iff_of_one_lt (ha : 1 < a)
     [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
-    ↑(ν Set.univ) + (a - 1) * hellingerDiv a μ ν = ⊤
+    ↑(ν .univ) + (a - 1) * hellingerDiv a μ ν = ⊤
       ↔ ¬ Integrable (fun x ↦ ((∂μ/∂ν) x).toReal ^ a) ν ∨ ¬ μ ≪ ν := by
   rw [← integrable_hellingerFun_iff_integrable_rpow ha.ne',
     ← hellingerDiv_eq_top_iff_of_one_le ha.le]
@@ -725,7 +716,7 @@ lemma meas_univ_add_mul_hellingerDiv_eq_top_iff_of_one_lt (ha : 1 < a)
   · contrapose! h
     refine EReal.add_ne_top ?_ ?_
     · rw [ne_eq, EReal.coe_ennreal_eq_top_iff]
-      exact measure_ne_top ν Set.univ
+      exact measure_ne_top ν .univ
     · rw [ne_eq, EReal.mul_eq_top]
       norm_cast
       simp_rw [EReal.coe_ne_bot, EReal.coe_ne_top, sub_neg, sub_pos, ha, not_lt_of_gt ha,
@@ -794,7 +785,7 @@ lemma integrable_hellingerDiv_iff' (ha_pos : 0 < a) (ha_ne_one : a ≠ 1)
     · exact hellingerDiv_ne_top_of_lt_one ha_pos.le ha_lt _ _
     · exact hellingerDiv_ne_top_iff_of_one_lt ha_gt _ _ |>.mpr ⟨hx_int, hx_ac ha_gt.le⟩
   have h_eq_eq : ∀ᵐ x ∂μ, (hellingerDiv a (κ x) (η x)).toReal =
-      (a - 1)⁻¹ * ((∫ b, ((∂κ x/∂η x) b).toReal ^ a ∂η x) - ((η x) Set.univ).toReal) := by
+      (a - 1)⁻¹ * ((∫ b, ((∂κ x/∂η x) b).toReal ^ a ∂η x) - ((η x) .univ).toReal) := by
     filter_upwards [h_fin] with x hx
     rw [hellingerDiv_eq_integral_of_ne_top' ha_pos.ne.symm ha_ne_one hx, ← EReal.coe_mul,
       EReal.toReal_sub (EReal.coe_ne_top _) (EReal.coe_ne_bot _), EReal.toReal_coe,
@@ -813,7 +804,7 @@ lemma integrable_hellingerDiv_iff' (ha_pos : 0 < a) (ha_ne_one : a ≠ 1)
     <| inv_eq_zero.mp.mt <| sub_ne_zero_of_ne ha_ne_one)]
   obtain ⟨C, ⟨hC_finite, hC⟩⟩ := IsFiniteKernel.exists_univ_le (κ := η)
   refine integrable_add_iff_integrable_left <| (integrable_const C.toReal).mono' ?_ ?_
-  · exact Kernel.measurable_coe η MeasurableSet.univ |>.ennreal_toReal.neg.aestronglyMeasurable
+  · exact η.measurable_coe .univ |>.ennreal_toReal.neg.aestronglyMeasurable
   refine eventually_of_forall (fun x ↦ ?_)
   rw [norm_eq_abs, abs_neg, abs_eq_self.mpr ENNReal.toReal_nonneg, ENNReal.toReal_le_toReal
     (measure_ne_top _ _) (lt_top_iff_ne_top.mp hC_finite)]
@@ -828,18 +819,18 @@ lemma integrable_hellingerDiv_zero [CountableOrCountablyGenerated α β]
   obtain ⟨C, ⟨hC_finite, hC⟩⟩ := IsFiniteKernel.exists_univ_le (κ := η)
   simp only [EReal.toReal_coe_ennreal]
   have h_eq : (fun x ↦ ((η x) {y | ((κ x).rnDeriv (η x) y).toReal = 0}).toReal) =
-      fun x ↦ ((η x) {y | (Kernel.rnDeriv κ η x y).toReal = 0}).toReal := by
+      fun x ↦ ((η x) {y | (κ.rnDeriv η x y).toReal = 0}).toReal := by
     ext x
     congr 1
     apply measure_congr
-    filter_upwards [Kernel.rnDeriv_eq_rnDeriv_measure κ η x] with y hy
+    filter_upwards [κ.rnDeriv_eq_rnDeriv_measure η x] with y hy
     simp only [Set.setOf_app_iff, eq_iff_iff, hy]
   simp_rw [h_eq]
   apply (integrable_const C.toReal).mono'
   · apply Measurable.aestronglyMeasurable
     apply Measurable.ennreal_toReal
     exact Kernel.measurable_kernel_prod_mk_left
-      (measurableSet_eq_fun (Kernel.measurable_rnDeriv _ _).ennreal_toReal measurable_const)
+      (measurableSet_eq_fun (κ.measurable_rnDeriv η).ennreal_toReal measurable_const)
   · refine eventually_of_forall (fun x ↦ ?_)
     simp only [norm_eq_abs, ENNReal.abs_toReal, ENNReal.toReal_le_toReal
     (measure_ne_top _ _) (lt_top_iff_ne_top.mp hC_finite)]
@@ -866,7 +857,7 @@ Consider the following conditions:
 3.a `∀ᵐ x ∂μ, Integrable (fun b ↦ ((∂κ x/∂η x) b).toReal ^ a) (η x)` (`h_int`)
 3.b `∀ᵐ x ∂μ, (κ x) ≪ (η x)` (`h_ac`)
 3.c `Integrable (fun x ↦ ∫ b, ((∂κ x/∂η x) b).toReal ^ a ∂η x) μ` (`h_int'`)
-4. `condHellingerDiv a κ η μ = (a - 1)⁻¹ * ∫ x, ∫ b, ((∂κ x/∂η x) b).toReal ^ a ∂η x ∂μ - (a - 1)⁻¹ * ((μ ⊗ₘ η) Set.univ).toReal`
+4. `condHellingerDiv a κ η μ = (a - 1)⁻¹ * ∫ x, ∫ b, ((∂κ x/∂η x) b).toReal ^ a ∂η x ∂μ - (a - 1)⁻¹ * ((μ ⊗ₘ η) .univ).toReal`
 
 Then the following hold:
 - 1. ↔ 2. (`condHellingerDiv_eq_integral_iff_ne_top`)
@@ -1109,19 +1100,19 @@ lemma condHellingerDiv_eq_integral'_of_one_lt (ha : 1 < a)
     (h_ac : ∀ᵐ x ∂μ, (κ x) ≪ (η x))
     (h_int' : Integrable (fun x ↦ ∫ b, ((∂κ x/∂η x) b).toReal ^ a ∂η x) μ) :
     condHellingerDiv a κ η μ = (a - 1)⁻¹ * ∫ x, ∫ b, ((∂κ x/∂η x) b).toReal ^ a ∂η x ∂μ
-      - (a - 1)⁻¹ * ((μ ⊗ₘ η) Set.univ).toReal := by
+      - (a - 1)⁻¹ * ((μ ⊗ₘ η) .univ).toReal := by
   rw [condHellingerDiv_eq_integral_iff_of_one_lt ha |>.mpr ⟨h_int, h_ac, h_int'⟩]
   norm_cast
   calc
     _ = ∫ x, ((a - 1)⁻¹ * ∫ b, ((∂κ x/∂η x) b).toReal ^ a ∂η x
-        - (a - 1)⁻¹ * ((η x) Set.univ).toEReal).toReal ∂μ := by
+        - (a - 1)⁻¹ * ((η x) .univ).toEReal).toReal ∂μ := by
       apply integral_congr_ae
       filter_upwards [h_int, h_ac] with x hx_int hx_ac
       congr
       exact hellingerDiv_eq_integral_of_ne_top' (by positivity) ha.ne.symm <|
         hellingerDiv_ne_top_iff_of_one_lt ha _ _ |>.mpr ⟨hx_int, hx_ac⟩
     _ = ∫ x, ((a - 1)⁻¹ * ∫ b, ((∂κ x/∂η x) b).toReal ^ a ∂η x
-        - (a - 1)⁻¹ * ((η x) Set.univ).toReal) ∂μ := by
+        - (a - 1)⁻¹ * ((η x) .univ).toReal) ∂μ := by
       refine integral_congr_ae (eventually_of_forall fun x ↦ ?_)
       dsimp
       rw [EReal.toReal_sub (ne_of_beq_false (by rfl)) (ne_of_beq_false (by rfl))]
@@ -1133,9 +1124,9 @@ lemma condHellingerDiv_eq_integral'_of_one_lt (ha : 1 < a)
           EReal.coe_ennreal_pos, Measure.measure_univ_pos, EReal.coe_pos,
           EReal.coe_ennreal_eq_top_iff, measure_ne_top, or_self, not_false_eq_true]
     _ = ∫ x, ((a - 1)⁻¹ * ∫ b, ((∂κ x/∂η x) b).toReal ^ a ∂η x) ∂μ
-        - ∫ x, ((a - 1)⁻¹ * ((η x) Set.univ).toReal) ∂μ :=
+        - ∫ x, ((a - 1)⁻¹ * ((η x) .univ).toReal) ∂μ :=
       integral_sub (Integrable.const_mul h_int' _)
-        (Integrable.const_mul (Integrable.Kernel _ MeasurableSet.univ) _)
+        (Integrable.const_mul (Integrable.Kernel _ .univ) _)
     _ = _ := by
       rw [integral_mul_left, integral_mul_left, compProd_univ_toReal]
 
@@ -1145,7 +1136,7 @@ lemma condHellingerDiv_eq_integral'_of_one_lt' (ha : 1 < a)
     (h_ac : ∀ᵐ x ∂μ, (κ x) ≪ (η x))
     (h_int' : Integrable (fun x ↦ ∫ b, ((∂κ x/∂η x) b).toReal ^ a ∂η x) μ) :
     condHellingerDiv a κ η μ = (a - 1)⁻¹ * ∫ x, ∫ b, ((∂κ x/∂η x) b).toReal ^ a ∂η x ∂μ
-      - (a - 1)⁻¹ * (μ Set.univ).toReal := by
+      - (a - 1)⁻¹ * (μ .univ).toReal := by
   simp_rw [condHellingerDiv_eq_integral'_of_one_lt ha h_int h_ac h_int',
     compProd_univ_toReal, measure_univ, ENNReal.one_toReal, integral_const, smul_eq_mul, mul_one]
 
@@ -1163,18 +1154,18 @@ lemma condHellingerDiv_eq_integral'_of_lt_one (ha_pos : 0 < a) (ha : a < 1)
     [IsFiniteMeasure μ] [IsFiniteKernel κ] [IsFiniteKernel η]
     (h_int' : Integrable (fun x ↦ ∫ b, ((∂κ x/∂η x) b).toReal ^ a ∂η x) μ) :
     condHellingerDiv a κ η μ = (a - 1)⁻¹ * ∫ x, ∫ b, ((∂κ x/∂η x) b).toReal ^ a ∂η x ∂μ
-      - (a - 1)⁻¹ * ((μ ⊗ₘ η) Set.univ).toReal := by
+      - (a - 1)⁻¹ * ((μ ⊗ₘ η) .univ).toReal := by
   rw [condHellingerDiv_eq_integral_iff_of_lt_one ha_pos ha |>.mpr h_int']
   norm_cast
   calc
     _ = ∫ x, ((a - 1)⁻¹ * ∫ b, ((∂κ x/∂η x) b).toReal ^ a ∂η x
-        - (a - 1)⁻¹ * ((η x) Set.univ).toEReal).toReal ∂μ := by
+        - (a - 1)⁻¹ * ((η x) .univ).toEReal).toReal ∂μ := by
       apply integral_congr_ae
       filter_upwards with x
       congr
       exact hellingerDiv_eq_integral_of_lt_one' ha_pos ha _ _
     _ = ∫ x, ((a - 1)⁻¹ * ∫ b, ((∂κ x/∂η x) b).toReal ^ a ∂η x --from here to the end the proof is the same as the one of `condHellingerDiv_eq_integral'_of_one_lt`, consider separating this part as a lemma
-        - (a - 1)⁻¹ * ((η x) Set.univ).toReal) ∂μ := by
+        - (a - 1)⁻¹ * ((η x) .univ).toReal) ∂μ := by
       refine integral_congr_ae (eventually_of_forall fun x ↦ ?_)
       dsimp
       rw [EReal.toReal_sub (ne_of_beq_false (by rfl)) (ne_of_beq_false (by rfl))]
@@ -1186,9 +1177,9 @@ lemma condHellingerDiv_eq_integral'_of_lt_one (ha_pos : 0 < a) (ha : a < 1)
           EReal.coe_ennreal_pos, Measure.measure_univ_pos, EReal.coe_pos,
           EReal.coe_ennreal_eq_top_iff, measure_ne_top, or_self, not_false_eq_true]
     _ = ∫ x, ((a - 1)⁻¹ * ∫ b, ((∂κ x/∂η x) b).toReal ^ a ∂η x) ∂μ
-        - ∫ x, ((a - 1)⁻¹ * ((η x) Set.univ).toReal) ∂μ :=
+        - ∫ x, ((a - 1)⁻¹ * ((η x) .univ).toReal) ∂μ :=
       integral_sub (Integrable.const_mul h_int' _)
-        (Integrable.const_mul (Integrable.Kernel _ MeasurableSet.univ) _)
+        (Integrable.const_mul (Integrable.Kernel _ .univ) _)
     _ = _ := by
       rw [integral_mul_left, integral_mul_left, compProd_univ_toReal]
 
@@ -1196,7 +1187,7 @@ lemma condHellingerDiv_eq_integral'_of_lt_one' (ha_pos : 0 < a) (ha : a < 1)
     [IsFiniteMeasure μ] [IsFiniteKernel κ] [IsMarkovKernel η]
     (h_int' : Integrable (fun x ↦ ∫ b, ((∂κ x/∂η x) b).toReal ^ a ∂η x) μ) :
     condHellingerDiv a κ η μ = (a - 1)⁻¹ * ∫ x, ∫ b, ((∂κ x/∂η x) b).toReal ^ a ∂η x ∂μ
-      - (a - 1)⁻¹ * (μ Set.univ).toReal := by
+      - (a - 1)⁻¹ * (μ .univ).toReal := by
   simp_rw [condHellingerDiv_eq_integral'_of_lt_one ha_pos ha h_int', compProd_univ_toReal,
     measure_univ, ENNReal.one_toReal, integral_const, smul_eq_mul, mul_one]
 
diff --git a/TestingLowerBounds/Divergences/KullbackLeibler.lean b/TestingLowerBounds/Divergences/KullbackLeibler.lean
index 68a1d4f6..1d87efd4 100644
--- a/TestingLowerBounds/Divergences/KullbackLeibler.lean
+++ b/TestingLowerBounds/Divergences/KullbackLeibler.lean
@@ -143,12 +143,12 @@ lemma kl_ne_bot (μ ν : Measure α) : kl μ ν ≠ ⊥ := by
 
 lemma kl_ge_mul_log' [IsFiniteMeasure μ] [IsProbabilityMeasure ν]
     (hμν : μ ≪ ν) :
-    (μ Set.univ).toReal * log (μ Set.univ).toReal ≤ kl μ ν :=
+    (μ .univ).toReal * log (μ .univ).toReal ≤ kl μ ν :=
   (le_fDiv_of_ac convexOn_mul_log continuous_mul_log.continuousOn hμν).trans_eq
     kl_eq_fDiv.symm
 
 lemma kl_ge_mul_log (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
-    (μ Set.univ).toReal * log ((μ Set.univ).toReal / (ν Set.univ).toReal) ≤ kl μ ν := by
+    (μ .univ).toReal * log ((μ .univ).toReal / (ν .univ).toReal) ≤ kl μ ν := by
   by_cases hμν : μ ≪ ν
   swap; · simp [hμν]
   by_cases h_int : Integrable (llr μ ν) μ
@@ -161,7 +161,7 @@ lemma kl_ge_mul_log (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure 
   · refine absurd ?_ hμ
     rw [hν] at hμν
     exact Measure.absolutelyContinuous_zero_iff.mp hμν
-  let ν' := (ν Set.univ)⁻¹ • ν
+  let ν' := (ν .univ)⁻¹ • ν
   have : IsProbabilityMeasure ν' := by
     constructor
     simp only [ν', Measure.coe_smul, Pi.smul_apply, smul_eq_mul]
@@ -172,11 +172,11 @@ lemma kl_ge_mul_log (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure 
     refine Measure.AbsolutelyContinuous.trans hμν (Measure.absolutelyContinuous_smul ?_)
     simp [measure_ne_top ν]
   have h := kl_ge_mul_log' hμν'
-  rw [kl_of_ac_of_integrable hμν', integral_congr_ae (llr_smul_right hμν (ν Set.univ)⁻¹ _ _)] at h
+  rw [kl_of_ac_of_integrable hμν', integral_congr_ae (llr_smul_right hμν (ν .univ)⁻¹ _ _)] at h
   rotate_left
   · simp [measure_ne_top ν _]
   · simp [hν]
-  · rw [integrable_congr (llr_smul_right hμν (ν Set.univ)⁻¹ _ _)]
+  · rw [integrable_congr (llr_smul_right hμν (ν .univ)⁻¹ _ _)]
     rotate_left
     · simp [measure_ne_top ν _]
     · simp [hν]
@@ -191,14 +191,14 @@ lemma kl_ge_mul_log (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure 
     simp [hν, measure_ne_top ν]
 
 lemma kl_nonneg' (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
-    (h : μ Set.univ ≥ ν Set.univ) :
+    (h : μ .univ ≥ ν .univ) :
     0 ≤ kl μ ν := by
   by_cases hμν : μ ≪ ν
   swap; · rw [kl_of_not_ac hμν]; simp
   by_cases h_int : Integrable (llr μ ν) μ
   swap; · rw [kl_of_not_integrable h_int]; simp
   calc 0
-    ≤ ((μ Set.univ).toReal : EReal) * log ((μ Set.univ).toReal / (ν Set.univ).toReal) := by
+    ≤ ((μ .univ).toReal : EReal) * log ((μ .univ).toReal / (ν .univ).toReal) := by
         by_cases h_zero : NeZero ν
         swap; · simp [not_neZero.mp h_zero]
         refine mul_nonneg (EReal.coe_nonneg.mpr ENNReal.toReal_nonneg) ?_
@@ -216,7 +216,7 @@ lemma kl_nonneg (μ ν : Measure α) [IsProbabilityMeasure μ] [IsProbabilityMea
 
 /-- **Converse Gibbs' inequality**: the Kullback-Leibler divergence between two finite measures is
 zero if and only if the two distributions are equal. -/
-lemma kl_eq_zero_iff [IsFiniteMeasure μ] [IsFiniteMeasure ν] (h_mass : μ Set.univ = ν Set.univ) :
+lemma kl_eq_zero_iff [IsFiniteMeasure μ] [IsFiniteMeasure ν] (h_mass : μ .univ = ν .univ) :
     kl μ ν = 0 ↔ μ = ν :=
   kl_eq_fDiv (μ := μ) (ν := ν) ▸ fDiv_eq_zero_iff h_mass derivAtTop_mul_log
     Real.strictConvexOn_mul_log Real.continuous_mul_log.continuousOn (by norm_num)
@@ -407,7 +407,7 @@ lemma condKL_nonneg (κ η : Kernel α β) [IsMarkovKernel κ] [IsMarkovKernel 
 
 @[simp]
 lemma condKL_const {ξ : Measure β} [IsFiniteMeasure ξ] [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
-    condKL (Kernel.const β μ) (Kernel.const β ν) ξ = (kl μ ν) * ξ Set.univ := by
+    condKL (Kernel.const β μ) (Kernel.const β ν) ξ = (kl μ ν) * ξ .univ := by
   rw [condKL_eq_condFDiv, kl_eq_fDiv]
   exact condFDiv_const convexOn_mul_log
 
@@ -447,22 +447,22 @@ lemma condKL_compProd_meas_eq_top [CountableOrCountablyGenerated (α × β) γ]
     {ξ : Kernel α β} [IsSFiniteKernel ξ] {κ η : Kernel (α × β) γ}
     [IsMarkovKernel κ] [IsMarkovKernel η] :
     condKL κ η (μ ⊗ₘ ξ) = ⊤
-      ↔ ¬ (∀ᵐ a ∂μ, condKL (Kernel.snd' κ a) (Kernel.snd' η a) (ξ a) ≠ ⊤)
-        ∨ ¬ Integrable (fun x ↦ (condKL (Kernel.snd' κ x) (Kernel.snd' η x) (ξ x)).toReal) μ := by
+      ↔ ¬ (∀ᵐ a ∂μ, condKL (κ.snd' a) (η.snd' a) (ξ a) ≠ ⊤)
+        ∨ ¬ Integrable (fun x ↦ (condKL (κ.snd' x) (η.snd' x) (ξ x)).toReal) μ := by
   rw [condKL_eq_top_iff]
   have h_ae_eq (h_ae : ∀ᵐ a ∂μ, ∀ᵐ b ∂ξ a, κ (a, b) ≪ η (a, b))
       (h_int : ∀ᵐ a ∂μ, ∀ᵐ b ∂ξ a, Integrable (llr (κ (a, b)) (η (a, b))) (κ (a, b))) :
-      (fun x ↦ (condKL (Kernel.snd' κ x) (Kernel.snd' η x) (ξ x)).toReal)
+      (fun x ↦ (condKL (κ.snd' x) (η.snd' x) (ξ x)).toReal)
         =ᵐ[μ] fun a ↦ ∫ b, (kl (κ (a, b)) (η (a, b))).toReal ∂ξ a := by
     filter_upwards [h_ae, h_int] with a ha_ae ha_int
     rw [condKL_toReal_of_ae_ac_of_ae_integrable]
     · simp only [Kernel.snd'_apply]
-    · filter_upwards [ha_ae] with b hb using Kernel.snd'_apply _ _ _ ▸ hb
-    · filter_upwards [ha_int] with b hb using Kernel.snd'_apply _ _ _ ▸ hb
+    · filter_upwards [ha_ae] with b hb using κ.snd'_apply _ _ ▸ hb
+    · filter_upwards [ha_int] with b hb using κ.snd'_apply _ _ ▸ hb
   constructor
   · by_cases h_ae : ∀ᵐ x ∂(μ ⊗ₘ ξ), κ x ≪ η x
     swap
-    · rw [Measure.ae_compProd_iff (Kernel.measurableSet_absolutelyContinuous _ _)] at h_ae
+    · rw [Measure.ae_compProd_iff (κ.measurableSet_absolutelyContinuous _)] at h_ae
       simp_rw [condKL_ne_top_iff, Kernel.snd'_apply, eventually_and, not_and_or]
       intro; left; left
       exact h_ae
@@ -485,7 +485,7 @@ lemma condKL_compProd_meas_eq_top [CountableOrCountablyGenerated (α × β) γ]
       simp only [condKL_ne_top_iff, Kernel.snd'_apply] at ha_int2
       exact ha_int2.2.2
     right
-    rw [Measure.ae_compProd_iff (Kernel.measurableSet_absolutelyContinuous _ _)] at h_ae
+    rw [Measure.ae_compProd_iff (κ.measurableSet_absolutelyContinuous _)] at h_ae
     apply Integrable.congr.mt
     swap; exact fun a ↦ ∫ b, (kl (κ (a, b)) (η (a, b))).toReal ∂(ξ a)
     push_neg
@@ -500,7 +500,7 @@ lemma condKL_compProd_meas_eq_top [CountableOrCountablyGenerated (α × β) γ]
     contrapose! h
     obtain ⟨h_ae, ⟨h_int1, h_int2⟩⟩ := h
     rw [ae_compProd_integrable_llr_iff h_ae] at h_int1
-    rw [Measure.ae_compProd_iff (Kernel.measurableSet_absolutelyContinuous _ _)] at h_ae
+    rw [Measure.ae_compProd_iff (κ.measurableSet_absolutelyContinuous _)] at h_ae
     have h_meas := (Integrable.integral_compProd' h_int2).aestronglyMeasurable
     rw [Measure.integrable_compProd_iff h_int2.aestronglyMeasurable] at h_int2
     constructor
@@ -524,7 +524,7 @@ lemma condKL_compProd_meas_eq_top [CountableOrCountablyGenerated (α × β) γ]
 lemma condKL_compProd_meas [CountableOrCountablyGenerated (α × β) γ] [SFinite μ] {ξ : Kernel α β}
     [IsSFiniteKernel ξ] {κ η : Kernel (α × β) γ} [IsMarkovKernel κ] [IsMarkovKernel η]
     (h : condKL κ η (μ ⊗ₘ ξ) ≠ ⊤) :
-    condKL κ η (μ ⊗ₘ ξ) = ∫ x, (condKL (Kernel.snd' κ x) (Kernel.snd' η x) (ξ x)).toReal ∂μ := by
+    condKL κ η (μ ⊗ₘ ξ) = ∫ x, (condKL (κ.snd' x) (η.snd' x) (ξ x)).toReal ∂μ := by
   rw [condKL_ne_top_iff'.mp h, Measure.integral_compProd (condKL_ne_top_iff.mp h).2.2]
   replace h := condKL_compProd_meas_eq_top.mpr.mt h
   push_neg at h
@@ -571,29 +571,28 @@ lemma kl_compProd [CountableOrCountablyGenerated α β] [IsMarkovKernel κ] [IsM
         condKL_ne_bot, condKL_of_not_integrable', EReal.add_top_of_ne_bot, kl_ne_bot,
         condKL_of_not_ae_integrable]
   have intμν := integrable_llr_of_integrable_llr_compProd h_prod h_int
-  have intκη : Integrable (fun a ↦ ∫ (x : β), log (Kernel.rnDeriv κ η a x).toReal ∂κ a) μ := by
+  have intκη : Integrable (fun a ↦ ∫ (x : β), log (κ.rnDeriv η a x).toReal ∂κ a) μ := by
     apply Integrable.congr (integrable_integral_llr_of_integrable_llr_compProd h_prod h_int)
     filter_upwards [hκη] with a ha
     apply integral_congr_ae
-    filter_upwards [ha.ae_le (Kernel.rnDeriv_eq_rnDeriv_measure κ η a)] with x hx
+    filter_upwards [ha.ae_le (κ.rnDeriv_eq_rnDeriv_measure η a)] with x hx
     rw [hx, llr_def]
   have intκη2 := ae_integrable_llr_of_integrable_llr_compProd h_prod h_int
   calc kl (μ ⊗ₘ κ) (ν ⊗ₘ η) = ∫ p, llr (μ ⊗ₘ κ) (ν ⊗ₘ η) p ∂(μ ⊗ₘ κ) :=
     kl_of_ac_of_integrable h_prod h_int
   _ = ∫ a, ∫ x, llr (μ ⊗ₘ κ) (ν ⊗ₘ η) (a, x) ∂κ a ∂μ := mod_cast Measure.integral_compProd h_int
-  _ = ∫ a, ∫ x, log (μ.rnDeriv ν a).toReal
-      + log (Kernel.rnDeriv κ η a x).toReal ∂κ a ∂μ := by
+  _ = ∫ a, ∫ x, log (μ.rnDeriv ν a).toReal + log (κ.rnDeriv η a x).toReal ∂κ a ∂μ := by
     norm_cast
     have h := hμν.ae_le (Measure.ae_ae_of_ae_compProd (Kernel.rnDeriv_measure_compProd μ ν κ η))
     apply Kernel.integral_congr_ae₂
     filter_upwards [h, hκη, Measure.rnDeriv_toReal_pos hμν] with a ha hκηa hμν_pos
     have hμν_zero : (μ.rnDeriv ν a).toReal ≠ 0 := by linarith
     filter_upwards [Kernel.rnDeriv_toReal_pos hκηa, hκηa.ae_le ha] with x hκη_pos hx
-    have hκη_zero : (Kernel.rnDeriv κ η a x).toReal ≠ 0 := by linarith
+    have hκη_zero : (κ.rnDeriv η a x).toReal ≠ 0 := by linarith
     rw [llr, hx, ENNReal.toReal_mul]
     exact log_mul hμν_zero hκη_zero
   _ = ∫ a, ∫ _, log (μ.rnDeriv ν a).toReal ∂κ a ∂μ
-      + ∫ a, ∫ x, log (Kernel.rnDeriv κ η a x).toReal ∂κ a ∂μ := by
+      + ∫ a, ∫ x, log (κ.rnDeriv η a x).toReal ∂κ a ∂μ := by
     norm_cast
     rw [← integral_add']
     simp only [Pi.add_apply]
@@ -603,7 +602,7 @@ lemma kl_compProd [CountableOrCountablyGenerated α β] [IsMarkovKernel κ] [IsM
     · exact intκη
     apply integral_congr_ae
     filter_upwards [hκη, intκη2] with a ha hκηa
-    have h := ha.ae_le (Kernel.rnDeriv_eq_rnDeriv_measure κ η a)
+    have h := ha.ae_le (κ.rnDeriv_eq_rnDeriv_measure η a)
     rw [← integral_add']
     rotate_left
     · simp only [integrable_const]
@@ -619,7 +618,7 @@ lemma kl_compProd [CountableOrCountablyGenerated α β] [IsMarkovKernel κ] [IsM
     congr 2
     apply Kernel.integral_congr_ae₂
     filter_upwards [hκη] with a ha
-    have h := ha.ae_le (Kernel.rnDeriv_eq_rnDeriv_measure κ η a)
+    have h := ha.ae_le (κ.rnDeriv_eq_rnDeriv_measure η a)
     filter_upwards [h] with x hx
     congr
   _ = kl μ ν + condKL κ η μ := by
@@ -630,7 +629,7 @@ lemma kl_compProd [CountableOrCountablyGenerated α β] [IsMarkovKernel κ] [IsM
       simp_rw [llr_def]
       apply Integrable.congr intκη
       filter_upwards [hκη] with a ha
-      have h := ha.ae_le (Kernel.rnDeriv_eq_rnDeriv_measure κ η a)
+      have h := ha.ae_le (κ.rnDeriv_eq_rnDeriv_measure η a)
       apply integral_congr_ae
       filter_upwards [h] with x hx
       rw [hx]
@@ -672,13 +671,13 @@ lemma kl_compProd_kernel_of_ae_ac_of_ae_integrable [CountableOrCountablyGenerate
   simp only [Kernel.absolutelyContinuous_compProd_iff, eventually_and] at h_ac
   filter_upwards [h_ac.1, h_ac.2, h_ae_int.1, h_ae_int.2.1, h_ae_int.2.2] with a ha_ac₁ ha_ac₂
     ha_int₁ ha_int_kl₂ ha_int₂
-  have h_snd_ne_top : condKL (Kernel.snd' κ₂ a) (Kernel.snd' η₂ a) (κ₁ a) ≠ ⊤ := by
+  have h_snd_ne_top : condKL (κ₂.snd' a) (η₂.snd' a) (κ₁ a) ≠ ⊤ := by
     apply condKL_ne_top_iff.mpr
     simp_rw [Kernel.snd'_apply]
     exact ⟨ha_ac₂, ⟨ha_int₂, ha_int_kl₂⟩⟩
   simp_rw [Kernel.compProd_apply_eq_compProd_snd', kl_compProd,
     EReal.toReal_add (kl_ne_top_iff.mpr ⟨ha_ac₁, ha_int₁⟩) (kl_ne_bot (κ₁ a) (η₁ a)) h_snd_ne_top
-    (condKL_ne_bot (Kernel.snd' κ₂ a) (Kernel.snd' η₂ a) (κ₁ a)),
+    (condKL_ne_bot (κ₂.snd' a) (η₂.snd' a) (κ₁ a)),
     condKL_ne_top_iff'.mp h_snd_ne_top, EReal.toReal_coe, Kernel.snd'_apply]
 
 lemma condKL_compProd_kernel_eq_top [CountableOrCountablyGenerated (α × β) γ] {κ₁ η₁ : Kernel α β}
@@ -691,14 +690,13 @@ lemma condKL_compProd_kernel_eq_top [CountableOrCountablyGenerated (α × β) γ
     simp only [condKL_isEmpty_left]
     tauto
   have := countableOrCountablyGenerated_right_of_prod_left_of_nonempty (α := α) (β := β) (γ := γ)
-  simp_rw [condKL_eq_top_iff,
-    Measure.ae_compProd_iff (Kernel.measurableSet_absolutelyContinuous _ _)]
+  simp_rw [condKL_eq_top_iff, Measure.ae_compProd_iff (κ₂.measurableSet_absolutelyContinuous _)]
   by_cases h_ac : ∀ᵐ a ∂μ, (κ₁ ⊗ₖ κ₂) a ≪ (η₁ ⊗ₖ η₂) a
     <;> have h_ac' := h_ac
     <;> simp only [Kernel.absolutelyContinuous_compProd_iff, eventually_and, not_and_or] at h_ac'
     <;> simp only [h_ac, h_ac', not_false_eq_true, true_or, not_true, true_iff, false_or]
   swap; tauto
-  rw [← Measure.ae_compProd_iff (Kernel.measurableSet_absolutelyContinuous _ _)] at h_ac'
+  rw [← Measure.ae_compProd_iff (κ₂.measurableSet_absolutelyContinuous _)] at h_ac'
   by_cases h_ae_int : ∀ᵐ a ∂μ, Integrable (llr ((κ₁ ⊗ₖ κ₂) a) ((η₁ ⊗ₖ η₂) a)) ((κ₁ ⊗ₖ κ₂) a)
     <;> have h_ae_int' := h_ae_int
     <;> simp only [eventually_congr (h_ac.mono (fun a h ↦ (Kernel.integrable_llr_compProd_iff' a h))),
@@ -757,7 +755,7 @@ variable {β : Type*} {mβ : MeasurableSpace β}
 
 lemma kl_prod_two' [CountableOrCountablyGenerated α β] {ξ ψ : Measure β} [IsProbabilityMeasure ξ]
     [IsProbabilityMeasure ψ] [IsFiniteMeasure μ] [IsFiniteMeasure ν]:
-    kl (μ.prod ξ) (ν.prod ψ) = kl μ ν + kl ξ ψ * (μ Set.univ) := by
+    kl (μ.prod ξ) (ν.prod ψ) = kl μ ν + kl ξ ψ * (μ .univ) := by
   simp only [← condKL_const, ← kl_compProd, Measure.compProd_const]
 
 /--Tensorization property for KL divergence-/
@@ -783,7 +781,7 @@ lemma Measure.pi_map_piCongrLeft {ι ι' : Type*} [hι : Fintype ι] [hι' : Fin
   refine Measure.pi_eq (fun s _ ↦ ?_) |>.symm
   rw [e_meas.measurableEmbedding.map_apply]
   let s' : (i : ι) → Set (β (e i)) := fun i ↦ s (e i)
-  have : e_meas ⁻¹' Set.pi Set.univ s = Set.pi Set.univ s' := by
+  have : e_meas ⁻¹' Set.univ.pi s = Set.univ.pi s' := by
     ext x
     simp only [Set.mem_preimage, Set.mem_pi, Set.mem_univ, forall_true_left, s']
     refine (e.forall_congr ?_).symm
diff --git a/TestingLowerBounds/Divergences/Renyi.lean b/TestingLowerBounds/Divergences/Renyi.lean
index 2c2cbd90..0b15a867 100644
--- a/TestingLowerBounds/Divergences/Renyi.lean
+++ b/TestingLowerBounds/Divergences/Renyi.lean
@@ -79,7 +79,7 @@ Hellinger divergence to the Rényi divergence. -/
 
 noncomputable def renyiDiv (a : ℝ) (μ ν : Measure α) : EReal :=
   if a = 1 then kl μ ν
-  else (a - 1)⁻¹ * ENNReal.log ((↑(ν Set.univ) + (a - 1) * (hellingerDiv a μ ν)).toENNReal)
+  else (a - 1)⁻¹ * ENNReal.log ((↑(ν .univ) + (a - 1) * (hellingerDiv a μ ν)).toENNReal)
 
 @[simp]
 lemma renyiDiv_zero (μ ν : Measure α) [SigmaFinite μ] [IsFiniteMeasure ν] :
@@ -99,7 +99,7 @@ lemma renyiDiv_one (μ ν : Measure α) : renyiDiv 1 μ ν = kl μ ν := by
 
 lemma renyiDiv_of_ne_one (ha_ne_one : a ≠ 1) (μ ν : Measure α) :
     renyiDiv a μ ν
-      = (a - 1)⁻¹ * ENNReal.log ((↑(ν Set.univ) + (a - 1) * (hellingerDiv a μ ν)).toENNReal) := by
+      = (a - 1)⁻¹ * ENNReal.log ((↑(ν .univ) + (a - 1) * (hellingerDiv a μ ν)).toENNReal) := by
   rw [renyiDiv, if_neg ha_ne_one]
 
 @[simp]
@@ -312,7 +312,7 @@ lemma renyiDiv_eq_log_integral' (ha_pos : 0 < a) (ha : a ≠ 1) [IsFiniteMeasure
 
 end IntegralForm
 
-lemma renyiDiv_symm' (ha_pos : 0 < a) (ha : a < 1) (h_eq : μ Set.univ = ν Set.univ)
+lemma renyiDiv_symm' (ha_pos : 0 < a) (ha : a < 1) (h_eq : μ .univ = ν .univ)
     [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
     (1 - a) * renyiDiv a μ ν = a * renyiDiv (1 - a) ν μ := by
   rw [renyiDiv_of_ne_one ha.ne, renyiDiv_of_ne_one (by linarith)]
@@ -491,7 +491,7 @@ lemma condRenyiDiv_of_ne_zero [CountableOrCountablyGenerated α β] (ha_nonneg :
     (ha_ne_one : a ≠ 1) (κ η : Kernel α β) (μ : Measure α) [IsFiniteKernel κ] [∀ x, NeZero (κ x)]
     [IsFiniteKernel η] [IsFiniteMeasure μ] :
     condRenyiDiv a κ η μ = (a - 1)⁻¹
-      * ENNReal.log (↑((μ ⊗ₘ η) Set.univ) + (a - 1) * (condHellingerDiv a κ η μ)).toENNReal := by
+      * ENNReal.log (↑((μ ⊗ₘ η) .univ) + (a - 1) * (condHellingerDiv a κ η μ)).toENNReal := by
   rw [condRenyiDiv, renyiDiv_of_ne_one ha_ne_one, hellingerDiv_compProd_left ha_nonneg _]
 
 end TopAndBounds
@@ -505,7 +505,7 @@ variable {β : Type*} {mβ : MeasurableSpace β} {κ η : Kernel α β}
 
 lemma le_renyiDiv_of_le_hellingerDiv {a : ℝ} {μ₁ ν₁ : Measure α} {μ₂ ν₂ : Measure β}
     [SigmaFinite μ₁] [SigmaFinite ν₁] [SigmaFinite μ₂] [SigmaFinite ν₂]
-    (h_eq : ν₁ Set.univ = ν₂ Set.univ) (h_le : hellingerDiv a μ₁ ν₁ ≤ hellingerDiv a μ₂ ν₂) :
+    (h_eq : ν₁ .univ = ν₂ .univ) (h_le : hellingerDiv a μ₁ ν₁ ≤ hellingerDiv a μ₂ ν₂) :
     renyiDiv a μ₁ ν₁ ≤ renyiDiv a μ₂ ν₂ := by
   rcases lt_trichotomy a 1 with (ha | rfl | ha)
   · simp_rw [renyiDiv_of_ne_one ha.ne, h_eq]
@@ -514,7 +514,7 @@ lemma le_renyiDiv_of_le_hellingerDiv {a : ℝ} {μ₁ ν₁ : Measure α} {μ₂
     gcongr
     · simp only [EReal.coe_nonneg, inv_nonneg, sub_nonneg, ha.le]
     refine ENNReal.log_monotone <| EReal.toENNReal_le_toENNReal ?_
-    gcongr (ν₂ Set.univ) + ?_
+    gcongr (ν₂ .univ) + ?_
     apply EReal.neg_le_neg_iff.mp
     norm_cast
     simp_rw [← neg_mul, ← EReal.coe_neg, neg_sub]
@@ -536,7 +536,7 @@ lemma le_renyiDiv_compProd [CountableOrCountablyGenerated α β] (ha_pos : 0 < a
     (κ η : Kernel α β) [IsMarkovKernel κ] [IsMarkovKernel η] :
     renyiDiv a μ ν ≤ renyiDiv a (μ ⊗ₘ κ) (ν ⊗ₘ η) := by
   refine le_renyiDiv_of_le_hellingerDiv ?_ (le_hellingerDiv_compProd ha_pos μ ν κ η)
-  rw [Measure.compProd_apply MeasurableSet.univ]
+  rw [Measure.compProd_apply .univ]
   simp
 
 lemma renyiDiv_fst_le [Nonempty β] [StandardBorelSpace β] (ha_pos : 0 < a)
@@ -570,7 +570,7 @@ lemma renyiDiv_comp_right_le [Nonempty α] [StandardBorelSpace α] (ha_pos : 0 <
     (κ : Kernel α β) [IsMarkovKernel κ] :
     renyiDiv a (κ ∘ₘ μ) (κ ∘ₘ ν) ≤ renyiDiv a μ ν := by
   refine le_renyiDiv_of_le_hellingerDiv ?_ (hellingerDiv_comp_right_le ha_pos μ ν κ)
-  rw [← Measure.snd_compProd ν κ, Measure.snd_univ, Measure.compProd_apply MeasurableSet.univ]
+  rw [← Measure.snd_compProd ν κ, Measure.snd_univ, Measure.compProd_apply .univ]
   simp
 
 end DataProcessingInequality
diff --git a/TestingLowerBounds/Divergences/StatInfo.lean b/TestingLowerBounds/Divergences/StatInfo.lean
index 77af1d48..21868b64 100644
--- a/TestingLowerBounds/Divergences/StatInfo.lean
+++ b/TestingLowerBounds/Divergences/StatInfo.lean
@@ -83,7 +83,7 @@ lemma statInfo_of_measure_false_eq_zero (μ ν : Measure 𝒳) (hπ : π {false}
 lemma statInfo_comp_le (μ ν : Measure 𝒳) (π : Measure Bool) (η : Kernel 𝒳 𝒳') [IsMarkovKernel η] :
     statInfo (η ∘ₘ μ) (η ∘ₘ ν) π ≤ statInfo μ ν π := by
   refine tsub_le_tsub ?_ (bayesBinaryRisk_le_bayesBinaryRisk_comp _ _ _ _)
-  simp [Measure.bind_apply MeasurableSet.univ (Kernel.measurable _)]
+  simp [Measure.bind_apply .univ (Kernel.measurable _)]
 
 lemma toReal_statInfo_eq_toReal_sub [IsFiniteMeasure ν] [IsFiniteMeasure π] :
     (statInfo μ ν π).toReal = (min (π {false} * μ univ) (π {true} * ν univ)).toReal
@@ -940,7 +940,7 @@ lemma fDiv_eq_lintegral_fDiv_statInfoFun_of_mutuallySingular [IsFiniteMeasure μ
       ← lintegral_mul_const _]
     swap
     · simp_rw [derivAtTop_statInfoFun_eq]
-      refine (Measurable.ite (MeasurableSet.const _) ?_ ?_).coe_real_ereal.ereal_toENNReal <;>
+      refine (Measurable.ite (.const _) ?_ ?_).coe_real_ereal.ereal_toENNReal <;>
       · refine Measurable.ite (measurableSet_le (fun _ a ↦ a) ?_) ?_ ?_ <;> exact measurable_const
     rw [← lintegral_add_left]
     swap; · exact measurable_statInfoFun2.ennreal_ofReal.mul_const _
diff --git a/TestingLowerBounds/FDiv/Basic.lean b/TestingLowerBounds/FDiv/Basic.lean
index 5d929d4f..c5001cc4 100644
--- a/TestingLowerBounds/FDiv/Basic.lean
+++ b/TestingLowerBounds/FDiv/Basic.lean
@@ -89,16 +89,16 @@ open Classical in
 noncomputable
 def fDiv (f : ℝ → ℝ) (μ ν : Measure α) : EReal :=
   if ¬ Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν then ⊤
-  else ∫ x, f ((∂μ/∂ν) x).toReal ∂ν + derivAtTop f * μ.singularPart ν Set.univ
+  else ∫ x, f ((∂μ/∂ν) x).toReal ∂ν + derivAtTop f * μ.singularPart ν .univ
 
 lemma fDiv_of_not_integrable (hf : ¬ Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν) :
     fDiv f μ ν = ⊤ := if_pos hf
 
 lemma fDiv_of_integrable (hf : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν) :
-    fDiv f μ ν = ∫ x, f ((∂μ/∂ν) x).toReal ∂ν + derivAtTop f * μ.singularPart ν Set.univ :=
+    fDiv f μ ν = ∫ x, f ((∂μ/∂ν) x).toReal ∂ν + derivAtTop f * μ.singularPart ν .univ :=
   if_neg (not_not.mpr hf)
 
-lemma fDiv_of_mul_eq_top (h : derivAtTop f * μ.singularPart ν Set.univ = ⊤) :
+lemma fDiv_of_mul_eq_top (h : derivAtTop f * μ.singularPart ν .univ = ⊤) :
     fDiv f μ ν = ⊤ := by
   by_cases hf : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν
   · rw [fDiv, if_neg (not_not.mpr hf), h, EReal.coe_add_top]
@@ -153,7 +153,7 @@ lemma fDiv_eq_zero_of_forall_nonneg (μ ν : Measure α) (hf : ∀ x ≥ 0, f x
   exact fun x hx ↦ hf x hx
 
 @[simp]
-lemma fDiv_zero_measure (ν : Measure α) [IsFiniteMeasure ν] : fDiv f 0 ν = f 0 * ν Set.univ := by
+lemma fDiv_zero_measure (ν : Measure α) [IsFiniteMeasure ν] : fDiv f 0 ν = f 0 * ν .univ := by
   have : (fun x ↦ f ((∂0/∂ν) x).toReal) =ᵐ[ν] fun _ ↦ f 0 := by
     filter_upwards [Measure.rnDeriv_zero ν] with x hx
     rw [hx]
@@ -167,12 +167,12 @@ lemma fDiv_zero_measure (ν : Measure α) [IsFiniteMeasure ν] : fDiv f 0 ν = f
     exact integrable_const _
 
 @[simp]
-lemma fDiv_zero_measure_right (μ : Measure α) : fDiv f μ 0 = derivAtTop f * μ Set.univ := by
+lemma fDiv_zero_measure_right (μ : Measure α) : fDiv f μ 0 = derivAtTop f * μ .univ := by
   rw [fDiv_of_integrable] <;> simp
 
 @[simp]
 lemma fDiv_const (c : ℝ) (μ ν : Measure α) [IsFiniteMeasure ν] :
-    fDiv (fun _ ↦ c) μ ν = ν Set.univ * c := by
+    fDiv (fun _ ↦ c) μ ν = ν .univ * c := by
   rw [fDiv_of_integrable (integrable_const c), integral_const]
   simp only [smul_eq_mul, EReal.coe_mul, derivAtTop_const, zero_mul, add_zero]
   congr
@@ -180,10 +180,10 @@ lemma fDiv_const (c : ℝ) (μ ν : Measure α) [IsFiniteMeasure ν] :
   exact measure_ne_top _ _
 
 lemma fDiv_const' {c : ℝ} (hc : 0 ≤ c) (μ ν : Measure α) :
-    fDiv (fun _ ↦ c) μ ν = ν Set.univ * c := by
+    fDiv (fun _ ↦ c) μ ν = ν .univ * c := by
   by_cases hν : IsFiniteMeasure ν
   · exact fDiv_const c μ ν
-  · have : ν Set.univ = ∞ := by
+  · have : ν .univ = ∞ := by
       by_contra h_univ
       exact absurd ⟨Ne.lt_top h_univ⟩ hν
     rw [this]
@@ -212,13 +212,13 @@ lemma fDiv_self (hf_one : f 1 = 0) (μ : Measure α) [SigmaFinite μ] : fDiv f 
 
 @[simp]
 lemma fDiv_id (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν] :
-    fDiv id μ ν = μ Set.univ := by
+    fDiv id μ ν = μ .univ := by
   by_cases h_int : Integrable (fun x ↦ ((∂μ/∂ν) x).toReal) ν
   · rw [fDiv_of_integrable h_int]
     simp only [id_eq, derivAtTop_id, one_mul]
     rw [← integral_univ, Measure.setIntegral_toReal_rnDeriv_eq_withDensity]
-    have h_ne_top : (Measure.withDensity ν (∂μ/∂ν)) Set.univ ≠ ∞ := by
-      rw [withDensity_apply _ MeasurableSet.univ, setLIntegral_univ]
+    have h_ne_top : (Measure.withDensity ν (∂μ/∂ν)) .univ ≠ ∞ := by
+      rw [withDensity_apply _ .univ, setLIntegral_univ]
       rwa [integrable_toReal_iff] at h_int
       · exact (μ.measurable_rnDeriv ν).aemeasurable
       · exact μ.rnDeriv_ne_top ν
@@ -237,7 +237,7 @@ lemma fDiv_id (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν] :
 
 @[simp]
 lemma fDiv_id' (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν] :
-    fDiv (fun x ↦ x) μ ν = μ Set.univ := fDiv_id μ ν
+    fDiv (fun x ↦ x) μ ν = μ .univ := fDiv_id μ ν
 
 lemma fDiv_mul {c : ℝ} (hc : 0 ≤ c) (hf_cvx : ConvexOn ℝ (Ici 0) f)
     (μ ν : Measure α) :
@@ -294,7 +294,7 @@ lemma fDiv_add [IsFiniteMeasure μ] (hf : Integrable (fun x ↦ f ((∂μ/∂ν)
 
 lemma fDiv_add_const (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
     (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (c : ℝ) :
-    fDiv (fun x ↦ f x + c) μ ν = fDiv f μ ν + c * ν Set.univ := by
+    fDiv (fun x ↦ f x + c) μ ν = fDiv f μ ν + c * ν .univ := by
   by_cases hf_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν
   · rw [fDiv_add hf_int (integrable_const _) hf_cvx, fDiv_const, mul_comm]
     exact convexOn_const _ (convex_Ici 0)
@@ -308,7 +308,7 @@ lemma fDiv_add_const (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure
 
 lemma fDiv_sub_const (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
     (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (c : ℝ) :
-    fDiv (fun x ↦ f x - c) μ ν = fDiv f μ ν - c * ν Set.univ := by
+    fDiv (fun x ↦ f x - c) μ ν = fDiv f μ ν - c * ν .univ := by
   have : f = fun x ↦ (f x - c) + c := by ext; simp
   conv_rhs => rw [this]
   rw [fDiv_add_const]
@@ -317,7 +317,7 @@ lemma fDiv_sub_const (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure
 
 lemma fDiv_linear {c : ℝ} [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
     fDiv (fun x ↦ c * (x - 1)) μ ν
-      = c * ((μ Set.univ).toReal - (ν Set.univ).toReal) := by
+      = c * ((μ .univ).toReal - (ν .univ).toReal) := by
   rw [fDiv_mul_of_ne_top]
   rotate_left
   · exact (convexOn_id (convex_Ici 0)).add (convexOn_const _ (convex_Ici 0))
@@ -332,7 +332,7 @@ lemma fDiv_linear {c : ℝ} [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
 lemma fDiv_add_linear' {c : ℝ} [IsFiniteMeasure μ] [IsFiniteMeasure ν]
     (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) :
     fDiv (fun x ↦ f x + c * (x - 1)) μ ν
-      = fDiv f μ ν + c * ((μ Set.univ).toReal - (ν Set.univ).toReal) := by
+      = fDiv f μ ν + c * ((μ .univ).toReal - (ν .univ).toReal) := by
   by_cases hf : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν
   · rw [fDiv_add hf _ hf_cvx _, fDiv_linear]
     · exact (Measure.integrable_toReal_rnDeriv.sub (integrable_const _)).const_mul c
@@ -356,7 +356,7 @@ lemma fDiv_add_linear' {c : ℝ} [IsFiniteMeasure μ] [IsFiniteMeasure ν]
       exact h_int.add ((Measure.integrable_toReal_rnDeriv.sub (integrable_const _)).const_mul c).neg
 
 lemma fDiv_add_linear {c : ℝ} [IsFiniteMeasure μ] [IsFiniteMeasure ν]
-    (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (h_eq : μ Set.univ = ν Set.univ) :
+    (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (h_eq : μ .univ = ν .univ) :
     fDiv (fun x ↦ f x + c * (x - 1)) μ ν = fDiv f μ ν := by
   rw [fDiv_add_linear' hf_cvx, h_eq, ← EReal.coe_sub, sub_self]
   simp
@@ -382,7 +382,7 @@ lemma fDiv_eq_fDiv_centeredFunction [IsFiniteMeasure μ] [IsFiniteMeasure ν]
     <;> simp [EReal.mul_ne_top, EReal.mul_ne_bot, measure_ne_top]
 
 lemma fDiv_of_mutuallySingular [SigmaFinite μ] [IsFiniteMeasure ν] (h : μ ⟂ₘ ν) :
-    fDiv f μ ν = (f 0 : EReal) * ν Set.univ + derivAtTop f * μ Set.univ := by
+    fDiv f μ ν = (f 0 : EReal) * ν .univ + derivAtTop f * μ .univ := by
   have : μ.singularPart ν = μ := (μ.singularPart_eq_self).mpr h
   have hf_rnDeriv : (fun x ↦ f ((∂μ/∂ν) x).toReal) =ᵐ[ν] fun _ ↦ f 0 := by
     filter_upwards [Measure.rnDeriv_eq_zero_of_mutuallySingular h Measure.AbsolutelyContinuous.rfl]
@@ -410,7 +410,7 @@ lemma fDiv_of_absolutelyContinuous
 lemma fDiv_eq_add_withDensity_singularPart
     (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hf_cvx : ConvexOn ℝ (Ici 0) f) :
     fDiv f μ ν = fDiv f (ν.withDensity (∂μ/∂ν)) ν + fDiv f (μ.singularPart ν) ν
-      - f 0 * ν Set.univ := by
+      - f 0 * ν .univ := by
   have h_int_iff : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν
       ↔ Integrable (fun x ↦ f ((∂(ν.withDensity (∂μ/∂ν))/∂ν) x).toReal) ν := by
     refine integrable_congr ?_
@@ -432,7 +432,7 @@ lemma fDiv_eq_add_withDensity_singularPart
   · rw [fDiv_of_not_integrable hf, fDiv_of_not_integrable]
     · rw [add_sub_assoc, ← EReal.coe_ennreal_toReal (measure_ne_top ν _), ← EReal.coe_mul,
         EReal.add_sub_cancel']
-      by_cases h0 : μ.singularPart ν Set.univ = 0
+      by_cases h0 : μ.singularPart ν .univ = 0
       · simp [h0]
       · by_cases h_top : derivAtTop f = ⊤
         · rw [h_top, EReal.top_mul_ennreal_coe h0, EReal.top_add_top]
@@ -463,7 +463,7 @@ lemma fDiv_eq_add_withDensity_singularPart''
 lemma fDiv_eq_add_withDensity_derivAtTop
     (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
     (hf_cvx : ConvexOn ℝ (Ici 0) f) :
-    fDiv f μ ν = fDiv f (ν.withDensity (∂μ/∂ν)) ν + derivAtTop f * μ.singularPart ν Set.univ := by
+    fDiv f μ ν = fDiv f (ν.withDensity (∂μ/∂ν)) ν + derivAtTop f * μ.singularPart ν .univ := by
   rw [fDiv_eq_add_withDensity_singularPart'' μ ν hf_cvx,
     fDiv_of_mutuallySingular (Measure.mutuallySingular_singularPart _ _),
     derivAtTop_sub_const hf_cvx]
@@ -478,7 +478,7 @@ lemma fDiv_lt_top_of_ac (h : μ ≪ ν) (h_int : Integrable (fun x ↦ f ((∂μ
 lemma fDiv_add_measure_le_of_ac {μ₁ μ₂ ν : Measure α} [IsFiniteMeasure μ₁] [IsFiniteMeasure μ₂]
     [IsFiniteMeasure ν] (h₁ : μ₁ ≪ ν) (h₂ : μ₂ ≪ ν)
     (hf : StronglyMeasurable f) (hf_cvx : ConvexOn ℝ (Ici 0) f) :
-    fDiv f (μ₁ + μ₂) ν ≤ fDiv f μ₁ ν + derivAtTop f * μ₂ Set.univ := by
+    fDiv f (μ₁ + μ₂) ν ≤ fDiv f μ₁ ν + derivAtTop f * μ₂ .univ := by
   classical
   by_cases hμ₂0 : μ₂ = 0
   · simp [hμ₂0]
@@ -507,14 +507,14 @@ lemma fDiv_add_measure_le_of_ac {μ₁ μ₂ ν : Measure α} [IsFiniteMeasure 
     ≤ ∫ x, f ((∂μ₁/∂ν) x).toReal + df * ((∂μ₂/∂ν) x).toReal ∂ν := by
         refine integral_mono_ae h_int_add ?_ h_le
         exact h_int.add (Measure.integrable_toReal_rnDeriv.const_mul _)
-  _ ≤ ∫ x, f ((∂μ₁/∂ν) x).toReal ∂ν + df * (μ₂ Set.univ).toReal := by
+  _ ≤ ∫ x, f ((∂μ₁/∂ν) x).toReal ∂ν + df * (μ₂ .univ).toReal := by
         rw [integral_add h_int (Measure.integrable_toReal_rnDeriv.const_mul _),
           integral_mul_left, Measure.integral_toReal_rnDeriv h₂]
 
 lemma fDiv_absolutelyContinuous_add_mutuallySingular {μ₁ μ₂ ν : Measure α}
     [IsFiniteMeasure μ₁] [IsFiniteMeasure μ₂] [IsFiniteMeasure ν] (h₁ : μ₁ ≪ ν) (h₂ : μ₂ ⟂ₘ ν)
     (hf_cvx : ConvexOn ℝ (Ici 0) f) :
-    fDiv f (μ₁ + μ₂) ν = fDiv f μ₁ ν + derivAtTop f * μ₂ Set.univ := by
+    fDiv f (μ₁ + μ₂) ν = fDiv f μ₁ ν + derivAtTop f * μ₂ .univ := by
   rw [fDiv_eq_add_withDensity_derivAtTop  _ _ hf_cvx, Measure.singularPart_add,
     Measure.singularPart_eq_zero_of_ac h₁, Measure.singularPart_eq_self.mpr h₂, zero_add]
   congr
@@ -527,7 +527,7 @@ lemma fDiv_absolutelyContinuous_add_mutuallySingular {μ₁ μ₂ ν : Measure 
 
 lemma fDiv_add_measure_le (μ₁ μ₂ ν : Measure α) [IsFiniteMeasure μ₁] [IsFiniteMeasure μ₂]
     [IsFiniteMeasure ν] (hf : StronglyMeasurable f) (hf_cvx : ConvexOn ℝ (Ici 0) f) :
-    fDiv f (μ₁ + μ₂) ν ≤ fDiv f μ₁ ν + derivAtTop f * μ₂ Set.univ := by
+    fDiv f (μ₁ + μ₂) ν ≤ fDiv f μ₁ ν + derivAtTop f * μ₂ .univ := by
   rw [μ₂.haveLebesgueDecomposition_add ν, μ₁.haveLebesgueDecomposition_add ν]
   have : μ₁.singularPart ν + ν.withDensity (∂μ₁/∂ν) + (μ₂.singularPart ν + ν.withDensity (∂μ₂/∂ν))
       = (ν.withDensity (∂μ₁/∂ν) + ν.withDensity (∂μ₂/∂ν))
@@ -542,32 +542,27 @@ lemma fDiv_add_measure_le (μ₁ μ₂ ν : Measure α) [IsFiniteMeasure μ₁]
   rw [fDiv_absolutelyContinuous_add_mutuallySingular (withDensity_absolutelyContinuous _ _)
     (Measure.mutuallySingular_singularPart _ _) hf_cvx]
   calc fDiv f (ν.withDensity (∂μ₁/∂ν) + ν.withDensity (∂μ₂/∂ν)) ν +
-      derivAtTop f * (↑(μ₁.singularPart ν Set.univ) + ↑(μ₂.singularPart ν Set.univ))
+      derivAtTop f * (↑(μ₁.singularPart ν .univ) + ↑(μ₂.singularPart ν .univ))
     = fDiv f (ν.withDensity (∂μ₁/∂ν) + ν.withDensity (∂μ₂/∂ν)) ν
-      + derivAtTop f * μ₁.singularPart ν Set.univ
-      + derivAtTop f * μ₂.singularPart ν Set.univ := by
+      + derivAtTop f * μ₁.singularPart ν .univ + derivAtTop f * μ₂.singularPart ν .univ := by
         simp_rw [← EReal.coe_ennreal_toReal (measure_ne_top _ _)]
         rw [add_assoc, EReal.mul_add_coe_of_nonneg _ ENNReal.toReal_nonneg ENNReal.toReal_nonneg]
-  _ ≤ fDiv f (ν.withDensity (∂μ₁/∂ν)) ν + derivAtTop f * ν.withDensity (∂μ₂/∂ν) Set.univ
-      + derivAtTop f * μ₁.singularPart ν Set.univ
-      + derivAtTop f * μ₂.singularPart ν Set.univ := by
+  _ ≤ fDiv f (ν.withDensity (∂μ₁/∂ν)) ν + derivAtTop f * ν.withDensity (∂μ₂/∂ν) .univ
+      + derivAtTop f * μ₁.singularPart ν .univ + derivAtTop f * μ₂.singularPart ν .univ := by
         gcongr
         exact fDiv_add_measure_le_of_ac (withDensity_absolutelyContinuous _ _)
           (withDensity_absolutelyContinuous _ _) hf hf_cvx
-  _ = fDiv f (ν.withDensity (∂μ₁/∂ν)) ν
-      + derivAtTop f * μ₁.singularPart ν Set.univ
-      + derivAtTop f * μ₂.singularPart ν Set.univ
-      + derivAtTop f * ν.withDensity (∂μ₂/∂ν) Set.univ := by
+  _ = fDiv f (ν.withDensity (∂μ₁/∂ν)) ν + derivAtTop f * μ₁.singularPart ν .univ
+      + derivAtTop f * μ₂.singularPart ν .univ + derivAtTop f * ν.withDensity (∂μ₂/∂ν) .univ := by
         abel
-  _ = fDiv f (ν.withDensity (∂μ₁/∂ν)) ν
-      + derivAtTop f * μ₁.singularPart ν Set.univ
-      + derivAtTop f * (↑(μ₂.singularPart ν Set.univ) + ↑(ν.withDensity (∂μ₂/∂ν) Set.univ)) := by
+  _ = fDiv f (ν.withDensity (∂μ₁/∂ν)) ν + derivAtTop f * μ₁.singularPart ν .univ
+      + derivAtTop f * (↑(μ₂.singularPart ν .univ) + ↑(ν.withDensity (∂μ₂/∂ν) .univ)) := by
         simp_rw [← EReal.coe_ennreal_toReal (measure_ne_top _ _)]
         rw [add_assoc, EReal.mul_add_coe_of_nonneg _ ENNReal.toReal_nonneg ENNReal.toReal_nonneg]
 
 lemma fDiv_le_zero_add_top_of_ac [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hμν : μ ≪ ν)
     (hf : StronglyMeasurable f) (hf_cvx : ConvexOn ℝ (Ici 0) f) :
-    fDiv f μ ν ≤ f 0 * ν Set.univ + derivAtTop f * μ Set.univ := by
+    fDiv f μ ν ≤ f 0 * ν .univ + derivAtTop f * μ .univ := by
   classical
   by_cases hμ : μ = 0
   · simp [hμ]
@@ -596,20 +591,20 @@ lemma fDiv_le_zero_add_top_of_ac [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hμ
 
 lemma fDiv_le_zero_add_top [IsFiniteMeasure μ] [IsFiniteMeasure ν]
     (hf : StronglyMeasurable f) (hf_cvx : ConvexOn ℝ (Ici 0) f) :
-    fDiv f μ ν ≤ f 0 * ν Set.univ + derivAtTop f * μ Set.univ := by
+    fDiv f μ ν ≤ f 0 * ν .univ + derivAtTop f * μ .univ := by
   rw [fDiv_eq_add_withDensity_derivAtTop _ _ hf_cvx]
-  calc fDiv f (ν.withDensity (∂μ/∂ν)) ν + derivAtTop f * μ.singularPart ν Set.univ
-    ≤ f 0 * ν Set.univ + derivAtTop f * ν.withDensity (∂μ/∂ν) Set.univ
-      + derivAtTop f * μ.singularPart ν Set.univ := by
+  calc fDiv f (ν.withDensity (∂μ/∂ν)) ν + derivAtTop f * μ.singularPart ν .univ
+    ≤ f 0 * ν .univ + derivAtTop f * ν.withDensity (∂μ/∂ν) .univ
+      + derivAtTop f * μ.singularPart ν .univ := by
         gcongr
         exact fDiv_le_zero_add_top_of_ac (withDensity_absolutelyContinuous _ _) hf hf_cvx
-  _ ≤ f 0 * ν Set.univ + derivAtTop f * μ Set.univ := by
-        rw [add_assoc]
-        gcongr
-        conv_rhs => rw [μ.haveLebesgueDecomposition_add ν, add_comm]
-        simp only [Measure.coe_add, Pi.add_apply, EReal.coe_ennreal_add]
-        simp_rw [← EReal.coe_ennreal_toReal (measure_ne_top _ _)]
-        rw [EReal.mul_add_coe_of_nonneg _ ENNReal.toReal_nonneg ENNReal.toReal_nonneg]
+    _ ≤ f 0 * ν .univ + derivAtTop f * μ .univ := by
+      rw [add_assoc]
+      gcongr
+      conv_rhs => rw [μ.haveLebesgueDecomposition_add ν, add_comm]
+      simp only [Measure.coe_add, Pi.add_apply, EReal.coe_ennreal_add]
+      simp_rw [← EReal.coe_ennreal_toReal (measure_ne_top _ _)]
+      rw [EReal.mul_add_coe_of_nonneg _ ENNReal.toReal_nonneg ENNReal.toReal_nonneg]
 
 section derivAtTopTop
 
@@ -618,7 +613,7 @@ lemma fDiv_of_not_ac [SigmaFinite μ] [SigmaFinite ν] (hf : derivAtTop f = ⊤)
   rw [fDiv]
   split_ifs with h_int
   · rw [hf]
-    suffices Measure.singularPart μ ν Set.univ ≠ 0 by
+    suffices Measure.singularPart μ ν .univ ≠ 0 by
       rw [EReal.top_mul_of_pos, EReal.coe_add_top]
       refine lt_of_le_of_ne (EReal.coe_ennreal_nonneg _) ?_
       exact mod_cast this.symm
@@ -714,7 +709,7 @@ lemma integrable_of_fDiv_ne_top (h : fDiv f μ ν ≠ ⊤) :
   exact h (fDiv_of_not_integrable h_not)
 
 lemma fDiv_of_ne_top (h : fDiv f μ ν ≠ ⊤) :
-    fDiv f μ ν = ∫ x, f ((∂μ/∂ν) x).toReal ∂ν + derivAtTop f * μ.singularPart ν Set.univ := by
+    fDiv f μ ν = ∫ x, f ((∂μ/∂ν) x).toReal ∂ν + derivAtTop f * μ.singularPart ν .univ := by
   rw [fDiv_of_integrable]
   exact integrable_of_fDiv_ne_top h
 
@@ -722,7 +717,7 @@ lemma toReal_fDiv_of_integrable [IsFiniteMeasure μ] (hf_cvx : ConvexOn ℝ (Ici
     (hf_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν)
     (h_deriv : derivAtTop f = ⊤ → μ ≪ ν) :
     (fDiv f μ ν).toReal = ∫ y, f ((∂μ/∂ν) y).toReal ∂ν
-        + (derivAtTop f * μ.singularPart ν Set.univ).toReal := by
+        + (derivAtTop f * μ.singularPart ν .univ).toReal := by
   rw [fDiv_of_integrable hf_int, EReal.toReal_add]
   rotate_left
   · simp
@@ -741,13 +736,13 @@ lemma toReal_fDiv_of_integrable [IsFiniteMeasure μ] (hf_cvx : ConvexOn ℝ (Ici
 lemma le_fDiv_of_ac [IsFiniteMeasure μ] [IsProbabilityMeasure ν]
     (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0))
     (hμν : μ ≪ ν) :
-    f (μ Set.univ).toReal ≤ fDiv f μ ν := by
+    f (μ .univ).toReal ≤ fDiv f μ ν := by
   by_cases hf_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν
   swap; · rw [fDiv_of_not_integrable hf_int]; exact le_top
   rw [fDiv_of_integrable hf_int, Measure.singularPart_eq_zero_of_ac hμν]
   simp only [Measure.coe_zero, Pi.zero_apply,
     EReal.coe_ennreal_zero, mul_zero, add_zero, EReal.coe_le_coe_iff]
-  calc f (μ Set.univ).toReal
+  calc f (μ .univ).toReal
     = f (∫ x, (μ.rnDeriv ν x).toReal ∂ν) := by rw [Measure.integral_toReal_rnDeriv hμν]
   _ ≤ ∫ x, f (μ.rnDeriv ν x).toReal ∂ν := by
     rw [← average_eq_integral, ← average_eq_integral]
@@ -756,9 +751,9 @@ lemma le_fDiv_of_ac [IsFiniteMeasure μ] [IsProbabilityMeasure ν]
 
 lemma f_measure_univ_le_add (μ ν : Measure α) [IsFiniteMeasure μ] [IsProbabilityMeasure ν]
     (hf_cvx : ConvexOn ℝ (Ici 0) f) :
-    f (μ Set.univ).toReal
-      ≤ f (ν.withDensity (∂μ/∂ν) Set.univ).toReal + derivAtTop f * μ.singularPart ν Set.univ := by
-  have : μ Set.univ = ν.withDensity (∂μ/∂ν) Set.univ + μ.singularPart ν Set.univ := by
+    f (μ .univ).toReal
+      ≤ f (ν.withDensity (∂μ/∂ν) .univ).toReal + derivAtTop f * μ.singularPart ν .univ := by
+  have : μ .univ = ν.withDensity (∂μ/∂ν) .univ + μ.singularPart ν .univ := by
     conv_lhs => rw [μ.haveLebesgueDecomposition_add ν, add_comm]
     simp
   rw [this]
@@ -766,7 +761,7 @@ lemma f_measure_univ_le_add (μ ν : Measure α) [IsFiniteMeasure μ] [IsProbabi
 
 lemma le_fDiv [IsFiniteMeasure μ] [IsProbabilityMeasure ν]
     (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0)) :
-    f (μ Set.univ).toReal ≤ fDiv f μ ν := by
+    f (μ .univ).toReal ≤ fDiv f μ ν := by
   refine (f_measure_univ_le_add μ ν hf_cvx).trans ?_
   rw [fDiv_eq_add_withDensity_singularPart'' μ _ hf_cvx,
     fDiv_of_mutuallySingular  (Measure.mutuallySingular_singularPart μ ν),
@@ -774,13 +769,13 @@ lemma le_fDiv [IsFiniteMeasure μ] [IsProbabilityMeasure ν]
   simp only [MeasurableSet.univ, withDensity_apply, Measure.restrict_univ, sub_self, EReal.coe_zero,
     measure_univ, EReal.coe_ennreal_one, mul_one, zero_add]
   gcongr
-  rw [← setLIntegral_univ, ← withDensity_apply _ MeasurableSet.univ]
+  rw [← setLIntegral_univ, ← withDensity_apply _ .univ]
   exact le_fDiv_of_ac hf_cvx hf_cont (withDensity_absolutelyContinuous _ _)
 
 lemma fDiv_nonneg [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
     (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0)) (hf_one : f 1 = 0) :
     0 ≤ fDiv f μ ν := by
-  calc (0 : EReal) = f (μ Set.univ).toReal := by simp [hf_one]
+  calc (0 : EReal) = f (μ .univ).toReal := by simp [hf_one]
   _ ≤ fDiv f μ ν := le_fDiv hf_cvx hf_cont
 
 /- The hypothesis `hfg'` can maybe become something like `f ≤ᵐ[atTop] g`, but then we would need
@@ -807,7 +802,7 @@ lemma fDiv_nonneg_of_nonneg (hf : 0 ≤ f) (hf' : 0 ≤ derivAtTop f) :
     0 ≤ fDiv f μ ν :=
   fDiv_zero μ ν ▸ fDiv_mono' (integrable_zero α ℝ ν) hf (derivAtTop_zero ▸ hf')
 
-lemma fDiv_eq_zero_iff [IsFiniteMeasure μ] [IsFiniteMeasure ν] (h_mass : μ Set.univ = ν Set.univ)
+lemma fDiv_eq_zero_iff [IsFiniteMeasure μ] [IsFiniteMeasure ν] (h_mass : μ .univ = ν .univ)
     (hf_deriv : derivAtTop f = ⊤) (hf_cvx : StrictConvexOn ℝ (Ici 0) f)
     (hf_cont : ContinuousOn f (Ici 0)) (hf_one : f 1 = 0) :
     fDiv f μ ν = 0 ↔ μ = ν := by
@@ -885,30 +880,30 @@ section Measurability
 
 lemma measurableSet_integrable_f_kernel_rnDeriv [MeasurableSpace.CountableOrCountablyGenerated α β]
     (κ η ξ : Kernel α β) [IsFiniteKernel ξ] (hf : StronglyMeasurable f) :
-    MeasurableSet {a | Integrable (fun x ↦ f (Kernel.rnDeriv κ η a x).toReal) (ξ a)} :=
+    MeasurableSet {a | Integrable (fun x ↦ f (κ.rnDeriv η a x).toReal) (ξ a)} :=
   measurableSet_kernel_integrable
-    (hf.comp_measurable (Kernel.measurable_rnDeriv κ η).ennreal_toReal)
+    (hf.comp_measurable (κ.measurable_rnDeriv η).ennreal_toReal)
 
 lemma measurableSet_integrable_f_rnDeriv [MeasurableSpace.CountableOrCountablyGenerated α β]
     (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] (hf : StronglyMeasurable f) :
     MeasurableSet {a | Integrable (fun x ↦ f ((∂κ a/∂η a) x).toReal) (η a)} := by
   convert measurableSet_integrable_f_kernel_rnDeriv κ η η hf using 3 with a
   refine integrable_congr ?_
-  filter_upwards [Kernel.rnDeriv_eq_rnDeriv_measure κ η a] with b hb
+  filter_upwards [κ.rnDeriv_eq_rnDeriv_measure η a] with b hb
   rw [hb]
 
 lemma measurable_integral_f_rnDeriv [MeasurableSpace.CountableOrCountablyGenerated α β]
     (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] (hf : StronglyMeasurable f) :
     Measurable fun a ↦ ∫ x, f ((∂κ a/∂η a) x).toReal ∂(η a) := by
   have : ∀ a, ∫ x, f ((∂κ a/∂η a) x).toReal ∂η a
-      = ∫ x, f (Kernel.rnDeriv κ η a x).toReal ∂η a := by
+      = ∫ x, f (κ.rnDeriv η a x).toReal ∂η a := by
     refine fun a ↦ integral_congr_ae ?_
-    filter_upwards [Kernel.rnDeriv_eq_rnDeriv_measure κ η a] with x hx
+    filter_upwards [κ.rnDeriv_eq_rnDeriv_measure η a] with x hx
     rw [hx]
   simp_rw [this]
   refine (StronglyMeasurable.integral_kernel_prod_left ?_).measurable
   refine hf.comp_measurable ?_
-  exact ((Kernel.measurable_rnDeriv κ η).comp measurable_swap).ennreal_toReal
+  exact ((κ.measurable_rnDeriv η).comp measurable_swap).ennreal_toReal
 
 lemma measurable_fDiv [MeasurableSpace.CountableOrCountablyGenerated α β]
     (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η]
@@ -919,7 +914,7 @@ lemma measurable_fDiv [MeasurableSpace.CountableOrCountablyGenerated α β]
   classical
   have h_eq : (fun a ↦ fDiv f (κ a) (η a))
       = fun a ↦ if a ∈ s then ∫ x, f ((∂κ a/∂η a) x).toReal ∂(η a)
-          + derivAtTop f * (κ a).singularPart (η a) Set.univ
+          + derivAtTop f * (κ a).singularPart (η a) .univ
         else ⊤ := by
     ext a
     split_ifs with ha
@@ -930,8 +925,7 @@ lemma measurable_fDiv [MeasurableSpace.CountableOrCountablyGenerated α β]
   refine Measurable.add ?_ ?_
   · exact (measurable_integral_f_rnDeriv _ _ hf).coe_real_ereal
   · refine Measurable.const_mul ?_ _
-    exact ((Measure.measurable_coe MeasurableSet.univ).comp
-      (Kernel.measurable_singularPart κ η)).coe_ereal_ennreal
+    exact ((Measure.measurable_coe .univ).comp (κ.measurable_singularPart η)).coe_ereal_ennreal
 
 end Measurability
 
diff --git a/TestingLowerBounds/FDiv/CompProd.lean b/TestingLowerBounds/FDiv/CompProd.lean
index 67a78ed6..9b11e8d2 100644
--- a/TestingLowerBounds/FDiv/CompProd.lean
+++ b/TestingLowerBounds/FDiv/CompProd.lean
@@ -63,7 +63,7 @@ lemma integrable_fDiv_iff [CountableOrCountablyGenerated α β] [IsFiniteMeasure
     simp_rw [fDiv_ne_top_iff_of_derivAtTop_ne_top h_top] at h_fin
     have : (fun x ↦ (fDiv f (κ x) (η x)).toReal)
         =ᵐ[μ] (fun x ↦ ∫ y, f ((∂κ x/∂η x) y).toReal ∂(η x)
-          + (derivAtTop f).toReal * ((κ x).singularPart (η x) Set.univ).toReal) := by
+          + (derivAtTop f).toReal * ((κ x).singularPart (η x) .univ).toReal) := by
       filter_upwards [h_fin'] with x hx1
       rw [fDiv_of_ne_top hx1, EReal.toReal_add]
       · simp only [EReal.toReal_coe, add_right_inj]
@@ -75,12 +75,12 @@ lemma integrable_fDiv_iff [CountableOrCountablyGenerated α β] [IsFiniteMeasure
       · simp [EReal.mul_eq_bot, h_cvx.derivAtTop_ne_bot, h_top, measure_ne_top]
     rw [integrable_congr this]
     have h_int : Integrable (fun x ↦ (derivAtTop f).toReal
-        * ((κ x).singularPart (η x) Set.univ).toReal) μ :=
+        * ((κ x).singularPart (η x) .univ).toReal) μ :=
       Integrable.const_mul integrable_singularPart (derivAtTop f).toReal
     have h_eq : (fun x ↦ ∫ y, f ((∂κ x/∂η x) y).toReal ∂η x)
         = (fun x ↦ (∫ y, f ((∂κ x/∂η x) y).toReal ∂η x +
-          (derivAtTop f).toReal * ((κ x).singularPart (η x) Set.univ).toReal)
-          - (derivAtTop f).toReal * ((κ x).singularPart (η x) Set.univ).toReal) := by
+          (derivAtTop f).toReal * ((κ x).singularPart (η x) .univ).toReal)
+          - (derivAtTop f).toReal * ((κ x).singularPart (η x) .univ).toReal) := by
       ext; simp
     exact ⟨fun h ↦ h_eq ▸ h.sub h_int, fun h ↦ h.add h_int⟩
 
@@ -202,7 +202,7 @@ lemma fDiv_compProd_right
     simp only [measure_univ, ENNReal.one_toReal, one_mul] at h
     rw [integral_congr_ae h.symm, Measure.integral_compProd]
     · congr
-      rw [singularPart_compProd_left, Measure.compProd_apply MeasurableSet.univ]
+      rw [singularPart_compProd_left, Measure.compProd_apply .univ]
       simp
     · rw [← ne_eq, fDiv_ne_top_iff] at h_top
       exact h_top.1
@@ -217,7 +217,7 @@ lemma fDiv_toReal_eq_ae {γ : Type*} [MeasurableSpace γ]
       Integrable (fun x ↦ f ((∂κ (a, b)/∂η (a, b)) x).toReal) (η (a, b))) :
     ∀ᵐ a ∂μ, ∀ᵐ b ∂ξ a, (fDiv f (κ (a, b)) (η (a, b))).toReal =
       ∫ x, f ((∂κ (a, b)/∂η (a, b)) x).toReal ∂η (a, b)
-      + (derivAtTop f).toReal * (((κ (a, b)).singularPart (η (a, b)) Set.univ)).toReal := by
+      + (derivAtTop f).toReal * (((κ (a, b)).singularPart (η (a, b)) .univ)).toReal := by
   filter_upwards [eventually_all.mpr h_ac, h_int] with a ha_ae ha_int
   filter_upwards [eventually_all.mpr ha_ae, ha_int] with b hb_ae hb_int
   rw [← EReal.toReal_coe (∫ _, _ ∂_), fDiv_of_integrable hb_int, ← EReal.toReal_coe_ennreal,
@@ -241,7 +241,7 @@ lemma f_rnDeriv_ae_le_integral [CountableOrCountablyGenerated α β]
     (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0))
     (h_int : Integrable (fun p ↦ f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η))
     (hκη : ∀ᵐ a ∂μ, κ a ≪ η a) :
-    (fun a ↦ f ((∂μ/∂ν) a * κ a Set.univ).toReal)
+    (fun a ↦ f ((∂μ/∂ν) a * κ a .univ).toReal)
       ≤ᵐ[ν] fun a ↦ ∫ b, f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) (a, b)).toReal ∂(η a) := by
   have h_compProd := Kernel.rnDeriv_measure_compProd' μ ν κ η
   have h_lt_top := Measure.ae_ae_of_ae_compProd <| Measure.rnDeriv_lt_top (μ ⊗ₘ κ) (ν ⊗ₘ η)
@@ -253,7 +253,7 @@ lemma f_rnDeriv_ae_le_integral [CountableOrCountablyGenerated α β]
   have hκη' : ∀ᵐ a ∂ν, (∂μ/∂ν) a ≠ 0 → κ a ≪ η a := Measure.ae_rnDeriv_ne_zero_imp_of_ae hκη
   filter_upwards [hκη', h_compProd, h_lt_top, h_int.compProd_mk_left_ae', this.1]
     with a h_ac h_eq h_lt_top h_int' h_rnDeriv_int
-  calc f ((∂μ/∂ν) a * κ a Set.univ).toReal
+  calc f ((∂μ/∂ν) a * κ a .univ).toReal
     = f ((∂μ/∂ν) a * ∫⁻ b, (∂κ a/∂η a) b ∂η a).toReal := by
         by_cases h0 : (∂μ/∂ν) a = 0
         · simp [h0]
@@ -275,21 +275,21 @@ lemma integrable_f_rnDeriv_mul_kernel [CountableOrCountablyGenerated α β]
     (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0))
     (h_int : Integrable (fun p ↦ f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η))
     (hκη : ∀ᵐ a ∂μ, κ a ≪ η a) :
-    Integrable (fun a ↦ f ((∂μ/∂ν) a * κ a Set.univ).toReal) ν := by
+    Integrable (fun a ↦ f ((∂μ/∂ν) a * κ a .univ).toReal) ν := by
   obtain ⟨c, c', h⟩ : ∃ c c', ∀ x, 0 ≤ x → c * x + c' ≤ f x :=
     hf_cvx.exists_affine_le (convex_Ici 0)
-  refine integrable_of_le_of_le (f := fun a ↦ f ((∂μ/∂ν) a * κ a Set.univ).toReal)
-    (g₁ := fun x ↦ c * ((∂μ/∂ν) x * κ x Set.univ).toReal + c')
+  refine integrable_of_le_of_le (f := fun a ↦ f ((∂μ/∂ν) a * κ a .univ).toReal)
+    (g₁ := fun x ↦ c * ((∂μ/∂ν) x * κ x .univ).toReal + c')
     (g₂ := fun x ↦ ∫ b, f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) (x, b)).toReal ∂(η x))
     ?_ ?_ ?_ ?_ ?_
-  · exact (hf.comp_measurable ((Measure.measurable_rnDeriv _ _).mul
-      (Kernel.measurable_coe _ MeasurableSet.univ)).ennreal_toReal).aestronglyMeasurable
+  · exact (hf.comp_measurable ((μ.measurable_rnDeriv _).mul
+      (κ.measurable_coe .univ)).ennreal_toReal).aestronglyMeasurable
   · exact ae_of_all _ (fun x ↦ h _ ENNReal.toReal_nonneg)
   · exact f_rnDeriv_ae_le_integral μ ν κ η hf_cvx hf_cont h_int hκη
   · refine (Integrable.const_mul ?_ _).add (integrable_const _)
     simp_rw [ENNReal.toReal_mul]
     have h := integrable_rnDeriv_mul_withDensity μ ν κ η
-    have h_ae : ∀ᵐ a ∂ν, (∂μ/∂ν) a ≠ 0 → Kernel.withDensity η (Kernel.rnDeriv κ η) a = κ a := by
+    have h_ae : ∀ᵐ a ∂ν, (∂μ/∂ν) a ≠ 0 → η.withDensity (κ.rnDeriv η) a = κ a := by
       refine Measure.ae_rnDeriv_ne_zero_imp_of_ae ?_
       filter_upwards [hκη] with x hx
       rw [Kernel.withDensity_rnDeriv_eq hx]
@@ -307,7 +307,7 @@ lemma integrable_f_rnDeriv_mul_withDensity [CountableOrCountablyGenerated α β]
     (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0))
     (h_int : Integrable (fun p ↦ f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)) :
     Integrable (fun a ↦
-      f ((∂μ/∂ν) a * Kernel.withDensity η (Kernel.rnDeriv κ η) a Set.univ).toReal) ν := by
+      f ((∂μ/∂ν) a * η.withDensity (κ.rnDeriv η) a .univ).toReal) ν := by
   refine integrable_f_rnDeriv_mul_kernel μ ν _ η hf hf_cvx hf_cont ?_ ?_
   · refine (integrable_congr ?_).mp h_int
     filter_upwards [Measure.rnDeriv_measure_compProd_Kernel_withDensity μ ν κ η] with x hx
@@ -321,8 +321,7 @@ lemma integral_f_rnDeriv_mul_le_integral [CountableOrCountablyGenerated α β]
     (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0))
     (h_int : Integrable (fun p ↦ f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η))
     (hκη : ∀ᵐ a ∂μ, κ a ≪ η a) :
-    ∫ x, f ((∂μ/∂ν) x * κ x Set.univ).toReal ∂ν
-      ≤ ∫ x, f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) x).toReal ∂(ν ⊗ₘ η) := by
+    ∫ x, f ((∂μ/∂ν) x * κ x .univ).toReal ∂ν ≤ ∫ x, f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) x).toReal ∂(ν ⊗ₘ η) := by
   rw [Measure.integral_compProd h_int]
   refine integral_mono_ae ?_ ?_ ?_
   · exact integrable_f_rnDeriv_mul_kernel μ ν κ η hf hf_cvx hf_cont h_int hκη
@@ -337,12 +336,12 @@ lemma integral_f_rnDeriv_mul_withDensity_le_integral [CountableOrCountablyGenera
     (hf : StronglyMeasurable f)
     (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0))
     (h_int : Integrable (fun p ↦ f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)) :
-    ∫ x, f ((∂μ/∂ν) x * Kernel.withDensity η (Kernel.rnDeriv κ η) x Set.univ).toReal ∂ν
+    ∫ x, f ((∂μ/∂ν) x * η.withDensity (κ.rnDeriv η) x .univ).toReal ∂ν
       ≤ ∫ x, f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) x).toReal ∂(ν ⊗ₘ η) := by
-  calc ∫ x, f ((∂μ/∂ν) x * Kernel.withDensity η (Kernel.rnDeriv κ η) x Set.univ).toReal ∂ν
-    ≤ ∫ x, f ((∂μ ⊗ₘ (Kernel.withDensity η (Kernel.rnDeriv κ η))/∂ν ⊗ₘ η) x).toReal
+  calc ∫ x, f ((∂μ/∂ν) x * η.withDensity (κ.rnDeriv η) x .univ).toReal ∂ν
+    ≤ ∫ x, f ((∂μ ⊗ₘ (η.withDensity (κ.rnDeriv η))/∂ν ⊗ₘ η) x).toReal
       ∂(ν ⊗ₘ η) := by
-        refine integral_f_rnDeriv_mul_le_integral μ ν (Kernel.withDensity η (Kernel.rnDeriv κ η))
+        refine integral_f_rnDeriv_mul_le_integral μ ν (η.withDensity (κ.rnDeriv η))
           η hf hf_cvx hf_cont ?_ ?_
         · refine (integrable_congr ?_).mpr h_int
           filter_upwards [Measure.rnDeriv_measure_compProd_Kernel_withDensity μ ν κ η] with x hx
@@ -358,12 +357,11 @@ lemma f_rnDeriv_le_add [CountableOrCountablyGenerated α β]
     (κ η : Kernel α β) [IsMarkovKernel κ] [IsFiniteKernel η]
     (hf_cvx : ConvexOn ℝ (Ici 0) f) (h_deriv : derivAtTop f = ⊤ → ∀ᵐ a ∂μ, κ a ≪ η a) :
     ∀ᵐ a ∂ ν, f ((∂μ/∂ν) a).toReal
-      ≤ f ((∂μ/∂ν) a * Kernel.withDensity η (Kernel.rnDeriv κ η) a Set.univ).toReal
-        + (derivAtTop f).toReal * ((∂μ/∂ν) a).toReal
-          * (Kernel.singularPart κ η a Set.univ).toReal := by
+      ≤ f ((∂μ/∂ν) a * η.withDensity (κ.rnDeriv η) a .univ).toReal
+        + (derivAtTop f).toReal * ((∂μ/∂ν) a).toReal * (κ.singularPart η a .univ).toReal := by
   by_cases h_deriv_top : derivAtTop f = ⊤
   · simp only [ENNReal.toReal_mul, h_deriv_top, EReal.toReal_top, zero_mul, add_zero]
-    have h_ae : ∀ᵐ a ∂ν, (∂μ/∂ν) a ≠ 0 → Kernel.withDensity η (Kernel.rnDeriv κ η) a = κ a := by
+    have h_ae : ∀ᵐ a ∂ν, (∂μ/∂ν) a ≠ 0 → η.withDensity (κ.rnDeriv η) a = κ a := by
       refine Measure.ae_rnDeriv_ne_zero_imp_of_ae ?_
       filter_upwards [h_deriv h_deriv_top] with a ha_ac
       rw [Kernel.withDensity_rnDeriv_eq ha_ac]
@@ -374,25 +372,24 @@ lemma f_rnDeriv_le_add [CountableOrCountablyGenerated α β]
       simp
   refine ae_of_all _ (fun a ↦ ?_)
   simp only [ENNReal.toReal_mul]
-  let κ' := Kernel.withDensity η (Kernel.rnDeriv κ η)
+  let κ' := η.withDensity (κ.rnDeriv η)
   calc f ((∂μ/∂ν) a).toReal
-  _ ≤ f (((∂μ/∂ν) a).toReal * (κ' a Set.univ).toReal)
-        + (derivAtTop f).toReal * ((∂μ/∂ν) a).toReal * (1 - (κ' a Set.univ).toReal) := by
+  _ ≤ f (((∂μ/∂ν) a).toReal * (κ' a .univ).toReal)
+        + (derivAtTop f).toReal * ((∂μ/∂ν) a).toReal * (1 - (κ' a .univ).toReal) := by
       refine le_add_derivAtTop' hf_cvx h_deriv_top ENNReal.toReal_nonneg ENNReal.toReal_nonneg ?_
-      calc (κ' a Set.univ).toReal
-      _ ≤ (κ a Set.univ).toReal := by
+      calc (κ' a .univ).toReal
+      _ ≤ (κ a .univ).toReal := by
           gcongr
           · exact measure_ne_top _ _
-          · exact Kernel.withDensity_rnDeriv_le κ η a Set.univ
+          · exact κ.withDensity_rnDeriv_le η a .univ
       _ = 1 := by simp
-  _ = f (((∂μ/∂ν) a).toReal * (κ' a Set.univ).toReal)
-        + (derivAtTop f).toReal * ((∂μ/∂ν) a).toReal
-          * (Kernel.singularPart κ η a Set.univ).toReal := by
+  _ = f (((∂μ/∂ν) a).toReal * (κ' a .univ).toReal)
+        + (derivAtTop f).toReal * ((∂μ/∂ν) a).toReal * (κ.singularPart η a .univ).toReal := by
       congr
       norm_cast
       unfold_let κ'
       rw [sub_eq_iff_eq_add, ← ENNReal.one_toReal, ← measure_univ (μ := κ a)]
-      conv_lhs => rw [← Kernel.rnDeriv_add_singularPart κ η, add_comm]
+      conv_lhs => rw [← κ.rnDeriv_add_singularPart η, add_comm]
       simp only [Kernel.coe_add, Pi.add_apply, Measure.coe_add]
       rw [ENNReal.toReal_add]
       · exact measure_ne_top _ _
@@ -410,9 +407,8 @@ lemma integrable_f_rnDeriv_of_integrable_compProd' [CountableOrCountablyGenerate
     hf_cvx.exists_affine_le (convex_Ici 0)
   refine integrable_of_le_of_le (f := fun a ↦ f ((∂μ/∂ν) a).toReal)
     (g₁ := fun a ↦ c * ((∂μ/∂ν) a).toReal + c')
-    (g₂ := fun a ↦ f ((∂μ/∂ν) a * Kernel.withDensity η (Kernel.rnDeriv κ η) a Set.univ).toReal
-        + (derivAtTop f).toReal * ((∂μ/∂ν) a).toReal
-          * (Kernel.singularPart κ η a Set.univ).toReal)
+    (g₂ := fun a ↦ f ((∂μ/∂ν) a * η.withDensity (κ.rnDeriv η) a .univ).toReal
+        + (derivAtTop f).toReal * ((∂μ/∂ν) a).toReal * (κ.singularPart η a .univ).toReal)
     ?_ ?_ ?_ ?_ ?_
   · exact (hf.comp_measurable (Measure.measurable_rnDeriv _ _).ennreal_toReal).aestronglyMeasurable
   · exact ae_of_all _ (fun x ↦ h _ ENNReal.toReal_nonneg)
@@ -449,25 +445,23 @@ lemma integral_f_rnDeriv_le_integral_add [CountableOrCountablyGenerated α β]
     (h_deriv : derivAtTop f = ⊤ → ∀ᵐ a ∂μ, κ a ≪ η a) :
     ∫ x, f ((∂μ/∂ν) x).toReal ∂ν
       ≤ ∫ x, f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) x).toReal ∂(ν ⊗ₘ η)
-      + (derivAtTop f).toReal
-        * ∫ a, ((∂μ/∂ν) a).toReal * (Kernel.singularPart κ η a Set.univ).toReal ∂ν := by
+        + (derivAtTop f).toReal
+          * ∫ a, ((∂μ/∂ν) a).toReal * (κ.singularPart η a .univ).toReal ∂ν := by
   suffices ∫ x, f ((∂μ/∂ν) x).toReal ∂ν
-      ≤ ∫ x, f ((∂μ/∂ν) x * Kernel.withDensity η (Kernel.rnDeriv κ η) x Set.univ).toReal ∂ν
-      + (derivAtTop f).toReal
-        * ∫ a, ((∂μ/∂ν) a).toReal * (Kernel.singularPart κ η a Set.univ).toReal ∂ν by
+      ≤ ∫ x, f ((∂μ/∂ν) x * η.withDensity (κ.rnDeriv η) x .univ).toReal ∂ν
+        + (derivAtTop f).toReal * ∫ a, ((∂μ/∂ν) a).toReal * (κ.singularPart η a .univ).toReal ∂ν by
     refine this.trans ?_
     gcongr
     exact integral_f_rnDeriv_mul_withDensity_le_integral μ ν κ η hf hf_cvx hf_cont h_int
-  let κ' := Kernel.withDensity η (Kernel.rnDeriv κ η)
+  let κ' := η.withDensity (κ.rnDeriv η)
   have h : ∀ᵐ a ∂ν, f ((∂μ/∂ν) a).toReal
-      ≤ f ((∂μ/∂ν) a * κ' a Set.univ).toReal
-        + (derivAtTop f).toReal * ((∂μ/∂ν) a).toReal
-          * (Kernel.singularPart κ η a Set.univ).toReal :=
+      ≤ f ((∂μ/∂ν) a * κ' a .univ).toReal
+        + (derivAtTop f).toReal * ((∂μ/∂ν) a).toReal * (κ.singularPart η a .univ).toReal :=
     f_rnDeriv_le_add _ _ _ _ hf_cvx h_deriv
-  have h_int_mul : Integrable (fun a ↦ f ((∂μ/∂ν) a * κ' a Set.univ).toReal) ν :=
+  have h_int_mul : Integrable (fun a ↦ f ((∂μ/∂ν) a * κ' a .univ).toReal) ν :=
     integrable_f_rnDeriv_mul_withDensity μ ν κ η hf hf_cvx hf_cont h_int
   have h_int_right : Integrable (fun a ↦ (derivAtTop f).toReal
-      * ((∂μ/∂ν) a).toReal * (Kernel.singularPart κ η a Set.univ).toReal) ν := by
+      * ((∂μ/∂ν) a).toReal * (κ.singularPart η a .univ).toReal) ν := by
     simp_rw [mul_assoc]
     refine Integrable.const_mul ?_ _
     simp_rw [Kernel.singularPart_eq_singularPart_measure]
@@ -492,22 +486,21 @@ lemma le_fDiv_compProd [CountableOrCountablyGenerated α β] (μ ν : Measure α
   obtain h_int := (fDiv_ne_top_iff.mp h_top).1
   rw [← ne_eq, fDiv_compProd_ne_top_iff hf hf_cvx] at h_top
   obtain ⟨_, _, h3⟩ := h_top
-  calc ∫ x, f ((∂μ/∂ν) x).toReal ∂ν + derivAtTop f * Measure.singularPart μ ν Set.univ
+  calc ∫ x, f ((∂μ/∂ν) x).toReal ∂ν + derivAtTop f * μ.singularPart ν .univ
     ≤ ∫ x, f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) x).toReal ∂(ν ⊗ₘ η)
-      + (derivAtTop f).toReal
-        * ∫ a, ((∂μ/∂ν) a).toReal * (Kernel.singularPart κ η a Set.univ).toReal ∂ν
-      + derivAtTop f * Measure.singularPart μ ν Set.univ := by
+      + (derivAtTop f).toReal * ∫ a, ((∂μ/∂ν) a).toReal * (κ.singularPart η a .univ).toReal ∂ν
+      + derivAtTop f * Measure.singularPart μ ν .univ := by
         gcongr
         norm_cast
         exact integral_f_rnDeriv_le_integral_add μ ν κ η hf hf_cvx hf_cont h_int (fun h ↦ (h3 h).2)
   _ = ∫ x, f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) x).toReal ∂(ν ⊗ₘ η)
       + (derivAtTop f).toReal
-        * (((ν.withDensity (∂μ/∂ν)) ⊗ₘ κ).singularPart (ν ⊗ₘ η) Set.univ).toReal
-      + derivAtTop f * Measure.singularPart μ ν Set.univ := by
+        * (((ν.withDensity (∂μ/∂ν)) ⊗ₘ κ).singularPart (ν ⊗ₘ η) .univ).toReal
+      + derivAtTop f * Measure.singularPart μ ν .univ := by
         simp_rw [Kernel.singularPart_eq_singularPart_measure]
-        rw [integral_rnDeriv_mul_singularPart _ _ _ _ MeasurableSet.univ, Set.univ_prod_univ]
+        rw [integral_rnDeriv_mul_singularPart _ _ _ _ .univ, Set.univ_prod_univ]
   _ = ∫ p, f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal ∂ν ⊗ₘ η
-      + derivAtTop f * (μ ⊗ₘ κ).singularPart (ν ⊗ₘ η) Set.univ := by
+      + derivAtTop f * (μ ⊗ₘ κ).singularPart (ν ⊗ₘ η) .univ := by
         rw [add_assoc]
         congr
         by_cases h_top : derivAtTop f = ⊤
@@ -531,18 +524,17 @@ lemma le_fDiv_compProd [CountableOrCountablyGenerated α β] (μ ν : Measure α
         congr
         rw [singularPart_compProd]
         simp only [Measure.coe_add, Pi.add_apply]
-        rw [Measure.compProd_apply MeasurableSet.univ]
-        rw [Measure.compProd_apply MeasurableSet.univ]
+        simp_rw [Measure.compProd_apply .univ]
         simp only [Measure.singularPart_singularPart, Set.preimage_univ]
         rw [← lintegral_add_right]
         · rw [← lintegral_one]
           congr with a
-          have h : κ a Set.univ = 1 := by simp
-          rw [← Kernel.rnDeriv_add_singularPart κ η] at h
+          have h : κ a .univ = 1 := by simp
+          rw [← κ.rnDeriv_add_singularPart η] at h
           simp only [Kernel.coe_add, Pi.add_apply, Measure.add_toOuterMeasure,
             OuterMeasure.coe_add] at h
           exact h.symm
-        · exact Kernel.measurable_coe _ MeasurableSet.univ
+        · exact Kernel.measurable_coe _ .univ
 
 lemma fDiv_fst_le [Nonempty β] [StandardBorelSpace β]
     (μ ν : Measure (α × β)) [IsFiniteMeasure μ] [IsFiniteMeasure ν]