-- 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
hY : AEMeasurable Y μ
hf : AEStronglyMeasurable (m₀ := Prod.instMeasurableSpace) f (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)
rw :
  (∀ᵐ (a : β) ∂Measure.map X μ,
        @Integrable.{u_4, u_3} F _ _ _ inst (fun (ω : Ω) ↦ f (a, ω))
          ((Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) : (a : β) → Measure Ω) a)) ∧
      @Integrable ℝ _ _ _ mβ
        (fun (a : β) ↦
          @integral _ _ _ _ inst
            ((Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) : (a : β) → Measure Ω) a) fun (ω : Ω) ↦
            ‖f (a, ω)‖)
        (Measure.map X μ) ↔
    @Integrable _ _ _ _ Prod.instMeasurableSpace f (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)
rw₁ :
  (∀ᵐ (a : β) ∂Measure.map X μ,
        @Integrable.{u_4, u_3} F _ _ _ inst (fun (ω : Ω) ↦ f (a, ω))
          ((Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) : (a : β) → Measure Ω) a)) ∧
      @Integrable ℝ _ _ _ mβ
        (fun (a : β) ↦
          @integral _ _ _ _ inst
            ((Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) : (a : β) → Measure Ω) a) fun (ω : Ω) ↦
            ‖f (a, ω)‖)
        (Measure.map X μ) ↔
    (∀ᵐ (a : β) ∂Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ),
        @Integrable.{u_4, u_3} F _ _ _ inst (fun (ω : Ω) ↦ f (a, ω))
          ((Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) : (a : β) → Measure Ω) a)) ∧
      @Integrable ℝ _ _ _ mβ
        (fun (a : β) ↦
          @integral _ _ _ _ inst
            ((Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) : (a : β) → Measure Ω) a) fun (ω : Ω) ↦
            ‖f (a, ω)‖)
        (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ))
rw₂ rw₃ :
  (∀ᵐ (a : β) ∂Measure.map X μ,
        @Integrable.{u_4, u_3} F _ _ _ inst (fun (ω : Ω) ↦ f (a, ω))
          ((Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) : (a : β) → Measure Ω) a)) ∧
      @Integrable ℝ _ _ _ mβ
        (fun (a : β) ↦
          @integral _ _ _ _ inst
            ((Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) : (a : β) → Measure Ω) a) fun (ω : Ω) ↦
            ‖f (a, ω)‖)
        (Measure.map X μ) ↔
    (∀ᵐ (a : β) ∂Measure.map X μ,
        @Integrable.{u_4, u_3} F _ _ _ inst (fun (ω : Ω) ↦ f (a, ω))
          ((Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) : (a : β) → Measure Ω) a)) ∧
      @Integrable ℝ _ _ _ mβ
        (fun (a : β) ↦
          @integral _ _ _ _ inst
            ((Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) : (a : β) → Measure Ω) a) fun (ω : Ω) ↦
            ‖f (a, ω)‖)
        (Measure.map X μ)
⊢ (∀ᵐ (a : β) ∂Measure.map X μ,
        @Integrable.{u_4, u_3} F _ _ _ inst (fun (ω : Ω) ↦ f (a, ω))
          (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) a)) ∧
      @Integrable ℝ _ _ _ mβ
        (fun (a : β) ↦
          @integral _ _ _ _ inst (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) a) fun (ω : Ω) ↦ ‖f (a, ω)‖)
        (Measure.map X μ) ↔
    @Integrable _ _ _ _ Prod.instMeasurableSpace f (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)

Tactic:
rw [condDistrib, ← hf.ae_integrable_condKernel_iff, Measure.fst_map_prodMk₀ hY]

Premises used: MeasureTheory.AEStronglyMeasurable.ae_integrable_condKernel_iff, ProbabilityTheory.condDistrib, MeasureTheory.Measure.fst_map_prodMk₀