awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel α γ
inst_1 : IsSFiniteKernel η
ξ : Kernel α δ
inst_2 : IsSFiniteKernel ξ
a : α
h :
  Eq (α := Measure (β × δ × γ))
    (Measure.map (α := (β × δ) × γ) (⇑MeasurableEquiv.prodAssoc : (a : (β × δ) × γ) → β × δ × γ)
      ((κ ×ₖ ξ ×ₖ η : (a : α) → Measure ((β × δ) × γ)) a))
    ((κ ×ₖ (ξ ×ₖ η) : (a : α) → Measure (β × δ × γ)) a)
h₁ :
  Eq (α := Measure (β × δ × γ))
    (Measure.map (α := (β × δ) × γ) (⇑MeasurableEquiv.prodAssoc : (a : (β × δ) × γ) → β × δ × γ)
      (Measure.prod ((κ ×ₖ ξ : (a : α) → Measure (β × δ)) a) ((η : (a : α) → Measure γ) a)))
    ((κ ×ₖ (ξ ×ₖ η) : (a : α) → Measure (β × δ × γ)) a)
h₂ :
  Eq (α := Measure (β × δ × γ))
    (Measure.map (α := (β × δ) × γ) (⇑MeasurableEquiv.prodAssoc : (a : (β × δ) × γ) → β × δ × γ)
      (Measure.prod (Measure.prod ((κ : (a : α) → Measure β) a) ((ξ : (a : α) → Measure δ) a))
        ((η : (a : α) → Measure γ) a)))
    ((κ ×ₖ (ξ ×ₖ η) : (a : α) → Measure (β × δ × γ)) a)
h₃ :
  Eq (α := Measure (β × δ × γ))
    (Measure.prod ((κ : (a : α) → Measure β) a)
      (Measure.prod ((ξ : (a : α) → Measure δ) a) ((η : (a : α) → Measure γ) a)))
    ((κ ×ₖ (ξ ×ₖ η) : (a : α) → Measure (β × δ × γ)) a)
h₄ :
  Eq (α := Measure (β × δ × γ))
    (Measure.prod ((κ : (a : α) → Measure β) a)
      (Measure.prod ((ξ : (a : α) → Measure δ) a) ((η : (a : α) → Measure γ) a)))
    (Measure.prod ((κ : (a : α) → Measure β) a) ((ξ ×ₖ η : (a : α) → Measure (δ × γ)) a))
h₅ h₆ :
  Eq (α := Measure (β × δ × γ))
    (Measure.prod ((κ : (a : α) → Measure β) a)
      (Measure.prod ((ξ : (a : α) → Measure δ) a) ((η : (a : α) → Measure γ) a)))
    (Measure.prod ((κ : (a : α) → Measure β) a)
      (Measure.prod ((ξ : (a : α) → Measure δ) a) ((η : (a : α) → Measure γ) a)))
⊢ Eq (α := Measure (β × δ × γ))
    (((κ ×ₖ ξ ×ₖ η).map (⇑MeasurableEquiv.prodAssoc : (a : (β × δ) × γ) → β × δ × γ) : (a : α) → Measure (β × δ × γ))
        a :
      Measure (β × δ × γ))
    ((κ ×ₖ (ξ ×ₖ η) : (a : α) → Measure (β × δ × γ)) a : Measure (β × δ × γ))

Tactic:
rw [map_apply _ (by fun_prop), prod_apply, prod_apply, Measure.prodAssoc_prod, prod_apply,
    prod_apply]

Premises used: ProbabilityTheory.Kernel.map_apply, ProbabilityTheory.Kernel.prod_apply, MeasureTheory.Measure.prodAssoc_prod
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel α γ
inst_1 : IsSFiniteKernel η
ξ : Kernel α δ
inst_2 : IsSFiniteKernel ξ
⊢ Measurable (α := (β × δ) × γ) (β := β × δ × γ) (⇑MeasurableEquiv.prodAssoc : (a : (β × δ) × γ) → β × δ × γ)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel α γ
inst_1 : IsSFiniteKernel η
ξ : Kernel α δ
inst_2 : IsSFiniteKernel ξ
⊢ Measurable (α := β × δ × γ) (β := (β × δ) × γ)
    (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × δ × γ) → (β × δ) × γ)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel α γ
