-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
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∞)
⊢ 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∞))
have 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∞) =
  (k ⁻¹' s).indicator 1 a *
    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∞)
Tactic: rw [@Measure.dirac_apply' _ (mγ.comap k) _ _ (hk_meas hs)]