awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
_mβ : MeasurableSpace β
_mβ' : MeasurableSpace β'
inst : Neg β'
inst_1 : MeasurableNeg β'
hfg : IndepFun f g κ μ
⊢ IndepFun f (-g) κ μ

Tactic:
hfg.comp measurable_id measurable_neg

Premises used: measurable_id, MeasurableNeg.measurable_neg, ProbabilityTheory.Kernel.IndepFun.comp
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
_mβ : MeasurableSpace β
_mβ' : MeasurableSpace β'
inst : Neg β
inst_1 : MeasurableNeg β
hfg : IndepFun f g κ μ
⊢ IndepFun (-f) g κ μ

Tactic:
hfg.comp measurable_neg measurable_id

Premises used: measurable_id, MeasurableNeg.measurable_neg, ProbabilityTheory.Kernel.IndepFun.comp
-- 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 :
  (∀ (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))
⊢ IndepFun f g κ μ ↔ Eq (α := Measure (α × β × γ)) (μ ⊗ₘ κ.map fun (ω : Ω) ↦ (f ω, g ω)) (μ ⊗ₘ (κ.map f ×ₖ κ.map g))

Tactic:
rw [indepFun_iff_measure_inter_preimage_eq_mul]

Premises used: ProbabilityTheory.Kernel.indepFun_iff_measure_inter_preimage_eq_mul
-- 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
⊢ (∀ (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))

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- 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
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 :
  ∀ (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)
⊢ (∀ (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))

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- 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
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)
refine_1 :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u →
          Eq (α := ENNReal)
            ((μ ⊗ₘ κ.map fun (ω : Ω) ↦ (f ω, g ω) : (a : Set (α × β × γ)) → ENNReal) (s ×ˢ t ×ˢ u) : ENNReal)
            ((μ ⊗ₘ (κ.map f ×ₖ κ.map g) : (a : Set (α × β × γ)) → ENNReal) (s ×ˢ t ×ˢ u) : ENNReal)
⊢ Eq (α := Measure (α × β × γ)) (μ ⊗ₘ κ.map fun (ω : Ω) ↦ (f ω, g ω)) (μ ⊗ₘ (κ.map f ×ₖ κ.map g))

Tactic:
rw [Measure.ext_prod₃_iff]

