-- 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
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∞)
h :
  s.indicator 1 (k a) *
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
        (((((condDistrib f k μ : Kernel γ β) : (a : γ) → Measure β) (k a) : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
        (((((condDistrib g k μ : Kernel γ β') : (a : γ) → Measure β') (k a) : Measure β') : (a : Set β') → ℝ≥0∞) u :
          ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (((Measure.dirac a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (k ⁻¹' s) : ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
        (((((Kernel.map (condExpKernel μ (MeasurableSpace.comap k mγ)) f : Kernel Ω β) : (a : Ω) → Measure β) a :
                Measure β) :
              (a : Set β) → ℝ≥0∞)
            t :
          ℝ≥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∞)

Tactic:
simp only [Kernel.prod_apply_prod, Kernel.id_apply, Measure.dirac_apply' _ hs]

Premises used: MeasureTheory.Measure.dirac_apply', ProbabilityTheory.Kernel.id_apply, ProbabilityTheory.Kernel.prod_apply_prod