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 α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : SFinite ν
pos : ∀ (hκ : IsSFiniteKernel κ), μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
neg : ∀ (hκ : ¬IsSFiniteKernel κ), μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η

Tactic:
by_cases hκ : IsSFiniteKernel κ

Premises used: ProbabilityTheory.IsSFiniteKernel
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : SFinite ν
hκ : ¬IsSFiniteKernel κ
neg : 0 ⟂ₘ ν ⊗ₘ η
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η

Tactic:
rw [compProd_of_not_isSFiniteKernel _ _ hκ]

Premises used: MeasureTheory.Measure.compProd_of_not_isSFiniteKernel
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : SFinite ν
hκ : ¬IsSFiniteKernel κ
⊢ 0 ⟂ₘ ν ⊗ₘ η

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : SFinite ν
hκ : IsSFiniteKernel κ
pos : ∀ (hη : IsSFiniteKernel η), μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
neg : ∀ (hη : ¬IsSFiniteKernel η), μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η

Tactic:
by_cases hη : IsSFiniteKernel η

Premises used: ProbabilityTheory.IsSFiniteKernel
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : SFinite ν
hκ : IsSFiniteKernel κ
hη : ¬IsSFiniteKernel η
neg : μ ⊗ₘ κ ⟂ₘ 0
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η

Tactic:
rw [compProd_of_not_isSFiniteKernel _ _ hη]

Premises used: MeasureTheory.Measure.compProd_of_not_isSFiniteKernel
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : SFinite ν
hκ : IsSFiniteKernel κ
hη : ¬IsSFiniteKernel η
⊢ μ ⊗ₘ κ ⟂ₘ 0

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : SFinite ν
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η

Tactic:
⟨hμν.nullSet ×ˢ univ, hμν.measurableSet_nullSet.prod .univ, ?_⟩

Premises used: SProd.sprod, Set.univ, MeasurableSet.prod, MeasureTheory.Measure.MutuallySingular.measurableSet_nullSet, MeasureTheory.Measure.MutuallySingular.nullSet, MeasureTheory.Measure.MutuallySingular, And.intro, Exists.intro, MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : SFinite ν
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
pos :
  Eq (α := ℝ≥0∞) ((μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) hμν.nullSet univ) : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) hμν.nullSet univ)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η

Tactic:
refine ⟨hμν.nullSet ×ˢ univ, hμν.measurableSet_nullSet.prod .univ, ?_⟩
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : SFinite ν
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
pos :
  ∫⁻ (a : α) in hμν.nullSet, (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ ∂μ = 0 ∧
    Eq (α := ℝ≥0∞)
      ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞)
          (SProd.sprod (β := Set β) hμν.nullSetᶜ univ ∪ SProd.sprod (α := Set α) (β := Set β) univ univᶜ) :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) hμν.nullSet univ) : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) hμν.nullSet univ)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [compProd_apply_prod hμν.measurableSet_nullSet .univ, compl_prod_eq_union]

Premises used: MeasureTheory.Measure.MutuallySingular.measurableSet_nullSet, Set.compl_prod_eq_union, MeasureTheory.Measure.compProd_apply_prod, MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : SFinite ν
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
pos :
  Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) hμν.nullSetᶜ univ) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∫⁻ (a : α) in hμν.nullSet, (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ ∂μ = 0 ∧
    Eq (α := ℝ≥0∞)
      ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞)
          (SProd.sprod (β := Set β) hμν.nullSetᶜ univ ∪ SProd.sprod (α := Set α) (β := Set β) univ univᶜ) :
        ℝ≥0∞)
      (0 : ℝ≥0∞)

Tactic:
simp only [MutuallySingular.restrict_nullSet, lintegral_zero_measure, compl_univ,
    prod_empty, union_empty, true_and]

Premises used: Set.union_empty, MeasureTheory.Measure.MutuallySingular.restrict_nullSet, Set.prod_empty, Set.compl_univ, MeasureTheory.lintegral_zero_measure, true_and
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : SFinite ν
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
pos : ∫⁻ (a : α) in hμν.nullSetᶜ, (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ ∂ν = 0
⊢ Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) hμν.nullSetᶜ univ) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [compProd_apply_prod hμν.measurableSet_nullSet.compl .univ]

