Bump Mathlib to the commit of Tau Ceti's v4.36.0-rc2 tag

LeanMachineLearning/ForMathlib/InformationTheory/KullbackLeibler/Convex.lean

@@ -86,9 +86,9 @@ lemma klDiv_finsetSum_smul_le [∀ i, IsFiniteMeasure (μ i)]
   have h_comp (ρ : Kernel s Ω) (ρ' : ι → Measure Ω) (hρ : ∀ i : s, ρ i = ρ' i) :
       ρ ∘ₘ β = ∑ i ∈ s, (c i : ℝ≥0∞) • ρ' i := by
     ext t ht
-    rw [Measure.bind_apply ht ρ.aemeasurable, hβ_lintegral, Measure.finsetSum_apply,
+    rw [Measure.bind_apply ht ρ.aemeasurable, hβ_lintegral, sum_apply,
       ← Finset.sum_coe_sort s]
-    exact Finset.sum_congr rfl fun i _ ↦ by rw [hρ i, Measure.smul_apply, smul_eq_mul]
+    exact Finset.sum_congr rfl fun i _ ↦ by rw [hρ i, smul_apply, smul_eq_mul]
   calc klDiv (∑ i ∈ s, (c i : ℝ≥0∞) • μ i) (∑ i ∈ s, (c i : ℝ≥0∞) • ν i)
   _ = klDiv (κ ∘ₘ β) (η ∘ₘ β) := by rw [h_comp κ μ hκ_apply, h_comp η ν hη_apply]
   -- data processing inequality for the second projection

LeanMachineLearning/ForMathlib/MeasureTheory/Measure/Decomposition/Lebesgue.lean

@@ -46,7 +46,7 @@ lemma sub_apply_eq_rnDeriv_add_singularPart [IsFiniteMeasure μ] [IsFiniteMeasur
   swap
   · simp only [withDensity_one]
     exact mutuallySingular_singularPart μ ν
-  simp only [coe_add, Pi.add_apply]
+  simp only [FunLike.coe_add, Pi.add_apply]
   have : IsFiniteMeasure (ν.withDensity 1) := by simp only [withDensity_one]; infer_instance
   rw [add_comm, ← withDensity_sub (by fun_prop) (by fun_prop)]
   congr

LeanMachineLearning/ForMathlib/Probability/ConditionalProbability.lean

@@ -34,7 +34,7 @@ lemma sum_meas_smul_cond_fiber {X : Ω → α} (hX : Measurable X) (μ : Measure
     [IsFiniteMeasure μ] :
     Measure.sum (fun x ↦ μ (X ⁻¹' {x}) • μ[|X ⁻¹' {x}]) = μ := by
   ext s hs
-  simp_rw [Measure.sum_apply _ hs, Measure.smul_apply, smul_eq_mul, mul_comm (μ _),
+  simp_rw [Measure.sum_apply _ hs, smul_apply, smul_eq_mul, mul_comm (μ _),
     cond_mul_eq_inter (hX (.singleton _))]
   rw [← measure_iUnion (fun i j hij ↦ ((Set.disjoint_singleton.2 hij).preimage X).mono
       Set.inter_subset_left Set.inter_subset_left) fun i ↦ (hX (.singleton i)).inter hs,

LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean

@@ -280,7 +280,7 @@ lemma HasCondDistrib.hasLaw_cond (h : HasCondDistrib Y X κ μ)
   map_eq := by
     ext u hu
     rw [Measure.map_apply_of_aemeasurable (h.aemeasurable_snd.mono_ac cond_absolutelyContinuous) hu,
-      cond, Measure.smul_apply, smul_eq_mul,
+      cond, smul_apply, smul_eq_mul,
       Measure.restrict_apply₀ (h.aemeasurable_snd.restrict.nullMeasurableSet_preimage hu),
       Set.inter_comm, h.measure_inter_preimage_eq_mul_of_eqOn_const hs hκ hu, ← mul_assoc,
       ENNReal.inv_mul_cancel hμs (measure_ne_top _ _), one_mul]

LeanMachineLearning/ForMathlib/Probability/HasLaw.lean

@@ -72,7 +72,7 @@ lemma hasLaw_of_forall_hasLaw_cond [IsProbabilityMeasure P] {g : Ω → ι} (hg
     rw [← Measure.sum_meas_smul_cond_fiber hg P] at hX ⊢
     simp_rw [Measure.map_sum hX, h_eq]
     ext s hs
-    simp_rw [Measure.sum_apply _ hs, Measure.smul_apply, smul_eq_mul, ENNReal.tsum_mul_right,
+    simp_rw [Measure.sum_apply _ hs, smul_apply, smul_eq_mul, ENNReal.tsum_mul_right,
       h_univ, one_mul]
 
 end Cond

LeanMachineLearning/ForMathlib/Probability/Kernel/RadonNikodym.lean

@@ -81,7 +81,7 @@ lemma sub_apply [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)] [IsFinit
   ext s hs
   rw [sub_apply_eq_rnDeriv_add_singularPart, Kernel.withDensity_apply _ (by fun_prop),
     Kernel.singularPart_eq_singularPart_measure, Measure.sub_apply_eq_rnDeriv_add_singularPart _]
-  simp only [Measure.coe_add, Pi.add_apply]
+  simp only [FunLike.coe_add, Pi.add_apply]
   congr 2
   refine MeasureTheory.withDensity_congr_ae ?_
   filter_upwards [Kernel.rnDeriv_eq_rnDeriv_measure (κ := κ) (η := η) (a := a)] with b hb

LeanMachineLearning/Tactic/EqLift/ForMathlib/Kernel.lean

@@ -63,7 +63,7 @@ instance (κ : Kernel α β) [IsDeterministic κ] : IsSFiniteKernel κ := by
   replace h := DFunLike.congr_fun h Set.univ
   rw [comp_apply'] at h
   · simp_rw [copy_apply, Measure.dirac_apply' _ MeasurableSet.univ, indicator_univ] at h
-    simp only [Measure.coe_zero, Pi.zero_apply, Pi.one_apply, MeasureTheory.lintegral_const,
+    simp only [FunLike.coe_zero, Pi.zero_apply, Pi.one_apply, MeasureTheory.lintegral_const,
       one_mul] at h
     exact ha.ne h
   exact MeasurableSet.univ

LeanMachineLearning/Tactic/EqLift/Kernel/Lift.lean

@@ -64,15 +64,15 @@ lemma isSFinite_lift (κ : Kernel X Y) :
     · simp only [κs']
       ext a s hs
       replace h := DFunLike.congr (x := ey.symm '' s) (DFunLike.congr (x := ex.symm a) h rfl) rfl
-      rw [sum_apply, Measure.sum_apply] at h ⊢
+      rw [Kernel.sum_apply, Measure.sum_apply] at h ⊢
       · rw [lift_apply'] at h
         · convert h with x
           · simp
           · rw [image_symm]
             simp
           · simp only [coe_comap, Function.comp_apply]
             rw [map_apply' _ ey.measurable _ hs, image_symm]
-        all_goals measurability
+        measurability
       all_goals measurability
 
 instance (κ : Kernel X Y) [IsSFiniteKernel κ] : IsSFiniteKernel (lift (ex := ex) (ey := ey) κ) :=
@@ -137,7 +137,7 @@ lemma id_lift : Kernel.id (α := X') = Kernel.id.lift (ex := ex) (ey := ex) := b
   simp only [id_apply]
   rw [Measure.dirac_apply' _ hs, Measure.dirac_apply']
   · exact Set.indicator_eq_indicator (by simp) rfl
-  all_goals measurability
+  measurability
 
 lemma discard_lift : discard.{_, w} X' = (discard X).lift (ex := ex) (ey := punit) := by
   ext _ _ hs
@@ -195,19 +195,21 @@ lemma compProd_lift (κ : Kernel X Y) (η : Kernel (X × Y) Z) :
     swap
     · simp [hη, (isSFinite_lift (ex.prodCongr ey) ez η).not.mpr hη]
       simp [lift]
-    · simp only [compProd]
-      rw [← comp_lift (ex := ex.prodCongr ex) (ey := ey.prodCongr ez), ← copy_lift,
-        ← comp_lift (ex := ex.prodCongr ey), ← parallelComp_lift, ← id_lift,
-        ← comp_lift (ex := ex.prodCongr (ey.prodCongr ey)), ← parallelComp_lift, ← id_lift,
-        ← copy_lift,
-        ← comp_lift (ex := (ex.prodCongr ey).prodCongr ey),
-        ← comp_lift (ex := ez.prodCongr ey), ← parallelComp_lift, ← id_lift, ← swap_lift]
-      congr
-      simp only [lift]
-      rw [deterministic_map (MeasurableEquiv.measurable _) (MeasurableEquiv.measurable _)]
-      ext _ : 1
-      simp [comap_apply, deterministic_apply, MeasurableEquiv.prodCongr, prodAssoc]
-
+    · have := (isSFinite_lift ex ey κ).mpr hκ
+      have := (isSFinite_lift (ex.prodCongr ey) ez η).mpr hη
+      ext a s hs
+      rw [compProd_apply hs, lift_apply' _ _ _ _ hs,
+        compProd_apply ((ey.prodCongr ez).measurableSet_image.mpr hs), lift_apply,
+        map_apply _ ey.symm.measurable, lintegral_map_equiv]
+      refine lintegral_congr fun y ↦ ?_
+      rw [lift_apply' _ _ _ _ (measurable_prodMk_left hs)]
+      congr 1
+      · simp [MeasurableEquiv.prodCongr]
+      · ext z
+        simp only [image_eq_preimage_symm, Set.mem_preimage, prodCongr, MeasurableEquiv.coe_mk,
+          Equiv.prodCongr_apply, coe_toEquiv, Set.mem_image, Prod.exists, Prod.map_apply,
+          Prod.mk.injEq]
+        exact ⟨fun h ↦ ⟨_, _, h, by simp, by simp⟩, by rintro ⟨_, _, h, rfl, rfl⟩; simpa using h⟩
 
 instance {κ : Kernel X Y} [IsDeterministic κ] :
     IsDeterministic (κ.lift (ex := ex) (ey := ey)) where

lake-manifest.json

@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9d581dfff2e41de989072ea63abf3daf69311520",
+   "rev": "1b1ccf4b088b32fa3f23f2de1127433254a81e1e",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.36.0-rc2",
+   "inputRev": "1b1ccf4b088b32fa3f23f2de1127433254a81e1e",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/verso",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d4c39b228d4a06f3b00748c2c445a7b9f056a6e3",
+   "rev": "6d971e7e6b3f7d0a501c5418815aa9022edd3499",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lakefile.toml

@@ -17,7 +17,7 @@ rev = "v4.36.0-rc2"
 [[require]]
 name = "mathlib"
 scope = "leanprover-community"
-rev = "v4.36.0-rc2"
+rev = "1b1ccf4b088b32fa3f23f2de1127433254a81e1e"
 
 [[lean_lib]]
 name = "LeanMachineLearning"