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
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)
⊢ ∀ᵐ (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 : α) ↦
  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 ?_ ?_ ?_
-- 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
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)
⊢ ∀ᵐ (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₂ : ∀ (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) ∂μ
Tactic: refine ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite ?_ ?_ ?_
-- 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 β} {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)
⊢ ∫⁻ (x : α) in u, (((κ : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) ∂μ =
    ∫⁻ (x : α) in u,
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((κ : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
        ((((κ : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal) ∂μ
have h₁ : 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
Cleared hypotheses: h
-- 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
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)
h :
  Eq (α := ENNReal) ((μ ⊗ₘ κ.map fun (ω : Ω) ↦ (f ω, g ω) : (a : Set (α × β × γ)) → ENNReal) (u ×ˢ s ×ˢ t) : ENNReal)
    ((μ ⊗ₘ (κ.map f ×ₖ κ.map g) : (a : Set (α × β × γ)) → ENNReal) (u ×ˢ s ×ˢ t) : ENNReal)
⊢ ∫⁻ (x : α) in u, (((κ : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) ∂μ =
    ∫⁻ (x : α) in u,
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((κ : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
        ((((κ : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal) ∂μ
have h₁ : ∫⁻ (a : α) in u,
    (((κ.map fun (ω : Ω) ↦ (f ω, g ω) : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
      (s ×ˢ t) ∂μ =
  ∫⁻ (a : α) in u,
    (((κ.map f ×ₖ κ.map g : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal) (s ×ˢ t) ∂μ
Tactic: rw [Measure.compProd_apply_prod hu (hs.prod ht),
      Measure.compProd_apply_prod hu (hs.prod ht)] at h
Cleared hypotheses: 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
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)
h :
  ∫⁻ (a : α) in u,
      (((κ.map fun (ω : Ω) ↦ (f ω, g ω) : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
        (s ×ˢ t) ∂μ =
    ∫⁻ (a : α) in u,
      (((κ.map f ×ₖ κ.map g : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal) (s ×ˢ t) ∂μ
⊢ ∫⁻ (x : α) in u, (((κ : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) ∂μ =
    ∫⁻ (x : α) in u,
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((κ : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
        ((((κ : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal) ∂μ
have h₁ : ∀ (ω : α),
  Eq (α := ENNReal) ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) : ENNReal)
    ((((κ.map fun (ω : Ω) ↦ (f ω, g ω) : (a : α) → Measure (β × γ)) ω : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
        (s ×ˢ t) :
      ENNReal)
Tactic: convert! h with ω ω
-- 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
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)
h :
  ∫⁻ (a : α) in u,
      (((κ.map fun (ω : Ω) ↦ (f ω, g ω) : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
        (s ×ˢ t) ∂μ =
    ∫⁻ (a : α) in u,
      (((κ.map f ×ₖ κ.map g : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal) (s ×ˢ t) ∂μ
h₁ :
  ∀ (ω : α),
    Eq (α := ENNReal)
      ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) : ENNReal)
      ((((κ.map fun (ω : Ω) ↦ (f ω, g ω) : (a : α) → Measure (β × γ)) ω : Measure (β × γ)) :
            (a : Set (β × γ)) → ENNReal)
          (s ×ˢ t) :
        ENNReal)
⊢ ∫⁻ (x : α) in u, (((κ : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) ∂μ =
    ∫⁻ (x : α) in u,
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((κ : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
        ((((κ : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal) ∂μ
have h₂ : ∀ (ω : α),
  HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
      ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal) =
    (((κ.map f ×ₖ κ.map g : (a : α) → Measure (β × γ)) ω : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal) (s ×ˢ t)
Tactic: convert! h with ω ω
-- 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
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)
h :
  ∫⁻ (a : α) in u,
      (((κ.map fun (ω : Ω) ↦ (f ω, g ω) : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
        (s ×ˢ t) ∂μ =
    ∫⁻ (a : α) in u,
      (((κ.map f ×ₖ κ.map g : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal) (s ×ˢ t) ∂μ
ω : α
⊢ Eq (α := ENNReal) ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) : ENNReal)
    ((((κ.map fun (ω : Ω) ↦ (f ω, g ω) : (a : α) → Measure (β × γ)) ω : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
        (s ×ˢ t) :
      ENNReal)
have h₁ : Eq (α := ENNReal) ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) : ENNReal)
  ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) ((fun (ω : Ω) ↦ (f ω, g ω)) ⁻¹' s ×ˢ t) :
    ENNReal)
Tactic: rw [map_apply' _ (by fun_prop) _ (hs.prod ht), mk_preimage_prod]
-- 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
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)
h :
  ∫⁻ (a : α) in u,
      (((κ.map fun (ω : Ω) ↦ (f ω, g ω) : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
        (s ×ˢ t) ∂μ =
    ∫⁻ (a : α) in u,
      (((κ.map f ×ₖ κ.map g : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal) (s ×ˢ t) ∂μ
ω : α
h₁ :
  Eq (α := ENNReal) ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) : ENNReal)
    ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) ((fun (ω : Ω) ↦ (f ω, g ω)) ⁻¹' s ×ˢ t) :
      ENNReal)
⊢ Eq (α := ENNReal) ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) : ENNReal)
    ((((κ.map fun (ω : Ω) ↦ (f ω, g ω) : (a : α) → Measure (β × γ)) ω : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
        (s ×ˢ t) :
      ENNReal)
have h₂ : Eq (α := ENNReal) ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) : ENNReal)
  ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s ∩ g ⁻¹' t) : ENNReal)
Tactic: rw [map_apply' _ (by fun_prop) _ (hs.prod ht), mk_preimage_prod]
-- 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
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)
h :
  ∫⁻ (a : α) in u,
      (((κ.map fun (ω : Ω) ↦ (f ω, g ω) : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
        (s ×ˢ t) ∂μ =
    ∫⁻ (a : α) in u,
      (((κ.map f ×ₖ κ.map g : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal) (s ×ˢ t) ∂μ
ω : α
⊢ HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
      ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal) =
    (((κ.map f ×ₖ κ.map g : (a : α) → Measure (β × γ)) ω : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal) (s ×ˢ t)
have h₁ : HMul.hMul (α := ENNReal) (β := ENNReal)
    ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
    ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal) =
  HMul.hMul (α := ENNReal) (β := ENNReal)
    (((((κ.map f : Kernel α β) : (a : α) → Measure β) ω : Measure β) : (a : Set β) → ENNReal) s : ENNReal)
    (((((κ.map g : Kernel α γ) : (a : α) → Measure γ) ω : Measure γ) : (a : Set γ) → ENNReal) t : ENNReal)
Tactic: rw [prod_apply_prod, map_apply' _ (by fun_prop) _ hs, map_apply' _ (by fun_prop) _ 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
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)
h :
  ∫⁻ (a : α) in u,
      (((κ.map fun (ω : Ω) ↦ (f ω, g ω) : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
        (s ×ˢ t) ∂μ =
    ∫⁻ (a : α) in u,
      (((κ.map f ×ₖ κ.map g : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal) (s ×ˢ t) ∂μ
ω : α
h₁ :
  HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
      ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal) =
    HMul.hMul (α := ENNReal) (β := ENNReal)
      (((((κ.map f : Kernel α β) : (a : α) → Measure β) ω : Measure β) : (a : Set β) → ENNReal) s : ENNReal)
      (((((κ.map g : Kernel α γ) : (a : α) → Measure γ) ω : Measure γ) : (a : Set γ) → ENNReal) t : ENNReal)
⊢ HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
      ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal) =
    (((κ.map f ×ₖ κ.map g : (a : α) → Measure (β × γ)) ω : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal) (s ×ˢ t)
have h₂ : HMul.hMul (α := ENNReal) (β := ENNReal)
    ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
    ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal) =
  HMul.hMul (α := ENNReal) (β := ENNReal)
    ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
    (((((κ.map g : Kernel α γ) : (a : α) → Measure γ) ω : Measure γ) : (a : Set γ) → ENNReal) t : ENNReal)
Tactic: rw [prod_apply_prod, map_apply' _ (by fun_prop) _ hs, map_apply' _ (by fun_prop) _ 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
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)
h :
  ∫⁻ (a : α) in u,
      (((κ.map fun (ω : Ω) ↦ (f ω, g ω) : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal)
        (s ×ˢ t) ∂μ =
    ∫⁻ (a : α) in u,
      (((κ.map f ×ₖ κ.map g : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal) (s ×ˢ t) ∂μ
ω : α
h₁ :
  HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
      ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal) =
    HMul.hMul (α := ENNReal) (β := ENNReal)
      (((((κ.map f : Kernel α β) : (a : α) → Measure β) ω : Measure β) : (a : Set β) → ENNReal) s : ENNReal)
      (((((κ.map g : Kernel α γ) : (a : α) → Measure γ) ω : Measure γ) : (a : Set γ) → ENNReal) t : ENNReal)
h₂ :
  HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
      ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal) =
    HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
      (((((κ.map g : Kernel α γ) : (a : α) → Measure γ) ω : Measure γ) : (a : Set γ) → ENNReal) t : ENNReal)
⊢ HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
      ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal) =
    (((κ.map f ×ₖ κ.map g : (a : α) → Measure (β × γ)) ω : Measure (β × γ)) : (a : Set (β × γ)) → ENNReal) (s ×ˢ t)
have h₃ : HMul.hMul (α := ENNReal) (β := ENNReal)
    ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
    ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal) =
  HMul.hMul (α := ENNReal) (β := ENNReal)
    ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (f ⁻¹' s) : ENNReal)
    ((((κ : (a : α) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ENNReal) (g ⁻¹' t) : ENNReal)
Tactic: rw [prod_apply_prod, map_apply' _ (by fun_prop) _ hs, map_apply' _ (by fun_prop) _ 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
⊢ IndepFun f g κ μ ↔ Eq (α := Measure (α × β × γ)) (μ ⊗ₘ κ.map fun (ω : Ω) ↦ (f ω, g ω)) (μ ⊗ₘ (κ.map f ×ₖ κ.map g))
have 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))
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]