-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst_2 : StandardBorelSpace β
inst_3 : Nonempty β
inst_4 : StandardBorelSpace β'
inst_5 : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
hk_meas : ∀ {s : Set γ} (hs : MeasurableSet s), MeasurableSet (k ⁻¹' s)
h_left :
  ∀ {s : Set γ} {t : Set β} {u : Set β'} (hs : MeasurableSet s) (ht : MeasurableSet t) (hu : MeasurableSet u),
    Eq (α := ℝ≥0∞)
      ((Measure.map (fun (ω : Ω) ↦ (k ω, f ω, g ω)) μ : (a : Set (γ × β × β')) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
      ((Measure.map (fun (ω : Ω) ↦ (ω, f ω, g ω)) μ : (a : Set (Ω × β × β')) → ℝ≥0∞) ((k ⁻¹' s) ×ˢ t ×ˢ u) : ℝ≥0∞)
h_right :
  ∀ {s : Set γ} {t : Set β} {u : Set β'} (hs : MeasurableSet s) (ht : MeasurableSet t) (hu : MeasurableSet u),
    Eq (α := ℝ≥0∞)
      ((Measure.bind (mα := mγ) (Measure.map k μ)
              (⇑(Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) : (a : γ) → Measure (γ × β × β')) :
            (a : Set (γ × β × β')) → ℝ≥0∞)
          (s ×ˢ t ×ˢ u) :
        ℝ≥0∞)
      (((⇑(Kernel.id ×ₖ
                    (Kernel.map (condExpKernel μ (MeasurableSpace.comap k mγ)) f ×ₖ
                      Kernel.map (condExpKernel μ (MeasurableSpace.comap k mγ)) g)) :
                (a : Ω) → Measure (Ω × β × β')) ∘ₘ
              μ.trim ⋯ :
            (a : Set (Ω × β × β')) → ℝ≥0∞)
          ((k ⁻¹' s) ×ˢ t ×ˢ u) :
        ℝ≥0∞)
h :
  ∀ {s : Set γ} {t : Set β} {u : Set β'},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u →
          Eq (α := ℝ≥0∞)
            ((Measure.map (fun (ω : Ω) ↦ (k ω, f ω, g ω)) μ : (a : Set (γ × β × β')) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
            ((Measure.bind (mα := mγ) (Measure.map k μ)
                    (⇑(Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) : (a : γ) → Measure (γ × β × β')) :
                  (a : Set (γ × β × β')) → ℝ≥0∞)
                (s ×ˢ t ×ˢ u) :
              ℝ≥0∞)
t : Set β
u : Set β'
s : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
h₁ :
  Eq (α := ℝ≥0∞)
    ((Measure.map (fun (ω : Ω) ↦ (ω, f ω, g ω)) μ : (a : Set (Ω × β × β')) → ℝ≥0∞) ((k ⁻¹' s) ×ˢ t ×ˢ u) : ℝ≥0∞)
    ((Measure.map (fun (ω : Ω) ↦ (k ω, f ω, g ω)) μ : (a : Set (γ × β × β')) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((Measure.map (fun (ω : Ω) ↦ (ω, f ω, g ω)) μ : (a : Set (Ω × β × β')) → ℝ≥0∞) ((k ⁻¹' s) ×ˢ t ×ˢ u) : ℝ≥0∞)
    (((⇑(Kernel.id ×ₖ
                  (Kernel.map (condExpKernel μ (MeasurableSpace.comap k inferInstance)) f ×ₖ
                    Kernel.map (condExpKernel μ (MeasurableSpace.comap k inferInstance)) g)) :
              (a : Ω) → Measure (Ω × β × β')) ∘ₘ
            μ.trim ⋯ :
          (a : Set (Ω × β × β')) → ℝ≥0∞)
        ((k ⁻¹' s) ×ˢ t ×ˢ u) :
      ℝ≥0∞)
have h₂ : Eq (α := ℝ≥0∞)
  (((⇑(Kernel.id ×ₖ
                (Kernel.map (condExpKernel μ (MeasurableSpace.comap k inferInstance)) f ×ₖ
                  Kernel.map (condExpKernel μ (MeasurableSpace.comap k inferInstance)) g)) :
            (a : Ω) → Measure (Ω × β × β')) ∘ₘ
          μ.trim sorry :
        (a : Set (Ω × β × β')) → ℝ≥0∞)
      ((k ⁻¹' s) ×ˢ t ×ˢ u) :
    ℝ≥0∞)
  ((Measure.bind (mα := mγ) (Measure.map k μ)
          (⇑(Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) : (a : γ) → Measure (γ × β × β')) :
        (a : Set (γ × β × β')) → ℝ≥0∞)
      (s ×ˢ t ×ˢ u) :
    ℝ≥0∞)
Tactic: convert! h hs ht hu