awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : SigmaFinite ν
inst_2 : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero.{u_2} (R := Measure β) ((κ : (a : α) → Measure β) x : Measure β)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
⊢ ν.withDensity (μ.rnDeriv ν) ≪ ν

Tactic:
exact withDensity_absolutelyContinuous _ _

Premises used: MeasureTheory.withDensity_absolutelyContinuous
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : SigmaFinite ν
inst_2 : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero.{u_2} (R := Measure β) ((κ : (a : α) → Measure β) x : Measure β)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
hh :
  ∀ᵐ (x : α) ∂ν.withDensity (μ.rnDeriv ν),
    @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) x) ((κ : (a : α) → Measure β) x)
⊢ ∀ᵐ (x : α) ∂ν.withDensity (μ.rnDeriv ν), False

Tactic:
simp_rw [MutuallySingular.self_iff, (hκ _).ne] at hh

Premises used: MeasureTheory.Measure.MutuallySingular.self_iff, NeZero.ne
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : SigmaFinite ν
inst_2 : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero.{u_2} (R := Measure β) ((κ : (a : α) → Measure β) x : Measure β)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
hh : ∀ᵐ (x : α) ∂ν.withDensity (μ.rnDeriv ν), False
⊢ ν.withDensity (μ.rnDeriv ν) = 0

Tactic:
ae_eq_bot.mp (Filter.eventually_false_iff_eq_bot.mp hh)

Premises used: Filter.eventually_false_iff_eq_bot, MeasureTheory.ae_eq_bot, Iff.mp
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : SigmaFinite ν
inst_2 : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero.{u_2} (R := Measure β) ((κ : (a : α) → Measure β) x : Measure β)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
hh : ∀ᵐ (x : α) ∂ν.withDensity (μ.rnDeriv ν), False
⊢ ν.withDensity (μ.rnDeriv ν) = 0

Tactic:
exact ae_eq_bot.mp (Filter.eventually_false_iff_eq_bot.mp hh)

Premises used: Filter.eventually_false_iff_eq_bot, MeasureTheory.ae_eq_bot, Iff.mp
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
rw : μ ⊗ₘ κ ⟂ₘ (ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)) ⊗ₘ η
| μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η

Tactic:
rw [ν.haveLebesgueDecomposition_add μ]

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_add
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
conv_lhs : μ ⊗ₘ κ ⟂ₘ (ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)) ⊗ₘ η ↔ μ ⊗ₘ κ ⟂ₘ μ ⊗ₘ η
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η ↔ μ ⊗ₘ κ ⟂ₘ μ ⊗ₘ η

Tactic:
conv_lhs => rw [ν.haveLebesgueDecomposition_add μ]

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_add
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
rw : μ ⊗ₘ κ ⟂ₘ ν.singularPart μ ⊗ₘ η ∧ μ ⊗ₘ κ ⟂ₘ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η ↔ μ ⊗ₘ κ ⟂ₘ μ ⊗ₘ η
⊢ μ ⊗ₘ κ ⟂ₘ (ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)) ⊗ₘ η ↔ μ ⊗ₘ κ ⟂ₘ μ ⊗ₘ η

Tactic:
rw [compProd_add_left, MutuallySingular.add_right_iff]

Premises used: MeasureTheory.Measure.compProd_add_left, MeasureTheory.Measure.MutuallySingular.add_right_iff
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
simp : μ ⊗ₘ κ ⟂ₘ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η ↔ μ ⊗ₘ κ ⟂ₘ μ ⊗ₘ η
⊢ μ ⊗ₘ κ ⟂ₘ ν.singularPart μ ⊗ₘ η ∧ μ ⊗ₘ κ ⟂ₘ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η ↔ μ ⊗ₘ κ ⟂ₘ μ ⊗ₘ η

Tactic:
simp only [(mutuallySingular_singularPart ν μ).symm.compProd_of_left κ η, true_and]

