-- 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∞)
h_right :
  ∀ {s : Set γ} {t : Set β} {u : Set β'} (hs : MeasurableSet s) (ht : MeasurableSet t) (hu : MeasurableSet u),
    Eq (α := ℝ≥0∞)
      ((Measure.bind (mα := mγ) (Measure.map k μ)
              (⇑(Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g 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 (Ω × β × β')) ∘ₘ
              μ.trim ⋯ :
            (a : Set (Ω × β × β')) → ℝ≥0∞)
          ((k ⁻¹' s) ×ˢ t ×ˢ u) :
        ℝ≥0∞)
refine_1 :
  ∀
    (h :
      ∀ {s : Set Ω} {t : Set β} {u : Set β'},
        MeasurableSet s →
          MeasurableSet t →
            MeasurableSet u →
              Eq (α := ℝ≥0∞)
                ((Measure.map (fun (ω : Ω) ↦ (ω, f ω, g ω)) μ : (a : Set (Ω × β × β')) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
                (((⇑(Kernel.id ×ₖ
                              (Kernel.map (condExpKernel μ (MeasurableSpace.comap k inferInstance)) f ×ₖ
                                Kernel.map (condExpKernel μ (MeasurableSpace.comap k inferInstance)) g)) :
                          (a : Ω) → Measure (Ω × β × β')) ∘ₘ
                        μ.trim ⋯ :
                      (a : Set (Ω × β × β')) → ℝ≥0∞)
                    (s ×ˢ t ×ˢ u) :
                  ℝ≥0∞))
    (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.bind (mα := mγ) (Measure.map k μ)
              (⇑(Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) : (a : γ) → Measure (γ × β × β')) :
            (a : Set (γ × β × β')) → ℝ≥0∞)
          (s ×ˢ t ×ˢ u) :
        ℝ≥0∞)
refine_2 :
  ∀
    (h :
      ∀ {s : Set γ} {t : Set β} {u : Set β'},
        MeasurableSet s →
          MeasurableSet t →
            MeasurableSet u →
              Eq (α := ℝ≥0∞)
                ((Measure.map (fun (ω : Ω) ↦ (k ω, f ω, g ω)) μ : (a : Set (γ × β × β')) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
                ((Measure.bind (mα := mγ) (Measure.map k μ)
                        (⇑(Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) : (a : γ) → Measure (γ × β × β')) :
                      (a : Set (γ × β × β')) → ℝ≥0∞)
                    (s ×ˢ t ×ˢ u) :
                  ℝ≥0∞))
    {s : Set Ω} {t : Set β} {u : Set β'},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u →
          Eq (α := ℝ≥0∞)
            ((Measure.map (fun (ω : Ω) ↦ (ω, f ω, g ω)) μ : (a : Set (Ω × β × β')) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
            (((⇑(Kernel.id ×ₖ
                          (Kernel.map (condExpKernel μ (MeasurableSpace.comap k inferInstance)) f ×ₖ
                            Kernel.map (condExpKernel μ (MeasurableSpace.comap k inferInstance)) g)) :
                      (a : Ω) → Measure (Ω × β × β')) ∘ₘ
                    μ.trim ⋯ :
                  (a : Set (Ω × β × β')) → ℝ≥0∞)
                (s ×ˢ t ×ˢ u) :
              ℝ≥0∞)
⊢ (∀ {s : Set Ω} {t : Set β} {u : Set β'},
      MeasurableSet s →
        MeasurableSet t →
          MeasurableSet u →
            Eq (α := ℝ≥0∞)
              ((Measure.map (fun (ω : Ω) ↦ (ω, f ω, g ω)) μ : (a : Set (Ω × β × β')) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
              (((⇑(Kernel.id ×ₖ
                            (Kernel.map (condExpKernel μ (MeasurableSpace.comap k inferInstance)) f ×ₖ
                              Kernel.map (condExpKernel μ (MeasurableSpace.comap k inferInstance)) g)) :
                        (a : Ω) → Measure (Ω × β × β')) ∘ₘ
                      μ.trim ⋯ :
                    (a : Set (Ω × β × β')) → ℝ≥0∞)
                  (s ×ˢ t ×ˢ u) :
                ℝ≥0∞)) ↔
    ∀ {s : Set γ} {t : Set β} {u : Set β'},
      MeasurableSet s →
        MeasurableSet t →
          MeasurableSet u →
            Eq (α := ℝ≥0∞)
              ((Measure.map (fun (ω : Ω) ↦ (k ω, f ω, g ω)) μ : (a : Set (γ × β × β')) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
              ((Measure.bind (mα := mγ) (Measure.map k μ)
                      (⇑(Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) : (a : γ) → Measure (γ × β × β')) :
                    (a : Set (γ × β × β')) → ℝ≥0∞)
                  (s ×ˢ t ×ˢ u) :
                ℝ≥0∞)

Tactic:
refine ⟨fun h s t u hs ht hu ↦ ?_, fun h ↦ ?_⟩