-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
γ : Type u_6
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
rw rw₁ rw₂ :
  (∀ (s : Set β) (t : Set γ),
      MeasurableSet s →
        MeasurableSet t →
          ∀ᵐ (a : α) ∂μ,
            (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) =
              HMul.hMul (α := ENNReal) (β := ENNReal)
                ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
                ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal)) ↔
    Eq (α := Measure (α × β × γ)) (μ ⊗ₘ κ.map fun (ω : Ω) ↦ (f ω, g ω)) (μ ⊗ₘ (κ.map f ×ₖ κ.map g))
refine_1 :
  ∀
    (h :
      ∀ (s : Set β) (t : Set γ),
        MeasurableSet s →
          MeasurableSet t →
            ∀ᵐ (a : α) ∂μ,
              (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) =
                HMul.hMul (α := ENNReal) (β := ENNReal)
                  ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
                  ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal)),
    Eq (α := Measure (α × β × γ)) (μ ⊗ₘ κ.map fun (ω : Ω) ↦ (f ω, g ω)) (μ ⊗ₘ (κ.map f ×ₖ κ.map g))
refine_2 refine_2₁ :
  ∀ (h : Eq (α := Measure (α × β × γ)) (μ ⊗ₘ κ.map fun (ω : Ω) ↦ (f ω, g ω)) (μ ⊗ₘ (κ.map f ×ₖ κ.map g))) (s : Set β)
    (t : Set γ),
    MeasurableSet s →
      MeasurableSet t →
        ∀ᵐ (a : α) ∂μ,
          (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) =
            HMul.hMul (α := ENNReal) (β := ENNReal)
              ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
              ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal)
⊢ IndepFun f g κ μ ↔ Eq (α := Measure (α × β × γ)) (μ ⊗ₘ κ.map fun (ω : Ω) ↦ (f ω, g ω)) (μ ⊗ₘ (κ.map f ×ₖ κ.map g))

Tactic:
classical
  rw [indepFun_iff_measure_inter_preimage_eq_mul]
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rw [Measure.ext_prod₃_iff]
    intro u s t hu hs ht
    rw [Measure.compProd_apply (hu.prod (hs.prod ht)),
      Measure.compProd_apply (hu.prod (hs.prod ht))]
    refine lintegral_congr_ae ?_
    have h_set_eq ω : Prod.mk ω ⁻¹' u ×ˢ s ×ˢ t = if ω ∈ u then s ×ˢ t else ∅ := by ext; simp
    simp_rw [h_set_eq]
    filter_upwards [h s t hs ht] with ω hω
    by_cases hωu : ω ∈ u
    swap; · simp [hωu]
    simp only [hωu, ↓reduceIte]
    rw [map_apply _ (by fun_prop), Measure.map_apply (by fun_prop) (hs.prod ht),
      mk_preimage_prod, hω, prod_apply_prod, map_apply' _ (by fun_prop), map_apply' _ (by fun_prop)]
    exacts [ht, hs]
  · intro s t hs ht
    rw [Measure.ext_prod₃_iff] at h
    refine ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite ?_ ?_ ?_
    · exact Kernel.measurable_coe _ ((hf hs).inter (hg ht))
    · exact (Kernel.measurable_coe _ (hf hs)).mul (Kernel.measurable_coe _ (hg ht))
    intro u hu hμu
    specialize h hu hs ht
    rw [Measure.compProd_apply_prod hu (hs.prod ht),
      Measure.compProd_apply_prod hu (hs.prod ht)] at h
    convert! h with ω ω
    · rw [map_apply' _ (by fun_prop) _ (hs.prod ht), mk_preimage_prod]
    · rw [prod_apply_prod, map_apply' _ (by fun_prop) _ hs, map_apply' _ (by fun_prop) _ ht]

Premises used: ProbabilityTheory.Kernel.map_apply, ProbabilityTheory.Kernel.map_apply', ProbabilityTheory.Kernel.indepFun_iff_measure_inter_preimage_eq_mul, MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite, MeasureTheory.lintegral_congr_ae, MeasureTheory.Measure.ext_prod₃_iff, reduceIte, Set.mk_preimage_prod, ProbabilityTheory.Kernel.prod_apply_prod