Premises used: MeasureTheory.Measure.MutuallySingular.measurableSet_nullSet, MeasurableSet.compl, MeasureTheory.Measure.compProd_apply_prod, MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : SFinite ν
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
⊢ ∫⁻ (a : α) in hμν.nullSetᶜ, (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ ∂ν = 0

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
ξ : Measure α
inst : SFinite μ
inst_1 : SFinite ν
inst_2 : IsSFiniteKernel κ
inst_3 : IsSFiniteKernel η
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
hμ : ξ ≪ μ
hν : ξ ≪ ν
⊢ MeasurableSet h.nullSet

Tactic:
have hs : MeasurableSet h.nullSet := h.measurableSet_nullSet
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
ξ : Measure α
inst : SFinite μ
inst_1 : SFinite ν
inst_2 : IsSFiniteKernel κ
inst_3 : IsSFiniteKernel η
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
hμ : ξ ≪ μ
hν : ξ ≪ ν
hs : MeasurableSet h.nullSet
⊢ Eq (α := ℝ≥0∞) ((μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) h.nullSet : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
have hμ_zero : (μ ⊗ₘ κ) h.nullSet = 0 := h.measure_nullSet
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
ξ : Measure α
inst : SFinite μ
inst_1 : SFinite ν
inst_2 : IsSFiniteKernel κ
inst_3 : IsSFiniteKernel η
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
hμ : ξ ≪ μ
hν : ξ ≪ ν
hs : MeasurableSet h.nullSet
hμ_zero : Eq (α := ℝ≥0∞) ((μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) h.nullSet : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) h.nullSetᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
have hν_zero : (ν ⊗ₘ η) h.nullSetᶜ = 0 := h.measure_compl_nullSet
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
ξ : Measure α
inst : SFinite μ
inst_1 : SFinite ν
inst_2 : IsSFiniteKernel κ
inst_3 : IsSFiniteKernel η
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
hμ : ξ ≪ μ
hν : ξ ≪ ν
hs : MeasurableSet h.nullSet
hμ_zero : Eq (α := ℝ≥0∞) ((μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) h.nullSet : ℝ≥0∞) (0 : ℝ≥0∞)
hν_zero : Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) h.nullSetᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
rw :
  ∀
    (hμ_zero :
      (ae μ).EventuallyEq (β := ℝ≥0∞)
        (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSet)) 0)
    (hν_zero :
      (ae ν).EventuallyEq (β := ℝ≥0∞)
        (fun (a : α) ↦ (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSetᶜ)) 0),
    ∀ᵐ (x : α) ∂ξ, @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) x) ((η : (a : α) → Measure β) x)
rw₁ :
  ∀
    (hμ_zero :
      (ae μ).EventuallyEq (β := ℝ≥0∞)
        (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSet)) 0)
    (hν_zero :
      ∫⁻ (a : α), (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSetᶜ) ∂ν = 0),
    AEMeasurable (β := ℝ≥0∞)
      (fun (a : α) ↦ (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSetᶜ)) ν
rw₂ :
  ∀
    (hμ_zero :
      ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSet) ∂μ = 0)
    (hν_zero :
      ∫⁻ (a : α), (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSetᶜ) ∂ν = 0),
    AEMeasurable (β := ℝ≥0∞)
      (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSet)) μ
rw₃ :
  ∀
    (hμ_zero :
      ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSet) ∂μ = 0)
    (hν_zero : Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) h.nullSetᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
    MeasurableSet h.nullSetᶜ
rw₄ : MeasurableSet h.nullSet
⊢ ∀ᵐ (x : α) ∂ξ, @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) x) ((η : (a : α) → Measure β) x)

Tactic:
rw [compProd_apply, lintegral_eq_zero_iff'] at hμ_zero hν_zero

Premises used: MeasureTheory.lintegral_eq_zero_iff', MeasureTheory.Measure.compProd_apply
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
ξ : Measure α
inst : SFinite μ
inst_1 : SFinite ν
inst_2 : IsSFiniteKernel κ
inst_3 : IsSFiniteKernel η
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
hμ : ξ ≪ μ
hν : ξ ≪ ν
hs : MeasurableSet h.nullSet
hμ_zero :
  (ae μ).EventuallyEq (β := ℝ≥0∞)
    (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSet)) 0
hν_zero :
  (ae ν).EventuallyEq (β := ℝ≥0∞)
    (fun (a : α) ↦ (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSetᶜ)) 0
h₁ :
  ∀ (x : α)
    (hxμ :
      Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' h.nullSet) : ℝ≥0∞)
        (0 x : ℝ≥0∞))
    (hxν :
      Eq (α := ℝ≥0∞)
        ((((η : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' h.nullSetᶜ) : ℝ≥0∞)
        (0 x : ℝ≥0∞)),
    @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) x) ((η : (a : α) → Measure β) x)
⊢ ∀ᵐ (x : α) ∂ξ, @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) x) ((η : (a : α) → Measure β) x)

Tactic:
filter_upwards [hμ hμ_zero, hν hν_zero] with x hxμ hxν
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
ξ : Measure α
inst : SFinite μ
inst_1 : SFinite ν
inst_2 : IsSFiniteKernel κ
inst_3 : IsSFiniteKernel η
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
hμ : ξ ≪ μ
hν : ξ ≪ ν
hs : MeasurableSet h.nullSet
hμ_zero :
  (ae μ).EventuallyEq (β := ℝ≥0∞)
    (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSet)) 0
