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)
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)

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

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)
h_right :
  ∀ {s : Set γ} {t : Set β} {u : Set β'},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u →
          (⇑(Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) ∘ₘ Measure.map k μ) (s ×ˢ t ×ˢ u) =
            (⇑(Kernel.id ×ₖ
                    ((condExpKernel μ (MeasurableSpace.comap k mγ)).map f ×ₖ
                      (condExpKernel μ (MeasurableSpace.comap k mγ)).map g)) ∘ₘ
                μ.trim ⋯)
              ((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)