Premises used: MeasureTheory.Measure.ext_prod₃_iff
-- 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
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)
u : Set α
s : Set β
t : Set γ
hu : MeasurableSet u
hs : MeasurableSet s
ht : MeasurableSet t
refine_1 :
  ∫⁻ (a : α),
      (((κ.map fun (ω : Ω) ↦ (f ω, g ω) : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
        (Prod.mk a ⁻¹' u ×ˢ s ×ˢ t) ∂μ =
    ∫⁻ (a : α),
      (((κ.map f ×ₖ κ.map g : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
        (Prod.mk a ⁻¹' u ×ˢ s ×ˢ t) ∂μ
⊢ Eq (α := ENNReal) ((μ ⊗ₘ κ.map fun (ω : Ω) ↦ (f ω, g ω) : (a : Set (α × β × γ)) → ENNReal) (u ×ˢ s ×ˢ t) : ENNReal)
    ((μ ⊗ₘ (κ.map f ×ₖ κ.map g) : (a : Set (α × β × γ)) → ENNReal) (u ×ˢ s ×ˢ t) : ENNReal)

Tactic:
rw [Measure.compProd_apply (hu.prod (hs.prod ht)),
      Measure.compProd_apply (hu.prod (hs.prod ht))]

Premises used: MeasureTheory.Measure.compProd_apply, MeasurableSet.prod
-- 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
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)
u : Set α
s : Set β
t : Set γ
hu : MeasurableSet u
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (a : α),
      (((κ.map fun (ω : Ω) ↦ (f ω, g ω) : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
        (Prod.mk a ⁻¹' u ×ˢ s ×ˢ t) ∂μ =
    ∫⁻ (a : α),
      (((κ.map f ×ₖ κ.map g : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
        (Prod.mk a ⁻¹' u ×ˢ s ×ˢ t) ∂μ

Tactic:
lintegral_congr_ae ?_

Premises used: MeasureTheory.lintegral_congr_ae
-- 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
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)
u : Set α
s : Set β
t : Set γ
hu : MeasurableSet u
hs : MeasurableSet s
ht : MeasurableSet t
refine_1 :
  (ae μ).EventuallyEq (β := ENNReal)
    (fun (a : α) ↦
      (((κ.map fun (ω : Ω) ↦ (f ω, g ω) : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
        (Prod.mk a ⁻¹' u ×ˢ s ×ˢ t))
    fun (a : α) ↦
    (((κ.map f ×ₖ κ.map g : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
      (Prod.mk a ⁻¹' u ×ˢ s ×ˢ t)
⊢ ∫⁻ (a : α),
      (((κ.map fun (ω : Ω) ↦ (f ω, g ω) : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
        (Prod.mk a ⁻¹' u ×ˢ s ×ˢ t) ∂μ =
    ∫⁻ (a : α),
      (((κ.map f ×ₖ κ.map g : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
        (Prod.mk a ⁻¹' u ×ˢ s ×ˢ t) ∂μ

Tactic:
refine lintegral_congr_ae ?_

Premises used: MeasureTheory.lintegral_congr_ae
-- 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
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)
u : Set α
s : Set β
t : Set γ
hu : MeasurableSet u
hs : MeasurableSet s
ht : MeasurableSet t
ω : α
h₁ : ∀ (x : β × γ), x ∈ Prod.mk ω ⁻¹' u ×ˢ s ×ˢ t ↔ x ∈ if ω ∈ u then s ×ˢ t else ∅
⊢ Prod.mk ω ⁻¹' u ×ˢ s ×ˢ t = if ω ∈ u then s ×ˢ t else ∅

Tactic:
ext
-- 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
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)
u : Set α
s : Set β
t : Set γ
hu : MeasurableSet u
hs : MeasurableSet s
ht : MeasurableSet t
ω : α
x : β × γ
⊢ x ∈ Prod.mk ω ⁻¹' u ×ˢ s ×ˢ t ↔ x ∈ if ω ∈ u then s ×ˢ t else ∅

Tactic:
simp
-- 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
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)
u : Set α
s : Set β
t : Set γ
hu : MeasurableSet u
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∀ (ω : α), Prod.mk ω ⁻¹' u ×ˢ s ×ˢ t = if ω ∈ u then s ×ˢ t else ∅

Tactic:
have h_set_eq ω : Prod.mk ω ⁻¹' u ×ˢ s ×ˢ t = if ω ∈ u then s ×ˢ t else ∅ := by ext; simp
-- 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
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)
u : Set α
s : Set β
t : Set γ
hu : MeasurableSet u
hs : MeasurableSet s
ht : MeasurableSet t
h_set_eq : ∀ (ω : α), Prod.mk ω ⁻¹' u ×ˢ s ×ˢ t = if ω ∈ u then s ×ˢ t else ∅
refine_1 :
  (ae μ).EventuallyEq (β := ENNReal)
    (fun (a : α) ↦
      (((κ.map fun (ω : Ω) ↦ (f ω, g ω) : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
        (if a ∈ u then s ×ˢ t else ∅))
    fun (a : α) ↦
    (((κ.map f ×ₖ κ.map g : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
      (if a ∈ u then s ×ˢ t else ∅)
⊢ (ae μ).EventuallyEq (β := ENNReal)
    (fun (a : α) ↦
      (((κ.map fun (ω : Ω) ↦ (f ω, g ω) : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
        (Prod.mk a ⁻¹' u ×ˢ s ×ˢ t))
    fun (a : α) ↦
    (((κ.map f ×ₖ κ.map g : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
      (Prod.mk a ⁻¹' u ×ˢ s ×ˢ t)

Tactic:
simp_rw [h_set_eq]
-- 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
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)
u : Set α
s : Set β
t : Set γ
hu : MeasurableSet u
hs : MeasurableSet s
ht : MeasurableSet t
h_set_eq : ∀ (ω : α), Prod.mk ω ⁻¹' u ×ˢ s ×ˢ t = if ω ∈ u then s ×ˢ t else ∅
h₁ :
  ∀ (ω : α)
    (hω :
      (((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) =
        HMul.hMul (α := ENNReal) (β := ENNReal)
          ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
          ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal)),
    Eq (α := ENNReal)
      ((((κ.map fun (ω : Ω) ↦ (f ω, g ω) : (a : α) → Measure (β × γ)) ω : Measure (β × γ)) :
            (a : Set (β × γ)) → ENNReal)
          (if ω ∈ u then s ×ˢ t else ∅) :
        ENNReal)
      ((((κ.map f ×ₖ κ.map g : (a : α) → Measure (β × γ)) ω : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
          (if ω ∈ u then s ×ˢ t else ∅) :
        ENNReal)
⊢ (ae μ).EventuallyEq (β := ENNReal)
    (fun (a : α) ↦
      (((κ.map fun (ω : Ω) ↦ (f ω, g ω) : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
        (if a ∈ u then s ×ˢ t else ∅))
    fun (a : α) ↦
    (((κ.map f ×ₖ κ.map g : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
      (if a ∈ u then s ×ˢ t else ∅)

Tactic:
filter_upwards [h s t hs ht] with ω hω
-- 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
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)
u : Set α
s : Set β
t : Set γ
hu : MeasurableSet u
hs : MeasurableSet s
ht : MeasurableSet t
h_set_eq : ∀ (ω : α), Prod.mk ω ⁻¹' u ×ˢ s ×ˢ t = if ω ∈ u then s ×ˢ t else ∅
ω : α
hω :
  (((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) =
    HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
      ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal)
pos :
  ∀ (hωu : ω ∈ u),
    Eq (α := ENNReal)
      ((((κ.map fun (ω : Ω) ↦ (f ω, g ω) : (a : α) → Measure (β × γ)) ω : Measure (β × γ)) :
            (a : Set (β × γ)) → ENNReal)
          (if ω ∈ u then s ×ˢ t else ∅) :
        ENNReal)
      ((((κ.map f ×ₖ κ.map g : (a : α) → Measure (β × γ)) ω : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
          (if ω ∈ u then s ×ˢ t else ∅) :
        ENNReal)
neg :
  ∀ (hωu : ω ∉ u),
    Eq (α := ENNReal)
      ((((κ.map fun (ω : Ω) ↦ (f ω, g ω) : (a : α) → Measure (β × γ)) ω : Measure (β × γ)) :
            (a : Set (β × γ)) → ENNReal)
          (if ω ∈ u then s ×ˢ t else ∅) :
        ENNReal)
      ((((κ.map f ×ₖ κ.map g : (a : α) → Measure (β × γ)) ω : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
          (if ω ∈ u then s ×ˢ t else ∅) :
        ENNReal)
⊢ Eq (α := ENNReal)
    ((((κ.map fun (ω : Ω) ↦ (f ω, g ω) : (a : α) → Measure (β × γ)) ω : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
        (if ω ∈ u then s ×ˢ t else ∅) :
      ENNReal)
    ((((κ.map f ×ₖ κ.map g : (a : α) → Measure (β × γ)) ω : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
        (if ω ∈ u then s ×ˢ t else ∅) :
      ENNReal)

Tactic:
by_cases hωu : ω ∈ u
-- 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
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)
u : Set α
s : Set β
t : Set γ
hu : MeasurableSet u
hs : MeasurableSet s
ht : MeasurableSet t
h_set_eq : ∀ (ω : α), Prod.mk ω ⁻¹' u ×ˢ s ×ˢ t = if ω ∈ u then s ×ˢ t else ∅
ω : α
hω :
  (((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) =
    HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
      ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal)
hωu : ω ∉ u
⊢ Eq (α := ENNReal)
    ((((κ.map fun (ω : Ω) ↦ (f ω, g ω) : (a : α) → Measure (β × γ)) ω : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
        (if ω ∈ u then s ×ˢ t else ∅) :
      ENNReal)
    ((((κ.map f ×ₖ κ.map g : (a : α) → Measure (β × γ)) ω : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
        (if ω ∈ u then s ×ˢ t else ∅) :
      ENNReal)

Tactic:
simp [hωu]