hν_zero :
  (ae ν).EventuallyEq (β := ℝ≥0∞)
    (fun (a : α) ↦ (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSetᶜ)) 0
x : α
hxμ :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' h.nullSet) : ℝ≥0∞)
    (0 x : ℝ≥0∞)
hxν :
  Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' h.nullSetᶜ) : ℝ≥0∞)
    (0 x : ℝ≥0∞)
⊢ @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) x) ((η : (a : α) → Measure β) x)

Tactic:
⟨Prod.mk x ⁻¹' h.nullSet, measurable_prodMk_left hs, ⟨hxμ, hxν⟩⟩

Premises used: Prod.mk, MeasureTheory.Measure.MutuallySingular.nullSet, Set.preimage, MeasureTheory.Measure.MutuallySingular, And.intro, Exists.intro, measurable_prodMk_left
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
ξ : Measure α
inst : SFinite μ
inst_1 : SFinite ν
inst_2 : IsSFiniteKernel κ
inst_3 : IsSFiniteKernel η
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
hμ : ξ ≪ μ
hν : ξ ≪ ν
hs : MeasurableSet h.nullSet
hμ_zero :
  (ae μ).EventuallyEq (β := ℝ≥0∞)
    (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSet)) 0
hν_zero :
  (ae ν).EventuallyEq (β := ℝ≥0∞)
    (fun (a : α) ↦ (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSetᶜ)) 0
x : α
hxμ :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' h.nullSet) : ℝ≥0∞)
    (0 x : ℝ≥0∞)
hxν :
  Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' h.nullSetᶜ) : ℝ≥0∞)
    (0 x : ℝ≥0∞)
⊢ @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) x) ((η : (a : α) → Measure β) x)

Tactic:
exact ⟨Prod.mk x ⁻¹' h.nullSet, measurable_prodMk_left hs, ⟨hxμ, hxν⟩⟩
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
ξ : Measure α
inst : SFinite μ
inst_1 : SFinite ν
inst_2 : IsSFiniteKernel κ
inst_3 : IsSFiniteKernel η
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
hμ : ξ ≪ μ
hν : ξ ≪ ν
hs : MeasurableSet h.nullSet
hμ_zero :
  (ae μ).EventuallyEq (β := ℝ≥0∞)
    (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSet)) 0
hν_zero : ∫⁻ (a : α), (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSetᶜ) ∂ν = 0
⊢ AEMeasurable (β := ℝ≥0∞)
    (fun (a : α) ↦ (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSetᶜ)) ν

Tactic:
(Kernel.measurable_kernel_prodMk_left hs.compl).aemeasurable

Premises used: Measurable.aemeasurable, MeasurableSet.compl, ProbabilityTheory.Kernel.measurable_kernel_prodMk_left
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
ξ : Measure α
inst : SFinite μ
inst_1 : SFinite ν
inst_2 : IsSFiniteKernel κ
inst_3 : IsSFiniteKernel η
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
hμ : ξ ≪ μ
hν : ξ ≪ ν
hs : MeasurableSet h.nullSet
hμ_zero :
  (ae μ).EventuallyEq (β := ℝ≥0∞)
    (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSet)) 0
hν_zero : ∫⁻ (a : α), (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSetᶜ) ∂ν = 0
⊢ AEMeasurable (β := ℝ≥0∞)
    (fun (a : α) ↦ (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSetᶜ)) ν

Tactic:
exact (Kernel.measurable_kernel_prodMk_left hs.compl).aemeasurable

Premises used: Measurable.aemeasurable, MeasurableSet.compl, ProbabilityTheory.Kernel.measurable_kernel_prodMk_left
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
ξ : Measure α
inst : SFinite μ
inst_1 : SFinite ν
inst_2 : IsSFiniteKernel κ
inst_3 : IsSFiniteKernel η
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
hμ : ξ ≪ μ
hν : ξ ≪ ν
hs : MeasurableSet h.nullSet
hμ_zero : ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSet) ∂μ = 0
hν_zero : ∫⁻ (a : α), (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSetᶜ) ∂ν = 0
⊢ AEMeasurable (β := ℝ≥0∞)
    (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSet)) μ

Tactic:
(Kernel.measurable_kernel_prodMk_left hs).aemeasurable

