-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
b : β
have :
  ∀ (x : γ),
    ∫⁻ (y : β),
        (((swap γ β : (a : γ × β) → Measure (β × γ)) (x, y) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
          s ∂Measure.dirac b =
      (Prod.mk b ⁻¹' s).indicator 1 x
e_f :
  ∀
    (h_int :
      ∀ (x : γ),
        ∫⁻ (y : β),
            (((swap γ β : (a : γ × β) → Measure (β × γ)) (x, y) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
              s ∂Measure.dirac b =
          (Prod.mk b ⁻¹' s).indicator 1 x),
    ∫⁻ (x : γ),
        ∫⁻ (y : β),
          (((swap γ β : (a : γ × β) → Measure (β × γ)) (x, y) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
            s ∂Measure.dirac ((a, b), b).2 ∂(η : (a : α × β) → Measure γ) ((a, b), b).1 =
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)
have₁ :
  ∀ (x : γ),
    ∫⁻ (y : β),
        (((swap γ β : (a : γ × β) → Measure (β × γ)) (x, y) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
          s ∂Measure.dirac b =
      (Prod.mk b ⁻¹' s).indicator 1 x
e_f₁ e_f₂ :
  ∀
    (h_int :
      ∀ (x : γ),
        ∫⁻ (y : β),
            (((swap γ β : (a : γ × β) → Measure (β × γ)) (x, y) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
              s ∂Measure.dirac b =
          (Prod.mk b ⁻¹' s).indicator 1 x),
    ∫⁻ (x : γ),
        ∫⁻ (y : β),
          (((swap γ β : (a : γ × β) → Measure (β × γ)) (x, y) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
            s ∂Measure.dirac ((a, b), b).2 ∂(η : (a : α × β) → Measure γ) ((a, b), b).1 =
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)
e_f₃ :
  ∀
    (h_int :
      ∀ (x : γ),
        ∫⁻ (y : β),
            (((swap γ β : (a : γ × β) → Measure (β × γ)) (x, y) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
              s ∂Measure.dirac b =
          (Prod.mk b ⁻¹' s).indicator 1 x),
    ∫⁻ (x : γ), (Prod.mk b ⁻¹' s).indicator 1 x ∂(η : (a : α × β) → Measure γ) (a, b) =
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)
e_f₄ :
  ∀
    (h_int :
      ∀ (x : γ),
        ∫⁻ (y : β),
            (((swap γ β : (a : γ × β) → Measure (β × γ)) (x, y) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
              s ∂Measure.dirac b =
          (Prod.mk b ⁻¹' s).indicator 1 x),
    MeasurableSet (Prod.mk b ⁻¹' s)
⊢ ∫⁻ (x : γ),
      ∫⁻ (y : β),
        (((swap γ β : (a : γ × β) → Measure (β × γ)) (x, y) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
          s ∂Measure.dirac ((a, b), b).2 ∂(η : (a : α × β) → Measure γ) ((a, b), b).1 =
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)

Tactic:
classical
  have h_int x : ∫⁻ y, swap γ β (x, y) s ∂Measure.dirac b = (Prod.mk b ⁻¹' s).indicator 1 x := by
    rw [lintegral_dirac']
    · simp [swap_apply' _ hs, Set.indicator_apply]
    · simpa [swap_apply' _ hs, Prod.swap_prod_mk] using
        measurable_const.indicator (measurable_prodMk_right hs)
  simp_rw [h_int]
  rw [lintegral_indicator_one]
  exact measurable_prodMk_left hs

Premises used: MeasureTheory.lintegral_indicator_one, measurable_prodMk_left