-- Module: Mathlib.Probability.Independence.Conditional
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 β'
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
h :
  ∀ (a : Ω)
    (haX :
      Eq (α := ℝ≥0∞)
        (((((condDistrib f k μ : Kernel γ β) : (a : γ) → Measure β) (k a) : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
        (((((Kernel.map (condExpKernel μ (MeasurableSpace.comap k mγ)) f : Kernel Ω β) : (a : Ω) → Measure β) a :
                Measure β) :
              (a : Set β) → ℝ≥0∞)
            t :
          ℝ≥0∞))
    (haT :
      Eq (α := ℝ≥0∞)
        (((((condDistrib g k μ : Kernel γ β') : (a : γ) → Measure β') (k a) : Measure β') : (a : Set β') → ℝ≥0∞) u :
          ℝ≥0∞)
        (((((Kernel.map (condExpKernel μ (MeasurableSpace.comap k mγ)) g : Kernel Ω β') : (a : Ω) → Measure β') a :
                Measure β') :
              (a : Set β') → ℝ≥0∞)
            u :
          ℝ≥0∞)),
    Eq (α := ℝ≥0∞)
      ((((Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ) : (a : γ) → Measure (γ × β × β')) (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 (Ω × β × β'))
                a :
              Measure (Ω × β × β')) :
            (a : Set (Ω × β × β')) → ℝ≥0∞)
          ((k ⁻¹' s) ×ˢ t ×ˢ u) :
        ℝ≥0∞)
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞)
    (fun (a : Ω) ↦
      (((Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ) : (a : γ) → Measure (γ × β × β')) (k a) :
            Measure (γ × β × β')) :
          (a : Set (γ × β × β')) → ℝ≥0∞)
        (s ×ˢ t ×ˢ u))
    fun (a : Ω) ↦
    (((Kernel.id ×ₖ
                (Kernel.map (condExpKernel μ (MeasurableSpace.comap k mγ)) f ×ₖ
                  Kernel.map (condExpKernel μ (MeasurableSpace.comap k mγ)) g) :
              (a : Ω) → Measure (Ω × β × β'))
            a :
          Measure (Ω × β × β')) :
        (a : Set (Ω × β × β')) → ℝ≥0∞)
      ((k ⁻¹' s) ×ˢ t ×ˢ u)

Tactic:
filter_upwards [condDistrib_apply_ae_eq_condExpKernel_map hf hk ht,
      condDistrib_apply_ae_eq_condExpKernel_map hg hk hu] with a haX haT

Premises used: ProbabilityTheory.condDistrib_apply_ae_eq_condExpKernel_map