inst_1 : IsSFiniteKernel η
ξ : Kernel α δ
inst_2 : IsSFiniteKernel ξ
rw :
  (κ ×ₖ ξ ×ₖ η).map
      (Function.comp (β := β × δ × γ)
        (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × δ × γ) → (β × δ) × γ)
        (⇑MeasurableEquiv.prodAssoc : (a : (β × δ) × γ) → β × δ × γ)) =
    κ ×ₖ ξ ×ₖ η
⊢ (κ ×ₖ (ξ ×ₖ η)).map (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × δ × γ) → (β × δ) × γ) = κ ×ₖ ξ ×ₖ η

Tactic:
rw [← prodAssoc_prod, ← Kernel.map_comp_right _ (by fun_prop) (by fun_prop)]

Premises used: ProbabilityTheory.Kernel.map_comp_right, ProbabilityTheory.Kernel.prodAssoc_prod
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel α γ
inst_1 : IsSFiniteKernel η
ξ : Kernel α δ
inst_2 : IsSFiniteKernel ξ
⊢ (κ ×ₖ ξ ×ₖ η).map
      (Function.comp (β := β × δ × γ)
        (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × δ × γ) → (β × δ) × γ)
        (⇑MeasurableEquiv.prodAssoc : (a : (β × δ) × γ) → β × δ × γ)) =
    κ ×ₖ ξ ×ₖ η

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
δ : Type u_6
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel β γ
inst_1 : IsSFiniteKernel η
μ : Measure δ
inst_2 : SFinite μ
h :
  ∀ (x : α) (s : Set (γ × δ)) (ms : MeasurableSet s),
    Eq (α := ℝ≥0∞)
      ((((η ×ₖ const β μ ∘ₖ κ : (a : α) → Measure (γ × δ)) x : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞) s : ℝ≥0∞)
      ((((η ∘ₖ κ ×ₖ const α μ : (a : α) → Measure (γ × δ)) x : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ η ×ₖ const β μ ∘ₖ κ = η ∘ₖ κ ×ₖ const α μ

Tactic:
ext x s ms
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
δ : Type u_6
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel β γ
inst_1 : IsSFiniteKernel η
μ : Measure δ
inst_2 : SFinite μ
x : α
s : Set (γ × δ)
ms : MeasurableSet s
h :
  ∫⁻ (b : β),
      (((η ×ₖ const β μ : (a : β) → Measure (γ × δ)) b : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞)
        s ∂(κ : (a : α) → Measure β) x =
    (((η ∘ₖ κ ×ₖ const α μ : (a : α) → Measure (γ × δ)) x : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞) s
h₁ :
  ∫⁻ (b : β),
      ∫⁻ (b_1 : γ),
        ((((const β μ : Kernel β δ) : (a : β) → Measure δ) b : Measure δ) : (a : Set δ) → ℝ≥0∞)
          (Prod.mk b_1 ⁻¹' s) ∂(η : (a : β) → Measure γ) b ∂(κ : (a : α) → Measure β) x =
    ∫⁻ (b : γ),
      ((((const α μ : Kernel α δ) : (a : α) → Measure δ) x : Measure δ) : (a : Set δ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(η ∘ₖ κ : (a : α) → Measure γ) x
h₂ :
  ∫⁻ (b : β),
      ∫⁻ (b : γ), (μ : (a : Set δ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) ∂(η : (a : β) → Measure γ) b ∂(κ : (a : α) → Measure β) x =
    ∫⁻ (b : γ), (μ : (a : Set δ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) ∂(η ∘ₖ κ : (a : α) → Measure γ) x
⊢ Eq (α := ℝ≥0∞)
    ((((η ×ₖ const β μ ∘ₖ κ : (a : α) → Measure (γ × δ)) x : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((η ∘ₖ κ ×ₖ const α μ : (a : α) → Measure (γ × δ)) x : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp_rw [comp_apply' _ _ _ ms, prod_apply' _ _ _ ms, const_apply,
  lintegral_comp _ _ _ (measurable_measure_prodMk_left ms)]

Premises used: ProbabilityTheory.Kernel.prod_apply', measurable_measure_prodMk_left, ProbabilityTheory.Kernel.lintegral_comp, ProbabilityTheory.Kernel.comp_apply', ProbabilityTheory.Kernel.const_apply
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
δ : Type u_6
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
μ : Measure γ
inst_1 : SFinite μ
η : Kernel β δ
inst_2 : IsSFiniteKernel η
h :
  ∀ (x : α) (s : Set (γ × δ)) (ms : MeasurableSet s),
    Eq (α := ℝ≥0∞)
      ((((const β μ ×ₖ η ∘ₖ κ : (a : α) → Measure (γ × δ)) x : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞) s : ℝ≥0∞)
      ((((const α μ ×ₖ (η ∘ₖ κ) : (a : α) → Measure (γ × δ)) x : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ const β μ ×ₖ η ∘ₖ κ = const α μ ×ₖ (η ∘ₖ κ)

Tactic:
ext x s ms
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
δ : Type u_6
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
μ : Measure γ
inst_1 : SFinite μ
η : Kernel β δ
inst_2 : IsSFiniteKernel η
x : α
s : Set (γ × δ)
ms : MeasurableSet s
h :
  ∫⁻ (b : β),
      (((const β μ ×ₖ η : (a : β) → Measure (γ × δ)) b : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞)
        s ∂(κ : (a : α) → Measure β) x =
    (((const α μ ×ₖ (η ∘ₖ κ) : (a : α) → Measure (γ × δ)) x : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞) s
h₁ :
  ∫⁻ (b : β),
      (Measure.prod (((const β μ : Kernel β γ) : (a : β) → Measure γ) b) ((η : (a : β) → Measure δ) b) :
          (a : Set (γ × δ)) → ℝ≥0∞)
        s ∂(κ : (a : α) → Measure β) x =
    (Measure.prod (((const α μ : Kernel α γ) : (a : α) → Measure γ) x) ((η ∘ₖ κ : (a : α) → Measure δ) x) :
        (a : Set (γ × δ)) → ℝ≥0∞)
      s
h₂ :
  ∫⁻ (b : β),
      ∫⁻ (y : δ),
        ((((const β μ : Kernel β γ) : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞)
          ((fun (x : γ) ↦ (x, y)) ⁻¹' s) ∂(η : (a : β) → Measure δ) b ∂(κ : (a : α) → Measure β) x =
    ∫⁻ (y : δ),
      ((((const α μ : Kernel α γ) : (a : α) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞)
        ((fun (x : γ) ↦ (x, y)) ⁻¹' s) ∂(η ∘ₖ κ : (a : α) → Measure δ) x
h₃ :
  ∫⁻ (b : β),
      ∫⁻ (y : δ),
        (μ : (a : Set γ) → ℝ≥0∞)
          ((fun (x : γ) ↦ (x, y)) ⁻¹' s) ∂(η : (a : β) → Measure δ) b ∂(κ : (a : α) → Measure β) x =
    ∫⁻ (y : δ), (μ : (a : Set γ) → ℝ≥0∞) ((fun (x : γ) ↦ (x, y)) ⁻¹' s) ∂(η ∘ₖ κ : (a : α) → Measure δ) x
⊢ Eq (α := ℝ≥0∞)
    ((((const β μ ×ₖ η ∘ₖ κ : (a : α) → Measure (γ × δ)) x : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((const α μ ×ₖ (η ∘ₖ κ) : (a : α) → Measure (γ × δ)) x : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp_rw [comp_apply' _ _ _ ms, prod_apply, Measure.prod_apply_symm ms, const_apply,
  lintegral_comp _ _ _ (measurable_measure_prodMk_right ms)]

Premises used: MeasureTheory.Measure.prod_apply_symm, ProbabilityTheory.Kernel.prod_apply, measurable_measure_prodMk_right, ProbabilityTheory.Kernel.lintegral_comp, ProbabilityTheory.Kernel.comp_apply', ProbabilityTheory.Kernel.const_apply
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
⊢ Measurable ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ))

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
⊢ Measurable (β := ℝ≥0∞) fun (p : α × β) ↦ μ.rnDeriv ν p.1

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
refine :
  ∀ (s : Set (α × β)) (hs : MeasurableSet s),
    LT.lt (α := ℝ≥0∞) ((ν ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
      ∫⁻ (x : α × β) in s, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in s, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
⊢ (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) =ᶠ[ae (ν ⊗ₘ κ)] fun (p : α × β) ↦ μ.rnDeriv ν p.1

Tactic:
refine ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite (by fun_prop) (by fun_prop) fun s hs _ ↦ ?_

Premises used: MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ν ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t₁ : Set α
t₂ : Set β
ht₁ : MeasurableSet t₁
ht₂ : MeasurableSet t₂
⊢ Measurable (β := ℝ≥0∞) fun (x : α × β) ↦ μ.rnDeriv ν x.1

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ν ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t₁ : Set α
t₂ : Set β
ht₁ : MeasurableSet t₁
ht₂ : MeasurableSet t₂
rw :
  (μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) (t₁ ×ˢ t₂) =
    ∫⁻ (a : α) in t₁, ∫⁻ (b : β) in t₂, μ.rnDeriv ν (a, b).1 ∂(κ : (a : α) → Measure β) a ∂ν
⊢ ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ

Tactic:
rw [Measure.setLIntegral_rnDeriv (hμν.compProd_left _),
      Measure.setLIntegral_compProd (by fun_prop) ht₁ ht₂]

Premises used: MeasureTheory.Measure.setLIntegral_rnDeriv, MeasureTheory.Measure.setLIntegral_compProd, MeasureTheory.Measure.AbsolutelyContinuous.compProd_left
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ν ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t₁ : Set α
t₂ : Set β
ht₁ : MeasurableSet t₁
ht₂ : MeasurableSet t₂
simp :
  (μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) (t₁ ×ˢ t₂) =
    ∫⁻ (a : α) in t₁,
      HMul.hMul (β := ℝ≥0∞) (μ.rnDeriv ν a)
        ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t₂ : ℝ≥0∞) ∂ν
⊢ (μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) (t₁ ×ˢ t₂) =
    ∫⁻ (a : α) in t₁, ∫⁻ (b : β) in t₂, μ.rnDeriv ν (a, b).1 ∂(κ : (a : α) → Measure β) a ∂ν

Tactic:
simp only [MeasureTheory.lintegral_const, MeasurableSet.univ, Measure.restrict_apply,
      univ_inter]

Premises used: MeasureTheory.lintegral_const, MeasureTheory.Measure.restrict_apply, Set.univ_inter, MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ν ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t₁ : Set α
t₂ : Set β
ht₁ : MeasurableSet t₁
ht₂ : MeasurableSet t₂
rw :
  (μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) (t₁ ×ˢ t₂) =
    ∫⁻ (x : α) in t₁, (((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) t₂ ∂μ
rw₁ rw₂ :
  ∫⁻ (a : α) in t₁, (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t₂ ∂μ =
    ∫⁻ (x : α) in t₁, (((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) t₂ ∂μ
⊢ (μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) (t₁ ×ˢ t₂) =
    ∫⁻ (a : α) in t₁,
      HMul.hMul (β := ℝ≥0∞) (μ.rnDeriv ν a)
        ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t₂ : ℝ≥0∞) ∂ν

Tactic:
rw [setLIntegral_rnDeriv_mul hμν (κ.measurable_coe ht₂).aemeasurable ht₁,
      Measure.compProd_apply_prod ht₁ ht₂]

Premises used: Measurable.aemeasurable, MeasureTheory.setLIntegral_rnDeriv_mul, MeasureTheory.Measure.compProd_apply_prod, ProbabilityTheory.Kernel.measurable_coe
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ν ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∀ (t₁ : Set α) (t₂ : Set β),
    MeasurableSet t₁ →
      MeasurableSet t₂ →
        ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
          ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ

Tactic:
have h_key t₁ t₂ : MeasurableSet t₁ → MeasurableSet t₂ →
      ∫⁻ x in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
        ∫⁻ x in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ := by
    intro ht₁ ht₂
    rw [Measure.setLIntegral_rnDeriv (hμν.compProd_left _),
      Measure.setLIntegral_compProd (by fun_prop) ht₁ ht₂]
    simp only [MeasureTheory.lintegral_const, MeasurableSet.univ, Measure.restrict_apply,
      univ_inter]
    rw [setLIntegral_rnDeriv_mul hμν (κ.measurable_coe ht₂).aemeasurable ht₁,
      Measure.compProd_apply_prod ht₁ ht₂]
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ν ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_key :
  ∀ (t₁ : Set α) (t₂ : Set β),
    MeasurableSet t₁ →
      MeasurableSet t₂ →
        ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
          ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
⊢ ∫⁻ (x : α × β) in s, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in s, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ

Tactic:
MeasurableSpace.induction_on_inter generateFrom_prod.symm isPiSystem_prod ?_ ?_ ?_ ?_ s hs

Premises used: isPiSystem_prod, generateFrom_prod, MeasurableSpace.induction_on_inter, Eq.symm
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ν ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_key :
  ∀ (t₁ : Set α) (t₂ : Set β),
    MeasurableSet t₁ →
      MeasurableSet t₂ →
        ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
          ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
refine_1 : ∫⁻ (x : α × β) in ∅, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in ∅, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
refine_2 :
  ∀ (t : Set (α × β))
    (ht :
      Membership.mem (γ := Set (Set (α × β)))
        (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) {s : Set α | MeasurableSet s} {t : Set β | MeasurableSet t})
        t),
    ∫⁻ (x : α × β) in t, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in t, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
refine_3 :
  ∀ (t : Set (α × β)) (htm : MeasurableSet t),
    ∫⁻ (x : α × β) in t, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in t, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ →
      ∫⁻ (x : α × β) in tᶜ, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in tᶜ, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
refine_4 :
  ∀ (f : ℕ → Set (α × β)),
    Pairwise (Function.onFun Disjoint f) →
      ∀ (hfm : ∀ (i : ℕ), MeasurableSet (f i)),
        (∀ (i : ℕ),
            ∫⁻ (x : α × β) in f i, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
              ∫⁻ (x : α × β) in f i, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ) →
          ∫⁻ (x : α × β) in ⋃ (i : ℕ), f i, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
            ∫⁻ (x : α × β) in ⋃ (i : ℕ), f i, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
⊢ ∫⁻ (x : α × β) in s, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in s, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ

Tactic:
refine MeasurableSpace.induction_on_inter generateFrom_prod.symm isPiSystem_prod ?_ ?_ ?_ ?_ s hs
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ν ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_key :
  ∀ (t₁ : Set α) (t₂ : Set β),
    MeasurableSet t₁ →
      MeasurableSet t₂ →
        ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
          ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
⊢ ∫⁻ (x : α × β) in ∅, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in ∅, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ν ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_key :
  ∀ (t₁ : Set α) (t₂ : Set β),
    MeasurableSet t₁ →
      MeasurableSet t₂ →
        ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
          ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
t₁ : Set α
ht₁ : Membership.mem (γ := Set (Set α)) {s : Set α | MeasurableSet s} t₁
t₂ : Set β
ht₂ : Membership.mem (γ := Set (Set β)) {t : Set β | MeasurableSet t} t₂
⊢ ∫⁻ (x : α × β) in (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) t₁ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
    ∫⁻ (x : α × β) in (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) t₁ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ

Tactic:
h_key t₁ t₂ ht₁ ht₂
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ν ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_key :
  ∀ (t₁ : Set α) (t₂ : Set β),
    MeasurableSet t₁ →
      MeasurableSet t₂ →
        ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
          ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
t₁ : Set α
ht₁ : Membership.mem (γ := Set (Set α)) {s : Set α | MeasurableSet s} t₁
t₂ : Set β
ht₂ : Membership.mem (γ := Set (Set β)) {t : Set β | MeasurableSet t} t₂
⊢ ∫⁻ (x : α × β) in (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) t₁ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
    ∫⁻ (x : α × β) in (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) t₁ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ

Tactic:
exact h_key t₁ t₂ ht₁ ht₂
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ν ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_key :
  ∀ (t₁ : Set α) (t₂ : Set β),
    MeasurableSet t₁ →
      MeasurableSet t₂ →
        ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
          ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
t : Set (α × β)
ht : MeasurableSet t
ht_eq : ∫⁻ (x : α × β) in t, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in t, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
refine_3 :
  ∫⁻ (x : α × β), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ - ∫⁻ (x : α × β) in t, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ =
    ∫⁻ (x : α × β), μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ - ∫⁻ (x : α × β) in t, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
refine_3₁ : ∫⁻ (x : α × β) in t, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ ≠ ∞
refine_3₂ : ∫⁻ (x : α × β) in t, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ ≠ ∞
⊢ ∫⁻ (x : α × β) in tᶜ, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in tᶜ, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ

Tactic:
rw [setLIntegral_compl ht, ht_eq, setLIntegral_compl ht]

Premises used: MeasureTheory.setLIntegral_compl