-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
hA : MeasurableSet A
this : IsFiniteKernel κ
hgen : mγ = generateFrom {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
hpi : IsPiSystem.{u_3} (α := γ) {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
empty :
  (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) ∅) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (SProd.sprod (α := Set γ) ∅ s)
basic :
  ∀ (s_1 : Set γ) (hs : Membership.mem (γ := Set (Set γ)) {s : Set γ | ∃ (n : ℕ), MeasurableSet s} s_1),
    (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) s_1) fun (x : γ) ↦ κ.density ν a x s) =
      Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (s_1 ×ˢ s)
compl :
  ∀ (A : Set γ) (hA : MeasurableSet A)
    (hA_eq :
      (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s) =
        Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s)),
    (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) Aᶜ) fun (x : γ) ↦ κ.density ν a x s) =
      Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (Aᶜ ×ˢ s)
iUnion :
  ∀ (f : ℕ → Set γ) (hf_disj : Pairwise (Function.onFun Disjoint f)) (hf : ∀ (i : ℕ), MeasurableSet (f i))
    (h_eq :
      ∀ (i : ℕ),
        (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) (f i)) fun (x : γ) ↦ κ.density ν a x s) =
          Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (f i ×ˢ s)),
    (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) (⋃ (i : ℕ), f i)) fun (x : γ) ↦
        κ.density ν a x s) =
      Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a)
        (SProd.sprod (α := Set γ) (⋃ (i : ℕ), f i) s)
⊢ (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s)

Tactic:
induction A, hA using induction_on_inter hgen hpi with
  | empty => simp
  | basic s hs =>
    rcases hs with ⟨n, hn⟩
    exact setIntegral_density_of_measurableSet hκν n a hs hn
  | compl A hA hA_eq =>
    have h := integral_add_compl hA (integrable_density hκν a hs)
    rw [hA_eq, integral_density hκν a hs] at h
    have : Aᶜ ×ˢ s = univ ×ˢ s \ A ×ˢ s := by
      rw [prod_diff_prod, compl_eq_univ_diff]
      simp
    rw [this, measureReal_def,
      measure_diff (by intro; simp) (hA.prod hs).nullMeasurableSet (measure_ne_top (κ a) _),
      ENNReal.toReal_sub_of_le (measure_mono (by intro x; simp)) (measure_ne_top _ _)]
    rw [eq_tsub_iff_add_eq_of_le, add_comm]
    · exact h
    · gcongr <;> simp
  | iUnion f hf_disj hf h_eq =>
    rw [integral_iUnion hf hf_disj (integrable_density hκν _ hs).integrableOn]
    simp_rw [h_eq, measureReal_def]
    rw [← ENNReal.tsum_toReal_eq (fun _ ↦ measure_ne_top _ _)]
    congr
    rw [iUnion_prod_const, measure_iUnion]
    · exact hf_disj.mono fun _ _ h ↦ h.set_prod_left _ _
    · exact fun i ↦ (hf i).prod hs

Premises used: Compl.compl, MeasurableSet.nullMeasurableSet, MeasureTheory.measure_ne_top, Set.iUnion_prod_const, MeasurableSet.prod, add_comm, MeasureTheory.measure_iUnion, ProbabilityTheory.Kernel.integral_density, ENNReal.toReal_sub_of_le, MeasureTheory.measure_diff, MeasureTheory.measure_mono, MeasureTheory.measureReal_def, eq_tsub_iff_add_eq_of_le, DFunLike.coe, Set.iUnion, ENNReal.tsum_toReal_eq