Premises used: MeasureTheory.Measure.MutuallySingular.compProd_of_left, MeasureTheory.Measure.mutuallySingular_singularPart, true_and, MeasureTheory.Measure.MutuallySingular.symm
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
⊢ μ ⊗ₘ κ ⟂ₘ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η ↔ μ ⊗ₘ κ ⟂ₘ μ ⊗ₘ η

Tactic:
⟨fun h ↦ h.mono_ac .rfl ?_, fun h ↦ h.mono_ac .rfl ?_⟩

Premises used: Iff.intro, MeasureTheory.Measure.AbsolutelyContinuous.rfl, MeasureTheory.Measure.MutuallySingular.mono_ac
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
refine_1 : ∀ (h : μ ⊗ₘ κ ⟂ₘ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η), μ ⊗ₘ η ≪ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η
refine_2 : ∀ (h : μ ⊗ₘ κ ⟂ₘ μ ⊗ₘ η), μ.withDensity (ν.rnDeriv μ) ⊗ₘ η ≪ μ ⊗ₘ η
⊢ μ ⊗ₘ κ ⟂ₘ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η ↔ μ ⊗ₘ κ ⟂ₘ μ ⊗ₘ η

Tactic:
refine ⟨fun h ↦ h.mono_ac .rfl ?_, fun h ↦ h.mono_ac .rfl ?_⟩
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
h : μ ⊗ₘ κ ⟂ₘ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η
⊢ μ ⊗ₘ η ≪ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η

Tactic:
(absolutelyContinuous_withDensity_rnDeriv hμν).compProd_left _

Premises used: MeasureTheory.Measure.absolutelyContinuous_withDensity_rnDeriv, MeasureTheory.Measure.AbsolutelyContinuous.compProd_left
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
h : μ ⊗ₘ κ ⟂ₘ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η
⊢ μ ⊗ₘ η ≪ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η

Tactic:
exact (absolutelyContinuous_withDensity_rnDeriv hμν).compProd_left _

Premises used: MeasureTheory.Measure.absolutelyContinuous_withDensity_rnDeriv, MeasureTheory.Measure.AbsolutelyContinuous.compProd_left
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
h : μ ⊗ₘ κ ⟂ₘ μ ⊗ₘ η
⊢ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η ≪ μ ⊗ₘ η

Tactic:
(withDensity_absolutelyContinuous μ (ν.rnDeriv μ)).compProd_left _

Premises used: MeasureTheory.Measure.rnDeriv, MeasureTheory.withDensity_absolutelyContinuous, MeasureTheory.Measure.AbsolutelyContinuous.compProd_left
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
h : μ ⊗ₘ κ ⟂ₘ μ ⊗ₘ η
⊢ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η ≪ μ ⊗ₘ η

Tactic:
exact (withDensity_absolutelyContinuous μ (ν.rnDeriv μ)).compProd_left _

Premises used: MeasureTheory.Measure.rnDeriv, MeasureTheory.withDensity_absolutelyContinuous, MeasureTheory.Measure.AbsolutelyContinuous.compProd_left
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
rw : (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)) ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
| μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η

Tactic:
rw [μ.haveLebesgueDecomposition_add ν]

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_add
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
conv_lhs :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)) ⊗ₘ κ ⟂ₘ ν ⊗ₘ η ↔
    ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η ↔ ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η

Tactic:
conv_lhs => rw [μ.haveLebesgueDecomposition_add ν]

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_add
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
rw :
  μ.singularPart ν ⊗ₘ κ ⟂ₘ ν ⊗ₘ η ∧ ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ ⟂ₘ ν ⊗ₘ η ↔
    ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η
⊢ (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)) ⊗ₘ κ ⟂ₘ ν ⊗ₘ η ↔
    ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η

Tactic:
rw [compProd_add_left, MutuallySingular.add_left_iff]

Premises used: MeasureTheory.Measure.MutuallySingular.add_left_iff, MeasureTheory.Measure.compProd_add_left
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
simp : ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ ⟂ₘ ν ⊗ₘ η ↔ ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η
⊢ μ.singularPart ν ⊗ₘ κ ⟂ₘ ν ⊗ₘ η ∧ ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ ⟂ₘ ν ⊗ₘ η ↔
    ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η

