-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (hypothesis)
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∞)
⊢ (∀ {s : Set Ω} {t : Set β} {u : Set β'},
      MeasurableSet s →
        MeasurableSet t →
          MeasurableSet u →
            Eq (α := ℝ≥0∞)
              ((Measure.map (fun (ω : Ω) ↦ (ω, f ω, g ω)) μ : (a : Set (Ω × β × β')) → ℝ≥0∞) (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∞)
                  (s ×ˢ t ×ˢ u) :
                ℝ≥0∞)) ↔
    ∀ {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∞)
have 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 sorry :
          (a : Set (Ω × β × β')) → ℝ≥0∞)
        ((k ⁻¹' s) ×ˢ t ×ˢ u) :
      ℝ≥0∞)
Tactic: have h_right {s : Set γ} {t : Set β} {u : Set β'} (hs : MeasurableSet s) (ht : MeasurableSet t)
      (hu : MeasurableSet u) :
      ((Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) ∘ₘ μ.map k) (s ×ˢ t ×ˢ u) =
        ((Kernel.id ×ₖ
          ((condExpKernel μ (mγ.comap k)).map f ×ₖ (condExpKernel μ (mγ.comap k)).map g)) ∘ₘ
        μ.trim hk.comap_le) ((k ⁻¹' s) ×ˢ t ×ˢ u) := by
    rw [Measure.bind_apply ((hk_meas hs).prod (ht.prod hu)) (by fun_prop),
      Measure.bind_apply (hs.prod (ht.prod hu)) (by fun_prop), lintegral_map ?_ (by fun_prop),
      lintegral_trim]
    rotate_left
    · exact Kernel.measurable_coe _ ((hk_meas hs).prod (ht.prod hu))
    · exact Kernel.measurable_coe _ (hs.prod (ht.prod hu))
    refine lintegral_congr_ae ?_
    filter_upwards [condDistrib_apply_ae_eq_condExpKernel_map hf hk ht,
      condDistrib_apply_ae_eq_condExpKernel_map hg hk hu] with a haX haT
    simp only [Kernel.prod_apply_prod, Kernel.id_apply, Measure.dirac_apply' _ hs]
    rw [@Measure.dirac_apply' _ (mγ.comap k) _ _ (hk_meas hs)]
    congr