-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst : ρ.IsCondKernel ρCond
inst_1 : IsFiniteMeasure ρ
inst_2 : MeasurableSingletonClass α
x : α
hx : Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set Ω
hs : MeasurableSet s
this : IsSFiniteKernel ρCond
have :
  ∀ (a : α),
    Eq (α := ℝ≥0∞)
      ((((ρCond : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          (Prod.mk a ⁻¹' SProd.sprod (α := Set α) {x} s) :
        ℝ≥0∞)
      (indicator {x} (fun (x : α) ↦ (((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s) a : ℝ≥0∞)
have₁ :
  ∀
    (this :
      ∀ (a : α),
        Eq (α := ℝ≥0∞)
          ((((ρCond : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
              (Prod.mk a ⁻¹' SProd.sprod (α := Set α) {x} s) :
            ℝ≥0∞)
          (indicator {x} (fun (x : α) ↦ (((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s) a :
            ℝ≥0∞)),
    (((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s =
      HMul.hMul (α := ℝ≥0∞) (((ρ.fst : (a : Set α) → ℝ≥0∞) {x})⁻¹ : ℝ≥0∞)
        (∫⁻ (a : α),
          (((ρCond : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
            (Prod.mk a ⁻¹' SProd.sprod (α := Set α) {x} s) ∂ρ.fst)
have₂ :
  ∀ (a : α),
    Eq (α := ℝ≥0∞)
      ((((ρCond : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          (Prod.mk a ⁻¹' SProd.sprod (α := Set α) {x} s) :
        ℝ≥0∞)
      (indicator {x} (fun (x : α) ↦ (((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s) a : ℝ≥0∞)
have₃ have₄ :
  ∀
    (this :
      ∀ (a : α),
        Eq (α := ℝ≥0∞)
          ((((ρCond : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
              (Prod.mk a ⁻¹' SProd.sprod (α := Set α) {x} s) :
            ℝ≥0∞)
          (indicator {x} (fun (x : α) ↦ (((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s) a :
            ℝ≥0∞)),
    (((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s =
      HMul.hMul (α := ℝ≥0∞) (((ρ.fst : (a : Set α) → ℝ≥0∞) {x})⁻¹ : ℝ≥0∞)
        (∫⁻ (a : α),
          (((ρCond : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
            (Prod.mk a ⁻¹' SProd.sprod (α := Set α) {x} s) ∂ρ.fst)
have₅ :
  ∀
    (this :
      ∀ (a : α),
        Eq (α := ℝ≥0∞)
          ((((ρCond : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
              (Prod.mk a ⁻¹' SProd.sprod (α := Set α) {x} s) :
            ℝ≥0∞)
          (indicator {x} (fun (x : α) ↦ (((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s) a :
            ℝ≥0∞)),
    (((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s =
      HMul.hMul (α := ℝ≥0∞) (((ρ.fst : (a : Set α) → ℝ≥0∞) {x})⁻¹ : ℝ≥0∞)
        (∫⁻ (a : α),
          indicator {x} (fun (x : α) ↦ (((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s) a ∂ρ.fst)
have₆ :
  ∀
    (this :
      ∀ (a : α),
        Eq (α := ℝ≥0∞)
          ((((ρCond : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
              (Prod.mk a ⁻¹' SProd.sprod (α := Set α) {x} s) :
            ℝ≥0∞)
          (indicator {x} (fun (x : α) ↦ (((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s) a :
            ℝ≥0∞)),
    (((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s =
      HMul.hMul (α := ℝ≥0∞) (((ρ.fst : (a : Set α) → ℝ≥0∞) {x})⁻¹ : ℝ≥0∞)
        (∫⁻ (a : α) in {x}, (((ρCond : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s ∂ρ.fst)
have₇ :
  ∀
    (this :
      ∀ (a : α),
        Eq (α := ℝ≥0∞)
          ((((ρCond : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
              (Prod.mk a ⁻¹' SProd.sprod (α := Set α) {x} s) :
            ℝ≥0∞)
          (indicator {x} (fun (x : α) ↦ (((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s) a :
            ℝ≥0∞)),
    (((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s =
      HMul.hMul (α := ℝ≥0∞) (((ρ.fst : (a : Set α) → ℝ≥0∞) {x})⁻¹ : ℝ≥0∞)
        (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞)
          ((((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞))
⊢ (((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s =
    HMul.hMul (α := ℝ≥0∞) (((ρ.fst : (a : Set α) → ℝ≥0∞) {x})⁻¹ : ℝ≥0∞)
      (∫⁻ (a : α),
        (((ρCond : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          (Prod.mk a ⁻¹' SProd.sprod (α := Set α) {x} s) ∂ρ.fst)

Tactic:
classical
  have (a : _) : ρCond a (Prod.mk a ⁻¹' {x} ×ˢ s) = ({x} : Set α).indicator (ρCond · s) a := by
    obtain rfl | hax := eq_or_ne a x
    · simp only [singleton_prod, mem_singleton_iff, indicator_of_mem]
      congr with y
      simp
    · simp only [singleton_prod, mem_singleton_iff, hax, not_false_eq_true, indicator_of_notMem]
      have : Prod.mk a ⁻¹' Prod.mk x '' s = ∅ := by ext y; simp [Ne.symm hax]
      simp only [this, measure_empty]
  simp_rw [this]
  rw [MeasureTheory.lintegral_indicator (measurableSet_singleton x)]
  simp only [Measure.restrict_singleton, lintegral_smul_measure, lintegral_dirac, smul_eq_mul]
  rw [← mul_assoc, ENNReal.inv_mul_cancel hx (measure_ne_top _ _), one_mul]

Premises used: MeasureTheory.Measure.restrict_singleton, MeasureTheory.lintegral_smul_measure, MeasurableSingletonClass.measurableSet_singleton, mul_assoc, MeasureTheory.measure_ne_top, MeasureTheory.lintegral_dirac, MeasureTheory.lintegral_indicator, ENNReal.inv_mul_cancel, smul_eq_mul, one_mul