Tactic:
simp only [(mutuallySingular_singularPart μ ν).compProd_of_left κ η, true_and]

Premises used: MeasureTheory.Measure.MutuallySingular.compProd_of_left, MeasureTheory.Measure.mutuallySingular_singularPart, true_and
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
rw :
  ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ ⟂ₘ ν.withDensity (μ.rnDeriv ν) ⊗ₘ η ↔
    ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η
⊢ ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ ⟂ₘ ν ⊗ₘ η ↔ ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η

Tactic:
rw [(withDensity_absolutelyContinuous ν (μ.rnDeriv ν)).mutuallySingular_compProd_iff]

Premises used: MeasureTheory.Measure.rnDeriv, MeasureTheory.withDensity_absolutelyContinuous, MeasureTheory.Measure.AbsolutelyContinuous.mutuallySingular_compProd_iff
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
⊢ ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ ⟂ₘ ν.withDensity (μ.rnDeriv ν) ⊗ₘ η ↔
    ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η

Tactic:
⟨fun h ξ hξ hξμ hξν ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
refine_1 :
  ∀ (h : ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ ⟂ₘ ν.withDensity (μ.rnDeriv ν) ⊗ₘ η) (ξ : Measure α) (hξ : SFinite ξ)
    (hξμ : ξ ≪ μ) (hξν : ξ ≪ ν), ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η
refine_2 :
  ∀ (h : ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η),
    ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ ⟂ₘ ν.withDensity (μ.rnDeriv ν) ⊗ₘ η
⊢ ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ ⟂ₘ ν.withDensity (μ.rnDeriv ν) ⊗ₘ η ↔
    ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η

Tactic:
refine ⟨fun h ξ hξ hξμ hξν ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
h : ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ ⟂ₘ ν.withDensity (μ.rnDeriv ν) ⊗ₘ η
ξ : Measure α
hξ : SFinite ξ
hξμ : ξ ≪ μ
hξν : ξ ≪ ν
⊢ ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η

Tactic:
h.mono_ac ((hξμ.withDensity_rnDeriv hξν).compProd_left _)
      ((hξμ.withDensity_rnDeriv hξν).compProd_left _)

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.withDensity_rnDeriv, MeasureTheory.Measure.AbsolutelyContinuous.compProd_left, MeasureTheory.Measure.MutuallySingular.mono_ac
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
h : ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ ⟂ₘ ν.withDensity (μ.rnDeriv ν) ⊗ₘ η
ξ : Measure α
hξ : SFinite ξ
hξμ : ξ ≪ μ
hξν : ξ ≪ ν
⊢ ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η

Tactic:
exact h.mono_ac ((hξμ.withDensity_rnDeriv hξν).compProd_left _)
      ((hξμ.withDensity_rnDeriv hξν).compProd_left _)

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.withDensity_rnDeriv, MeasureTheory.Measure.AbsolutelyContinuous.compProd_left, MeasureTheory.Measure.MutuallySingular.mono_ac
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
h : ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η
⊢ ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ ⟂ₘ ν.withDensity (μ.rnDeriv ν) ⊗ₘ η

Tactic:
h _ ?_ ?_ ?_
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
h : ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η
refine_2 : SFinite (ν.withDensity (μ.rnDeriv ν))
refine_2₁ : ν.withDensity (μ.rnDeriv ν) ≪ μ
refine_2₂ : ν.withDensity (μ.rnDeriv ν) ≪ ν
⊢ ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ ⟂ₘ ν.withDensity (μ.rnDeriv ν) ⊗ₘ η

Tactic:
refine h _ ?_ ?_ ?_
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
h : ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η
⊢ SFinite (ν.withDensity (μ.rnDeriv ν))

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
h : ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η
⊢ ν.withDensity (μ.rnDeriv ν) ≪ μ

Tactic:
absolutelyContinuous_of_le (withDensity_rnDeriv_le _ _)

Premises used: MeasureTheory.Measure.withDensity_rnDeriv_le, MeasureTheory.Measure.absolutelyContinuous_of_le
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
h : ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η
⊢ ν.withDensity (μ.rnDeriv ν) ≪ μ

