-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
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)) μ))
⊢ (∀ᵐ (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)) μ)
have 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 μ)
Tactic: rw [condDistrib, ← hf.ae_integrable_condKernel_iff, Measure.fst_map_prodMk₀ hY]