awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
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))
⊢ (∀ (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))
have 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)
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
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)
⊢ Eq (α := Measure (α × β × γ)) (μ ⊗ₘ κ.map fun (ω : Ω) ↦ (f ω, g ω)) (μ ⊗ₘ (κ.map f ×ₖ κ.map g))
have 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)
Tactic: rw [Measure.ext_prod₃_iff]
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
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
⊢ Eq (α := ENNReal) ((μ ⊗ₘ κ.map fun (ω : Ω) ↦ (f ω, g ω) : (a : Set (α × β × γ)) → ENNReal) (u ×ˢ s ×ˢ t) : ENNReal)
    ((μ ⊗ₘ (κ.map f ×ₖ κ.map g) : (a : Set (α × β × γ)) → ENNReal) (u ×ˢ s ×ˢ t) : ENNReal)
have 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) ∂μ
Tactic: rw [Measure.compProd_apply (hu.prod (hs.prod ht)),
      Measure.compProd_apply (hu.prod (hs.prod ht))]
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
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) ∂μ
have 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)
Tactic: refine lintegral_congr_ae ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
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 ∅
have h₁ : ∀ (x : β × γ), x ∈ Prod.mk ω ⁻¹' u ×ˢ s ×ˢ t ↔ x ∈ if ω ∈ u then s ×ˢ t else ∅
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (hypothesis)
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
⊢ (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)
have h_set_eq : ∀ (ω : α), 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
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
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 ∅
⊢ (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)
have 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 ∅)
Tactic: simp_rw [h_set_eq]
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
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 ∅
⊢ (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 ∅)
have 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)
Tactic: filter_upwards [h s t hs ht] with ω hω
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases hωu : ω ∈ u
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases hωu : ω ∈ u
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
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)
have 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)
Tactic: simp only [hωu, ↓reduceIte]
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
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
⊢ ∀ᵐ (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)
have 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)
Tactic: rw [Measure.ext_prod₃_iff] at h
Cleared hypotheses: h, s, t, hs, ht
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.IndepFun (goal)
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)
have refine_2 : Measurable (β := ENNReal) fun (a : α) ↦
  (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t)
Tactic: refine ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite ?_ ?_ ?_