Tactic:
exact absolutelyContinuous_of_le (withDensity_rnDeriv_le _ _)

Premises used: MeasureTheory.Measure.withDensity_rnDeriv_le, MeasureTheory.Measure.absolutelyContinuous_of_le
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
h : ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η
⊢ ν.withDensity (μ.rnDeriv ν) ≪ ν

Tactic:
withDensity_absolutelyContinuous ν (μ.rnDeriv ν)

Premises used: MeasureTheory.Measure.rnDeriv, MeasureTheory.withDensity_absolutelyContinuous
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
h : ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η
⊢ ν.withDensity (μ.rnDeriv ν) ≪ ν

Tactic:
exact withDensity_absolutelyContinuous ν (μ.rnDeriv ν)

Premises used: MeasureTheory.Measure.rnDeriv, MeasureTheory.withDensity_absolutelyContinuous
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hκη : μ ⊗ₘ κ ≪ ν ⊗ₘ η
⊢ μ ⊗ₘ κ ≪ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η + ν.singularPart μ ⊗ₘ η

Tactic:
rw [ν.haveLebesgueDecomposition_add μ, compProd_add_left, add_comm] at hκη

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_add, add_comm, MeasureTheory.Measure.compProd_add_left
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hκη : μ ⊗ₘ κ ≪ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η + ν.singularPart μ ⊗ₘ η
⊢ μ ⊗ₘ κ ≪ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η

Tactic:
have h := absolutelyContinuous_of_add_of_mutuallySingular hκη
    ((mutuallySingular_singularPart _ _).symm.compProd_of_left _ _)
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hκη : μ ⊗ₘ κ ≪ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η + ν.singularPart μ ⊗ₘ η
h : μ ⊗ₘ κ ≪ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η
⊢ μ ⊗ₘ κ ≪ μ ⊗ₘ η

Tactic:
h.trans (AbsolutelyContinuous.compProd_left ?_ _)

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.trans, MeasureTheory.Measure.AbsolutelyContinuous.compProd_left
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hκη : μ ⊗ₘ κ ≪ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η + ν.singularPart μ ⊗ₘ η
h : μ ⊗ₘ κ ≪ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η
refine : μ.withDensity (ν.rnDeriv μ) ≪ μ
⊢ μ ⊗ₘ κ ≪ μ ⊗ₘ η

Tactic:
refine h.trans (AbsolutelyContinuous.compProd_left ?_ _)

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.trans, MeasureTheory.Measure.AbsolutelyContinuous.compProd_left
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hκη : μ ⊗ₘ κ ≪ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η + ν.singularPart μ ⊗ₘ η
h : μ ⊗ₘ κ ≪ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η
⊢ μ.withDensity (ν.rnDeriv μ) ≪ μ

Tactic:
withDensity_absolutelyContinuous _ _

Premises used: MeasureTheory.withDensity_absolutelyContinuous
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hκη : μ ⊗ₘ κ ≪ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η + ν.singularPart μ ⊗ₘ η
h : μ ⊗ₘ κ ≪ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η
⊢ μ.withDensity (ν.rnDeriv μ) ≪ μ

Tactic:
exact withDensity_absolutelyContinuous _ _

Premises used: MeasureTheory.withDensity_absolutelyContinuous
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : IsSFiniteKernel κ
inst_3 : IsSFiniteKernel η
inst_4 : ∀ (x : α), NeZero.{u_2} (R := Measure β) ((κ : (a : α) → Measure β) x : Measure β)
⊢ μ ⊗ₘ κ ≪ ν ⊗ₘ η ↔ μ ≪ ν ∧ μ ⊗ₘ κ ≪ μ ⊗ₘ η

Tactic:
⟨fun h ↦ ⟨absolutelyContinuous_of_compProd h, absolutelyContinuous_compProd_of_compProd h⟩,
    fun h ↦ h.1.compProd_of_compProd h.2⟩

