-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
hs : MeasurableSet s
empty :
  ∫⁻ (b : β),
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' ∅) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) ∅
basic :
  ∀ (s : Set (β × ℝ))
    (hs :
      Membership.mem (γ := Set (Set (β × ℝ)))
        (image2 (fun (x1 : Set β) (x2 : Set ℝ) ↦ x1 ×ˢ x2) {s : Set β | MeasurableSet s} {t : Set ℝ | MeasurableSet t})
        s),
    ∫⁻ (b : β),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' s) ∂(ν : (a : α) → Measure β) a =
      (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) s
compl :
  ∀ (t : Set (β × ℝ)) (ht : MeasurableSet t)
    (ht_eq :
      ∫⁻ (b : β),
          (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
            (Prod.mk b ⁻¹' t) ∂(ν : (a : α) → Measure β) a =
        (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) t),
    ∫⁻ (b : β),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' tᶜ) ∂(ν : (a : α) → Measure β) a =
      (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) tᶜ
iUnion :
  ∀ (f' : ℕ → Set (β × ℝ)) (hf_disj : Pairwise (Disjoint on f')) (hf_meas : ∀ (i : ℕ), MeasurableSet (f' i))
    (hf_eq :
      ∀ (i : ℕ),
        ∫⁻ (b : β),
            (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
              (Prod.mk b ⁻¹' f' i) ∂(ν : (a : α) → Measure β) a =
          (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (f' i)),
    ∫⁻ (b : β),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' ⋃ (i : ℕ), f' i) ∂(ν : (a : α) → Measure β) a =
      (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (⋃ (i : ℕ), f' i)
⊢ ∫⁻ (b : β),
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) s

Tactic:
induction s, hs
    using MeasurableSpace.induction_on_inter generateFrom_prod.symm isPiSystem_prod with
  | empty =>
    simp only [preimage_empty, measure_empty, lintegral_const, zero_mul]
  | basic s hs =>
    rcases hs with ⟨t₁, ht₁, t₂, ht₂, rfl⟩
    simp only [mem_setOf_eq] at ht₁ ht₂
    rw [← lintegral_add_compl _ ht₁]
    have h_eq1 : ∫⁻ x in t₁, hf.toKernel f (a, x) (Prod.mk x ⁻¹' t₁ ×ˢ t₂) ∂(ν a)
        = ∫⁻ x in t₁, hf.toKernel f (a, x) t₂ ∂(ν a) := by
      refine setLIntegral_congr_fun ht₁ (fun a ha ↦ ?_)
      rw [mk_preimage_prod_right ha]
    have h_eq2 :
        ∫⁻ x in t₁ᶜ, hf.toKernel f (a, x) (Prod.mk x ⁻¹' t₁ ×ˢ t₂) ∂(ν a) = 0 := by
      suffices h_eq_zero :
          ∀ x ∈ t₁ᶜ, hf.toKernel f (a, x) (Prod.mk x ⁻¹' t₁ ×ˢ t₂) = 0 by
        rw [setLIntegral_congr_fun ht₁.compl h_eq_zero]
        simp only [lintegral_const, zero_mul]
      intro a hat₁
      rw [mem_compl_iff] at hat₁
      simp only [hat₁, not_false_eq_true, mk_preimage_prod_right_eq_empty, measure_empty]
    rw [h_eq1, h_eq2, add_zero]
    exact setLIntegral_toKernel_prod hf a ht₁ ht₂
  | compl t ht ht_eq =>
    calc ∫⁻ b, hf.toKernel f (a, b) (Prod.mk b ⁻¹' tᶜ) ∂(ν a)
      = ∫⁻ b, hf.toKernel f (a, b) (Prod.mk b ⁻¹' t)ᶜ ∂(ν a) := rfl
    _ = ∫⁻ b, hf.toKernel f (a, b) univ
          - hf.toKernel f (a, b) (Prod.mk b ⁻¹' t) ∂(ν a) := by
        congr with x : 1
        exact measure_compl (measurable_prodMk_left ht)
          (measure_ne_top (hf.toKernel f (a, x)) _)
    _ = ∫⁻ x, hf.toKernel f (a, x) univ ∂(ν a) -
          ∫⁻ x, hf.toKernel f (a, x) (Prod.mk x ⁻¹' t) ∂(ν a) := by
        have h_le : (fun x ↦ hf.toKernel f (a, x) (Prod.mk x ⁻¹' t))
              ≤ᵐ[ν a] fun x ↦ hf.toKernel f (a, x) univ :=
          Eventually.of_forall fun _ ↦ measure_mono (subset_univ _)
        rw [lintegral_sub _ _ h_le]
        · exact Kernel.measurable_kernel_prodMk_left' ht a
        refine ((lintegral_mono_ae h_le).trans_lt ?_).ne
        rw [lintegral_toKernel_univ hf]
        exact measure_lt_top _ univ
    _ = κ a univ - κ a t := by rw [ht_eq, lintegral_toKernel_univ hf]
    _ = κ a tᶜ := (measure_compl ht (measure_ne_top _ _)).symm
  | iUnion f' hf_disj hf_meas hf_eq =>
    have h_eq : ∀ a, Prod.mk a ⁻¹' ⋃ i, f' i = ⋃ i, Prod.mk a ⁻¹' f' i := by
      simp only [preimage_iUnion, implies_true]
    simp_rw [h_eq]
    have h_disj : ∀ a, Pairwise (Disjoint on fun i ↦ Prod.mk a ⁻¹' f' i) := by
      intro _ _ _ hij
      exact Disjoint.preimage _ (hf_disj hij)
    calc ∫⁻ b, hf.toKernel f (a, b) (⋃ i, Prod.mk b ⁻¹' f' i) ∂(ν a)
      = ∫⁻ b, ∑' i, hf.toKernel f (a, b) (Prod.mk b ⁻¹' f' i) ∂(ν a) := by
          congr with x : 1
          rw [measure_iUnion (h_disj x) fun i ↦ measurable_prodMk_left (hf_meas i)]
    _ = ∑' i, ∫⁻ b, hf.toKernel f (a, b) (Prod.mk b ⁻¹' f' i) ∂(ν a) :=
          lintegral_tsum fun i ↦ (Kernel.measurable_kernel_prodMk_left' (hf_meas i) a).aemeasurable
    _ = ∑' i, κ a (f' i) := by simp_rw [hf_eq]
    _ = κ a (iUnion f') := (measure_iUnion hf_disj hf_meas).symm

Premises used: MeasureTheory.lintegral_const, Compl.compl, Set.univ, MulZeroClass.zero_mul, MeasureTheory.measure_empty, Set.mem_setOf_eq, Set.preimage_empty, add_zero, DFunLike.coe, Set.iUnion, rfl