Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝³ : StandardBorelSpace β
inst✝² : Nonempty β
inst✝¹ : StandardBorelSpace β'
inst✝ : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
hk_meas : ∀ {s : Set γ}, MeasurableSet s → MeasurableSet (k ⁻¹' s)
⊢ (∀ {s : Set Ω} {t : Set β} {u : Set β'},
      MeasurableSet s →
        MeasurableSet t →
          MeasurableSet u →
            (Measure.map (fun ω ↦ (ω, f ω, g ω)) μ) (s ×ˢ t ×ˢ u) =
              (⇑(Kernel.id ×ₖ
                      ((condExpKernel μ (MeasurableSpace.comap k inferInstance)).map f ×ₖ
                        (condExpKernel μ (MeasurableSpace.comap k inferInstance)).map g)) ∘ₘ
                  μ.trim ⋯)
                (s ×ˢ t ×ˢ u)) ↔
    ∀ {s : Set γ} {t : Set β} {u : Set β'},
      MeasurableSet s →
        MeasurableSet t →
          MeasurableSet u →
            (Measure.map (fun ω ↦ (k ω, f ω, g ω)) μ) (s ×ˢ t ×ˢ u) =
              (⇑(Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) ∘ₘ Measure.map k μ) (s ×ˢ t ×ˢ u)

Tactic:
have h_left {s : Set γ} {t : Set β} {u : Set β'} (hs : MeasurableSet s) (ht : MeasurableSet t)
      (hu : MeasurableSet u) :
      (μ.map (fun ω ↦ (k ω, f ω, g ω))) (s ×ˢ t ×ˢ u) =
        (@Measure.map _ _ _ ((mγ.comap k).prod inferInstance)
          (fun ω ↦ (ω, f ω, g ω)) μ) ((k ⁻¹' s) ×ˢ t ×ˢ u) := by
    rw [Measure.map_apply (by fun_prop) (hs.prod (ht.prod hu)),
      Measure.map_apply _ ((hk_meas hs).prod (ht.prod hu))]
    · simp [Set.mk_preimage_prod]
    · exact (measurable_id.mono le_rfl hk.comap_le).prodMk (by fun_prop)

Goal state after:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝³ : StandardBorelSpace β
inst✝² : Nonempty β
inst✝¹ : StandardBorelSpace β'
inst✝ : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
hk_meas : ∀ {s : Set γ}, MeasurableSet s → MeasurableSet (k ⁻¹' s)
h_left :
  ∀ {s : Set γ} {t : Set β} {u : Set β'},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u →
          (Measure.map (fun ω ↦ (k ω, f ω, g ω)) μ) (s ×ˢ t ×ˢ u) =
            (Measure.map (fun ω ↦ (ω, f ω, g ω)) μ) ((k ⁻¹' s) ×ˢ t ×ˢ u)
⊢ (∀ {s : Set Ω} {t : Set β} {u : Set β'},
      MeasurableSet s →
        MeasurableSet t →
          MeasurableSet u →
            (Measure.map (fun ω ↦ (ω, f ω, g ω)) μ) (s ×ˢ t ×ˢ u) =
              (⇑(Kernel.id ×ₖ
                      ((condExpKernel μ (MeasurableSpace.comap k inferInstance)).map f ×ₖ
                        (condExpKernel μ (MeasurableSpace.comap k inferInstance)).map g)) ∘ₘ
                  μ.trim ⋯)
                (s ×ˢ t ×ˢ u)) ↔
    ∀ {s : Set γ} {t : Set β} {u : Set β'},
      MeasurableSet s →
        MeasurableSet t →
          MeasurableSet u →
            (Measure.map (fun ω ↦ (k ω, f ω, g ω)) μ) (s ×ˢ t ×ˢ u) =
              (⇑(Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) ∘ₘ Measure.map k μ) (s ×ˢ t ×ˢ u)