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 α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set ((α × β) × γ)
hs : MeasurableSet s
pos :
  ∫⁻ (a : α),
      (((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
        (Prod.mk a ⁻¹' (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) ⁻¹' s) ∂μ =
    ∫⁻ (a : α),
      ∫⁻ (b : β),
        (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (Prod.mk (a, b) ⁻¹' s) ∂(κ : (a : α) → Measure β) a ∂μ
pos₁ :
  Measurable (β := ℝ≥0∞) fun (a : α × β) ↦
    (((η : (a : α × β) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk a ⁻¹' s)
⊢ Eq (α := ℝ≥0∞)
    ((map (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) (μ ⊗ₘ (κ ⊗ₖ η)) :
          (a : Set ((α × β) × γ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((μ ⊗ₘ κ ⊗ₘ η : (a : Set ((α × β) × γ)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [Measure.compProd_apply hs, Measure.map_apply (by fun_prop) hs,
    Measure.compProd_apply (hs.preimage (by fun_prop)), Measure.lintegral_compProd]

Premises used: MeasurableSet.preimage, MeasureTheory.Measure.map_apply, MeasureTheory.Measure.compProd_apply, MeasureTheory.Measure.lintegral_compProd
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set ((α × β) × γ)
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (a : α × β) ↦
    (((η : (a : α × β) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk a ⁻¹' s)

Tactic:
Kernel.measurable_kernel_prodMk_left hs

Premises used: 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 α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set ((α × β) × γ)
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (a : α × β) ↦
    (((η : (a : α × β) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk a ⁻¹' s)

Tactic:
exact Kernel.measurable_kernel_prodMk_left hs

Premises used: 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 α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set ((α × β) × γ)
hs : MeasurableSet s
pos :
  ∀ (a : α),
    (((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
        (Prod.mk a ⁻¹' (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) ⁻¹' s) =
      ∫⁻ (b : β),
        (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (Prod.mk (a, b) ⁻¹' s) ∂(κ : (a : α) → Measure β) a
⊢ ∫⁻ (a : α),
      (((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
        (Prod.mk a ⁻¹' (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) ⁻¹' s) ∂μ =
    ∫⁻ (a : α),
      ∫⁻ (b : β),
        (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (Prod.mk (a, b) ⁻¹' s) ∂(κ : (a : α) → Measure β) a ∂μ

Tactic:
congr with a
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set ((α × β) × γ)
hs : MeasurableSet s
a : α
pos :
  ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹'
          Prod.mk a ⁻¹'
            (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) ⁻¹'
              s) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk (a, b) ⁻¹' s) ∂(κ : (a : α) → Measure β) a
pos₁ :
  MeasurableSet (α := β × γ)
    (Prod.mk a ⁻¹' (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) ⁻¹' s)
⊢ (((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
      (Prod.mk a ⁻¹' (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) ⁻¹' s) =
    ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk (a, b) ⁻¹' s) ∂(κ : (a : α) → Measure β) a

Tactic:
rw [Kernel.compProd_apply]

Premises used: ProbabilityTheory.Kernel.compProd_apply
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set ((α × β) × γ)
hs : MeasurableSet s
a : α
⊢ ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹'
          Prod.mk a ⁻¹'
            (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) ⁻¹'
              s) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk (a, b) ⁻¹' s) ∂(κ : (a : α) → Measure β) a

Tactic:
congr
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set ((α × β) × γ)
hs : MeasurableSet s
a : α
⊢ Measurable (β := (α × β) × γ) fun (x : β × γ) ↦
    (MeasurableEquiv.symm MeasurableEquiv.prodAssoc : (a : α × β × γ) → (α × β) × γ) (a, x)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set ((α × β) × γ)
hs : MeasurableSet s
a : α
⊢ MeasurableSet (α := β × γ)
    (Prod.mk a ⁻¹' (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) ⁻¹' s)

Tactic:
exact hs.preimage (by fun_prop)

Premises used: MeasurableSet.preimage
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
⊢ map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) (μ ⊗ₘ κ ⊗ₘ η) = μ ⊗ₘ (κ ⊗ₖ η)

Tactic:
simp [← Measure.compProd_assoc]

Premises used: MeasureTheory.Measure.compProd_assoc
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst : SFinite ν
hμν : μ ≪ ν
κ : Kernel α β
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 α
inst : SFinite ν
hμν : μ ≪ ν
κ : Kernel α β
hκ : IsSFiniteKernel κ
⊢ SFinite μ

Tactic:
have : SFinite μ := sFinite_of_absolutelyContinuous hμν
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst : SFinite ν
hμν : μ ≪ ν
κ : Kernel α β
hκ : IsSFiniteKernel κ
this : SFinite μ
⊢ μ ⊗ₘ κ ≪ ν ⊗ₘ κ

Tactic:
Measure.AbsolutelyContinuous.mk fun s hs hs_zero ↦ ?_

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst : SFinite ν
hμν : μ ≪ ν
κ : Kernel α β
hκ : IsSFiniteKernel κ
this : SFinite μ
pos :
  ∀ (s : Set (α × β)) (hs : MeasurableSet s)
    (hs_zero : Eq (α := ℝ≥0∞) ((ν ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ ⊗ₘ κ ≪ ν ⊗ₘ κ

Tactic:
refine Measure.AbsolutelyContinuous.mk fun s hs hs_zero ↦ ?_

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst : SFinite ν
hμν : μ ≪ ν
κ : Kernel α β
hκ : IsSFiniteKernel κ
this : SFinite μ
s : Set (α × β)
hs : MeasurableSet s
hs_zero : Eq (α := ℝ≥0∞) ((ν ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
pos :
  ∀
    (hs_zero :
      (ae ν).EventuallyEq (β := ℝ≥0∞)
        (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s)) 0),
    (ae μ).EventuallyEq (β := ℝ≥0∞)
      (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s)) 0
⊢ Eq (α := ℝ≥0∞) ((μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [Measure.compProd_apply hs, lintegral_eq_zero_iff (Kernel.measurable_kernel_prodMk_left hs)]
      at hs_zero ⊢

Premises used: MeasureTheory.lintegral_eq_zero_iff, MeasureTheory.Measure.compProd_apply, ProbabilityTheory.Kernel.measurable_kernel_prodMk_left
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst : SFinite ν
hμν : μ ≪ ν
κ : Kernel α β
hκ : IsSFiniteKernel κ
this : SFinite μ
s : Set (α × β)
hs : MeasurableSet s
hs_zero :
  (ae ν).EventuallyEq (β := ℝ≥0∞)
    (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s)) 0
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞)
    (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s)) 0

Tactic:
hμν.ae_eq hs_zero

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.ae_eq
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst : SFinite ν
hμν : μ ≪ ν
κ : Kernel α β
hκ : IsSFiniteKernel κ
this : SFinite μ
s : Set (α × β)
hs : MeasurableSet s
hs_zero :
  (ae ν).EventuallyEq (β := ℝ≥0∞)
    (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s)) 0
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞)
    (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s)) 0

Tactic:
exact hμν.ae_eq hs_zero

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.ae_eq
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst : SFinite ν
hμν : μ ≪ ν
κ : Kernel α β
hκ : ¬IsSFiniteKernel κ
⊢ μ ⊗ₘ κ ≪ ν ⊗ₘ κ

Tactic:
simp [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 α
κ η : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel η
hκη :
  ∀ᵐ (a : α) ∂μ,
    AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
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 α
κ η : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel η
hκη :
  ∀ᵐ (a : α) ∂μ,
    AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hκ : IsSFiniteKernel κ
⊢ μ ⊗ₘ κ ≪ μ ⊗ₘ η

Tactic:
Measure.AbsolutelyContinuous.mk fun s hs hs_zero ↦ ?_

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel η
hκη :
  ∀ᵐ (a : α) ∂μ,
    AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hκ : IsSFiniteKernel κ
pos :
  ∀ (s : Set (α × β)) (hs : MeasurableSet s)
    (hs_zero : Eq (α := ℝ≥0∞) ((μ ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ ⊗ₘ κ ≪ μ ⊗ₘ η

Tactic:
refine Measure.AbsolutelyContinuous.mk fun s hs hs_zero ↦ ?_

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel η
hκη :
  ∀ᵐ (a : α) ∂μ,
    AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hκ : IsSFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
hs_zero : Eq (α := ℝ≥0∞) ((μ ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
pos :
  ∀
    (hs_zero :
      (ae μ).EventuallyEq (β := ℝ≥0∞)
        (fun (a : α) ↦ (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s)) 0),
    (ae μ).EventuallyEq (β := ℝ≥0∞)
      (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s)) 0
⊢ Eq (α := ℝ≥0∞) ((μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [Measure.compProd_apply hs, lintegral_eq_zero_iff (Kernel.measurable_kernel_prodMk_left hs)]
      at hs_zero ⊢

Premises used: MeasureTheory.lintegral_eq_zero_iff, MeasureTheory.Measure.compProd_apply, 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 α β
inst : SFinite μ
inst_1 : IsSFiniteKernel η
hκη :
  ∀ᵐ (a : α) ∂μ,
    AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hκ : IsSFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
hs_zero :
  (ae μ).EventuallyEq (β := ℝ≥0∞)
    (fun (a : α) ↦ (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s)) 0
a : α
ha_zero :
  Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) : ℝ≥0∞)
    (0 a : ℝ≥0∞)
ha_ac : AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) : ℝ≥0∞)
    (0 a : ℝ≥0∞)

Tactic:
ha_ac ha_zero
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel η
hκη :
  ∀ᵐ (a : α) ∂μ,
    AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hκ : IsSFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
hs_zero :
  (ae μ).EventuallyEq (β := ℝ≥0∞)
    (fun (a : α) ↦ (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s)) 0
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α)
            {x : α |
              (fun (x : α) ↦
                  Eq (α := ℝ≥0∞)
                    ((fun (a : α) ↦
                        ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) : ℝ≥0∞))
                      x)
                    (0 x))
                x}
            x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α)
                  {x : α |
                    (fun (a : α) ↦
                        AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a)
                          ((η : (a : α) → Measure β) a))
                      x}
                  x →
                Membership.mem (γ := Set α)
                  {x : α |
                    (fun (x : α) ↦
                        Eq (α := ℝ≥0∞)
                          ((fun (a : α) ↦
                              ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) :
                                ℝ≥0∞))
                            x)
                          (0 x))
                      x}
                  x}
            x}
      a
h₁ h₂ :
  ∀ (a : α)
    (ha_zero :
      Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) : ℝ≥0∞)
        (0 a : ℝ≥0∞))
    (ha_ac :
      AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)),
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) : ℝ≥0∞)
      (0 a : ℝ≥0∞)
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞)
    (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s)) 0

Tactic:
filter_upwards [hs_zero, hκη] with a ha_zero ha_ac using ha_ac ha_zero
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel η
hκη :
  ∀ᵐ (a : α) ∂μ,
    AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hκ : ¬IsSFiniteKernel κ
⊢ μ ⊗ₘ κ ≪ μ ⊗ₘ η

Tactic:
simp [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 α
κ η : Kernel α β
inst : SFinite ν
inst_1 : IsSFiniteKernel η
hμν : μ ≪ ν
hκη :
  ∀ᵐ (a : α) ∂μ,
    AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
⊢ μ ⊗ₘ κ ≪ ν ⊗ₘ η

Tactic:
have : SFinite μ := sFinite_of_absolutelyContinuous hμν
  (Measure.AbsolutelyContinuous.compProd_right hκη).trans (hμν.compProd_left _)

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.compProd_right, MeasureTheory.Measure.AbsolutelyContinuous.trans, MeasureTheory.Measure.AbsolutelyContinuous.compProd_left, MeasureTheory.sFinite_of_absolutelyContinuous
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero.{u_2} (R := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
⊢ μ ≪ ν

Tactic:
Measure.AbsolutelyContinuous.mk (fun s hs hs0 ↦ ?_)

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero.{u_2} (R := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
refine :
  ∀ (s : Set α) (hs : MeasurableSet s) (hs0 : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ ≪ ν

Tactic:
refine Measure.AbsolutelyContinuous.mk (fun s hs hs0 ↦ ?_)

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero.{u_2} (R := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
pos :
  ∀ (hν : SFinite ν),
    Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) s univ) : ℝ≥0∞) (0 : ℝ≥0∞)
neg :
  ∀ (hν : ¬SFinite ν),
    Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) s univ) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) s univ) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
by_cases hν : SFinite ν

Premises used: MeasureTheory.SFinite
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero.{u_2} (R := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hν : ¬SFinite ν
⊢ Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) s univ) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp [compProd_of_not_sfinite _ _ hν]

Premises used: MeasureTheory.Measure.compProd_of_not_sfinite
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero.{u_2} (R := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hν : SFinite ν
pos :
  ∀ (hη : IsSFiniteKernel η),
    Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) s univ) : ℝ≥0∞) (0 : ℝ≥0∞)
neg :
  ∀ (hη : ¬IsSFiniteKernel η),
    Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) s univ) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) s univ) : ℝ≥0∞) (0 : ℝ≥0∞)

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 α
κ η : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero.{u_2} (R := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hν : SFinite ν
hη : ¬IsSFiniteKernel η
⊢ Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) s univ) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp [compProd_of_not_isSFiniteKernel _ _ hη]

Premises used: MeasureTheory.Measure.compProd_of_not_isSFiniteKernel