Premises used: Measurable.aemeasurable, ProbabilityTheory.Kernel.measurable_kernel_prodMk_left
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
ξ : Measure α
inst : SFinite μ
inst_1 : SFinite ν
inst_2 : IsSFiniteKernel κ
inst_3 : IsSFiniteKernel η
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
hμ : ξ ≪ μ
hν : ξ ≪ ν
hs : MeasurableSet h.nullSet
hμ_zero : ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSet) ∂μ = 0
hν_zero : ∫⁻ (a : α), (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSetᶜ) ∂ν = 0
⊢ AEMeasurable (β := ℝ≥0∞)
    (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSet)) μ

Tactic:
exact (Kernel.measurable_kernel_prodMk_left hs).aemeasurable

Premises used: Measurable.aemeasurable, ProbabilityTheory.Kernel.measurable_kernel_prodMk_left
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
ξ : Measure α
inst : SFinite μ
inst_1 : SFinite ν
inst_2 : IsSFiniteKernel κ
inst_3 : IsSFiniteKernel η
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
hμ : ξ ≪ μ
hν : ξ ≪ ν
hs : MeasurableSet h.nullSet
hμ_zero : ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSet) ∂μ = 0
hν_zero : Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) h.nullSetᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ MeasurableSet h.nullSetᶜ

Tactic:
hs.compl

Premises used: MeasurableSet.compl
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
ξ : Measure α
inst : SFinite μ
inst_1 : SFinite ν
inst_2 : IsSFiniteKernel κ
inst_3 : IsSFiniteKernel η
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
hμ : ξ ≪ μ
hν : ξ ≪ ν
hs : MeasurableSet h.nullSet
hμ_zero : ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSet) ∂μ = 0
hν_zero : Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) h.nullSetᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ MeasurableSet h.nullSetᶜ

Tactic:
exact hs.compl

Premises used: MeasurableSet.compl
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
ξ : Measure α
inst : SFinite μ
inst_1 : SFinite ν
inst_2 : IsSFiniteKernel κ
inst_3 : IsSFiniteKernel η
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
hμ : ξ ≪ μ
hν : ξ ≪ ν
hs : MeasurableSet h.nullSet
hμ_zero : Eq (α := ℝ≥0∞) ((μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) h.nullSet : ℝ≥0∞) (0 : ℝ≥0∞)
hν_zero : Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) h.nullSetᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ MeasurableSet h.nullSet

Tactic:
hs
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
ξ : Measure α
inst : SFinite μ
inst_1 : SFinite ν
inst_2 : IsSFiniteKernel κ
inst_3 : IsSFiniteKernel η
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
hμ : ξ ≪ μ
hν : ξ ≪ ν
hs : MeasurableSet h.nullSet
hμ_zero : Eq (α := ℝ≥0∞) ((μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) h.nullSet : ℝ≥0∞) (0 : ℝ≥0∞)
hν_zero : Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) h.nullSetᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ MeasurableSet h.nullSet

Tactic:
exact hs
-- 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 β)
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ ↔ μ ⟂ₘ ν

Tactic:
⟨fun h ↦ ?_, fun h ↦ h.compProd_of_left _ _⟩

Premises used: MeasureTheory.Measure.MutuallySingular.compProd_of_left, Iff.intro
-- 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 β)
refine : ∀ (h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ), μ ⟂ₘ ν
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ ↔ μ ⟂ₘ ν

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.compProd_of_left _ _⟩
-- 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 : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
rw : ν.withDensity (μ.rnDeriv ν) = 0
⊢ μ ⟂ₘ ν

Tactic:
rw [← withDensity_rnDeriv_eq_zero]

Premises used: MeasureTheory.Measure.withDensity_rnDeriv_eq_zero
-- 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 : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
refine_3 :
  ∀
    (hh :
      ∀ᵐ (x : α) ∂ν.withDensity (μ.rnDeriv ν),
        @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) x) ((κ : (a : α) → Measure β) x)),
    ν.withDensity (μ.rnDeriv ν) = 0
refine_1 : ν.withDensity (μ.rnDeriv ν) ≪ μ
refine_2 : ν.withDensity (μ.rnDeriv ν) ≪ ν
⊢ ν.withDensity (μ.rnDeriv ν) = 0

Tactic:
have hh := mutuallySingular_of_mutuallySingular_compProd h ?_ ?_
    (ξ := ν.withDensity (μ.rnDeriv ν))
-- 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:
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 : SFinite μ
inst_1 : SigmaFinite ν
inst_2 : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero.{u_2} (R := Measure β) ((κ : (a : α) → Measure β) x : Measure β)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
⊢ ν.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 : SFinite μ
inst_1 : SigmaFinite ν
inst_2 : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero.{u_2} (R := Measure β) ((κ : (a : α) → Measure β) x : Measure β)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
⊢ ν.withDensity (μ.rnDeriv ν) ≪ ν

Tactic:
withDensity_absolutelyContinuous _ _

Premises used: MeasureTheory.withDensity_absolutelyContinuous