-- Module: Mathlib.Probability.Kernel.CondDistrib
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst_4 : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst_5 : NormedSpace ℝ F
inst_6 : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y μ
hf_int : @Integrable _ _ _ _ Prod.instMeasurableSpace f (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)
hf_int' : Integrable.{u_4, u_1} (ε := F) (fun (a : α) ↦ f (X a, Y a)) μ
t : Set β
ht : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' t) : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_2 :
  Eq.{u_4 + 1} (α := F)
    (@integral _ _ _ _ mβ (Measure.restrict (Measure.map X μ) t) fun (y : β) ↦
      @integral _ _ _ _ inst (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) y) fun (y_1 : Ω) ↦ f (y, y_1))
    (∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ)
refine_2₁ :
  Eq.{u_4 + 1} (α := F)
    (@integral _ _ _ _ mβ
      (Measure.restrict (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)) t) fun (y : β) ↦
      @integral _ _ _ _ inst (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) y) fun (y_1 : Ω) ↦ f (y, y_1))
    (∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ)
refine_2₂ :
  Eq.{u_4 + 1} (α := F)
    (@integral _ _ _ _ mβ
      (Measure.restrict (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)) t) fun (y : β) ↦
      @integral _ _ _ _ inst ((Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) : (a : β) → Measure Ω) y)
        fun (y_1 : Ω) ↦ f (y, y_1))
    (∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ)
refine_2₃ :
  Eq.{u_4 + 1} (α := F)
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.restrict (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) (SProd.sprod (β := Set Ω) t univ)) fun (x : β × Ω) ↦
      f x)
    (∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ)
refine_2₄ :
  Eq.{u_4 + 1} (α := F) (∫ (x : α) in (fun (a : α) ↦ (X a, Y a)) ⁻¹' SProd.sprod (β := Set Ω) t univ, f (X x, Y x) ∂μ)
    (∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ)
refine_2₅ :
  Eq.{u_4 + 1} (α := F) (∫ (x : α) in X ⁻¹' t ∩ Y ⁻¹' univ, f (X x, Y x) ∂μ) (∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ)
refine_2₆ : Eq.{u_4 + 1} (α := F) (∫ (x : α) in X ⁻¹' t ∩ univ, f (X x, Y x) ∂μ) (∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ)
refine_2₇ refine_2₈ :
  Eq.{u_4 + 1} (α := F) (∫ (x : α) in X ⁻¹' t, f (X x, Y x) ∂μ) (∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ)
⊢ Eq.{u_4 + 1} (α := F)
    (@integral _ _ _ _ mβ (Measure.map X (μ.restrict (X ⁻¹' t))) fun (y : β) ↦
      @integral _ _ _ _ inst (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) y) fun (y_1 : Ω) ↦ f (y, y_1))
    (∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ)

Tactic:
rw [← Measure.restrict_map hX ht, ← Measure.fst_map_prodMk₀ hY, condDistrib,
      Measure.setIntegral_condKernel_univ_right ht hf_int.integrableOn,
      setIntegral_map (ht.prod MeasurableSet.univ) hf_int.1 (hX.aemeasurable.prodMk hY),
      mk_preimage_prod, preimage_univ, inter_univ]

Premises used: Measurable.aemeasurable, Set.inter_univ, MeasureTheory.Measure.restrict_map, MeasureTheory.Measure.setIntegral_condKernel_univ_right, MeasureTheory.setIntegral_map, ProbabilityTheory.condDistrib, MeasurableSet.prod, And.left, AEMeasurable.prodMk, MeasureTheory.Measure.fst_map_prodMk₀, Set.preimage_univ, MeasureTheory.Integrable.integrableOn, MeasurableSet.univ, Set.mk_preimage_prod