Premises used: MeasureTheory.Measure.absolutelyContinuous_of_compProd, MeasureTheory.Measure.AbsolutelyContinuous.compProd_of_compProd, MeasureTheory.Measure.absolutelyContinuous_compProd_of_compProd, And.right, And.left, And.intro, Iff.intro
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ_1 : Kernel α β
η_1 : Kernel γ δ
x : α × γ
κ : Kernel α β
η : Kernel γ δ
h : IsSFiniteKernel κ ∧ IsSFiniteKernel η
⊢ IsSFiniteKernel κ

Tactic:
have hκ := h.1
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ_1 : Kernel α β
η_1 : Kernel γ δ
x : α × γ
κ : Kernel α β
η : Kernel γ δ
h : IsSFiniteKernel κ ∧ IsSFiniteKernel η
hκ : IsSFiniteKernel κ
⊢ IsSFiniteKernel η

Tactic:
have hη := h.2
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ_1 : Kernel α β
η_1 : Kernel γ δ
x : α × γ
κ : Kernel α β
η : Kernel γ δ
h : IsSFiniteKernel κ ∧ IsSFiniteKernel η
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
⊢ Measurable (β := Measure (β × δ)) fun (x : α × γ) ↦
    Measure.prod ((κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2)

Tactic:
Measure.measurable_of_measurable_coe _ fun s hs ↦ ?_

Premises used: MeasureTheory.Measure.measurable_of_measurable_coe
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ_1 : Kernel α β
η_1 : Kernel γ δ
x : α × γ
κ : Kernel α β
η : Kernel γ δ
h : IsSFiniteKernel κ ∧ IsSFiniteKernel η
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
refine :
  ∀ (s : Set (β × δ)) (hs : MeasurableSet s),
    Measurable (β := ℝ≥0∞) fun (b : α × γ) ↦
      (Measure.prod ((κ : (a : α) → Measure β) b.1) ((η : (a : γ) → Measure δ) b.2) : (a : Set (β × δ)) → ℝ≥0∞) s
⊢ Measurable (β := Measure (β × δ)) fun (x : α × γ) ↦
    Measure.prod ((κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2)

Tactic:
refine Measure.measurable_of_measurable_coe _ fun s hs ↦ ?_

Premises used: MeasureTheory.Measure.measurable_of_measurable_coe
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ_1 : Kernel α β
η_1 : Kernel γ δ
x : α × γ
κ : Kernel α β
η : Kernel γ δ
h : IsSFiniteKernel κ ∧ IsSFiniteKernel η
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set (β × δ)
hs : MeasurableSet s
simp_rw :
  Measurable (β := ℝ≥0∞) fun (b : α × γ) ↦
    ∫⁻ (x : β),
      (((η : (a : γ) → Measure δ) b.2 : Measure δ) : (a : Set δ) → ℝ≥0∞)
        (Prod.mk x ⁻¹' s) ∂(κ : (a : α) → Measure β) b.1
⊢ Measurable (β := ℝ≥0∞) fun (b : α × γ) ↦
    (Measure.prod ((κ : (a : α) → Measure β) b.1) ((η : (a : γ) → Measure δ) b.2) : (a : Set (β × δ)) → ℝ≥0∞) s

Tactic:
simp_rw [Measure.prod_apply hs]

Premises used: MeasureTheory.Measure.prod_apply
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ_1 : Kernel α β
η_1 : Kernel γ δ
x : α × γ
κ : Kernel α β
η : Kernel γ δ
h : IsSFiniteKernel κ ∧ IsSFiniteKernel η
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set (β × δ)
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : α × γ) ↦
    ∫⁻ (x : β),
      (((η : (a : γ) → Measure δ) b.2 : Measure δ) : (a : Set δ) → ℝ≥0∞)
        (Prod.mk x ⁻¹' s) ∂(κ : (a : α) → Measure β) b.1

Tactic:
Measurable.lintegral_kernel_prod_right'
        (f := fun y ↦ prodMkLeft α η y.1 (Prod.mk y.2 ⁻¹' s)) (κ := prodMkRight γ κ) ?_

Premises used: Measurable.lintegral_kernel_prod_right'