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_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
pos :
  Eq (α := ENNReal)
    ((((κ.map fun (ω : Ω) ↦ (f ω, g ω) : (a : α) → Measure (β × γ)) ω : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
        (s ×ˢ t) :
      ENNReal)
    ((((κ.map f ×ₖ κ.map g : (a : α) → Measure (β × γ)) ω : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal) (s ×ˢ 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)

Tactic:
simp only [hωu, ↓reduceIte]

Premises used: reduceIte
-- 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
⊢ Measurable (β := β × γ) fun (ω : Ω) ↦ (f ω, g ω)

Tactic:
fun_prop
-- 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
⊢ Measurable f

Tactic:
fun_prop
-- 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
⊢ Measurable g

Tactic:
fun_prop
-- 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
pos : MeasurableSet t
pos₁ : MeasurableSet s
⊢ Eq (α := ENNReal)
    ((((κ.map fun (ω : Ω) ↦ (f ω, g ω) : (a : α) → Measure (β × γ)) ω : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
        (s ×ˢ t) :
      ENNReal)
    ((((κ.map f ×ₖ κ.map g : (a : α) → Measure (β × γ)) ω : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal) (s ×ˢ t) :
      ENNReal)

Tactic:
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)]

Premises used: ProbabilityTheory.Kernel.map_apply, ProbabilityTheory.Kernel.map_apply', MeasureTheory.Measure.map_apply, MeasurableSet.prod, Set.mk_preimage_prod, ProbabilityTheory.Kernel.prod_apply_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
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
⊢ MeasurableSet t

Tactic:
ht
-- 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
⊢ MeasurableSet s

Tactic:
hs
-- 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
⊢ MeasurableSet t

Tactic:
exacts [ht, hs]
-- 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 : Eq (α := Measure (α × β × γ)) (μ ⊗ₘ κ.map fun (ω : Ω) ↦ (f ω, g ω)) (μ ⊗ₘ (κ.map f ×ₖ κ.map g))
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
refine_2 :
  ∀
    (h :
      ∀ {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))
    (s : Set β) (t : Set γ) (hs : MeasurableSet s) (ht : 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)
⊢ ∀ᵐ (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)

Tactic:
rw [Measure.ext_prod₃_iff] at h

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 β} {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)
s : Set β
t : Set γ
hs : MeasurableSet s
ht : 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)

Tactic:
ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite ?_ ?_ ?_

Premises used: MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite, Filter.EventuallyEq
-- 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 β} {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)
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
refine_2 :
  Measurable (β := ENNReal) fun (a : α) ↦
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t)
refine_2₁ :
  Measurable (β := ENNReal) fun (a : α) ↦
    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_2₂ :
  ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      LT.lt (α := ENNReal) ((μ : (a : Set α) → ENNReal) s_1 : ENNReal) (⊤ : ENNReal) →
        ∫⁻ (x : α) in s_1, (((κ : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) ∂μ =
          ∫⁻ (x : α) in s_1,
            HMul.hMul (α := ENNReal) (β := ENNReal)
              ((((κ : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
              ((((κ : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal) ∂μ
⊢ ∀ᵐ (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)

Tactic:
refine ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite ?_ ?_ ?_

Premises used: MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite
-- 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 β} {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)
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ Measurable (β := ENNReal) fun (a : α) ↦
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t)

Tactic:
Kernel.measurable_coe _ ((hf hs).inter (hg ht))

Premises used: ProbabilityTheory.Kernel.measurable_coe, MeasurableSet.inter
-- 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 β} {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)
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ Measurable (β := ENNReal) fun (a : α) ↦
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t)

Tactic:
exact Kernel.measurable_coe _ ((hf hs).inter (hg ht))

Premises used: ProbabilityTheory.Kernel.measurable_coe, MeasurableSet.inter
-- 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 β} {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)
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ Measurable (β := ENNReal) fun (a : α) ↦
    HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal)

Tactic:
(Kernel.measurable_coe _ (hf hs)).mul (Kernel.measurable_coe _ (hg ht))

Premises used: Measurable.mul, ProbabilityTheory.Kernel.measurable_coe
-- 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 β} {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)
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ Measurable (β := ENNReal) fun (a : α) ↦
    HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal)

Tactic:
exact (Kernel.measurable_coe _ (hf hs)).mul (Kernel.measurable_coe _ (hg ht))

Premises used: Measurable.mul, ProbabilityTheory.Kernel.measurable_coe
-- 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 β} {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)
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
u : Set α
hu : MeasurableSet u
hμu : LT.lt (α := ENNReal) ((μ : (a : Set α) → ENNReal) u : ENNReal) (⊤ : ENNReal)
⊢ 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:
specialize h hu hs ht