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 : 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 η
pos : ∫⁻ (a : α) in s, (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ ∂ν = 0
⊢ Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) s univ) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [Measure.compProd_apply_prod hs MeasurableSet.univ]

Premises used: 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 α
κ η : 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 η
⊢ ∫⁻ (a : α) in s, (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ ∂ν = 0

Tactic:
setLIntegral_measure_zero _ _ hs0

Premises used: MeasureTheory.setLIntegral_measure_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_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 η
⊢ ∫⁻ (a : α) in s, (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ ∂ν = 0

Tactic:
exact setLIntegral_measure_zero _ _ hs0

Premises used: MeasureTheory.setLIntegral_measure_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_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∞)
⊢ Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) s univ) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
have h1 : (ν ⊗ₘ η) (s ×ˢ univ) = 0 := by
    by_cases hν : SFinite ν
    swap; · simp [compProd_of_not_sfinite _ _ hν]
    by_cases hη : IsSFiniteKernel η
    swap; · simp [compProd_of_not_isSFiniteKernel _ _ hη]
    rw [Measure.compProd_apply_prod hs MeasurableSet.univ]
    exact setLIntegral_measure_zero _ _ hs0
-- 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∞)
h1 : 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:
have h2 : (μ ⊗ₘ κ) (s ×ˢ univ) = 0 := h h1
-- 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∞)
h1 : Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) s univ) : ℝ≥0∞) (0 : ℝ≥0∞)
h2 : Eq (α := ℝ≥0∞) ((μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) s univ) : ℝ≥0∞) (0 : ℝ≥0∞)
rw :
  ∀
    (h2 :
      (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞)
        (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ) 0),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rw₁ :
  ∀ (h2 : ∫⁻ (a : α) in s, (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ ∂μ = 0),
    Measurable (β := ℝ≥0∞) fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [Measure.compProd_apply_prod hs MeasurableSet.univ, lintegral_eq_zero_iff] at h2

Premises used: MeasureTheory.lintegral_eq_zero_iff, 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 α
κ η : 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∞)
h1 : Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) s univ) : ℝ≥0∞) (0 : ℝ≥0∞)
h2 : ∫⁻ (a : α) in s, (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ ∂μ = 0
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ

Tactic:
Kernel.measurable_coe _ MeasurableSet.univ

Premises used: ProbabilityTheory.Kernel.measurable_coe, MeasurableSet.univ
-- 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∞)
h1 : Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) s univ) : ℝ≥0∞) (0 : ℝ≥0∞)
h2 : ∫⁻ (a : α) in s, (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ ∂μ = 0
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ

Tactic:
exact Kernel.measurable_coe _ MeasurableSet.univ

Premises used: ProbabilityTheory.Kernel.measurable_coe, MeasurableSet.univ
-- 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∞)
h1 : Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) s univ) : ℝ≥0∞) (0 : ℝ≥0∞)
h2 :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞)
    (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ) 0
by_contra : ∀ (hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), False
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
by_contra hμs
-- 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∞)
h1 : Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) s univ) : ℝ≥0∞) (0 : ℝ≥0∞)
h2 :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞)
    (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ) 0
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (ae (μ.restrict s)).NeBot

Tactic:
simp [hμs]
-- 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∞)
h1 : Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) s univ) : ℝ≥0∞) (0 : ℝ≥0∞)
h2 :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞)
    (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ) 0
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (ae (μ.restrict s)).NeBot

Tactic:
have : Filter.NeBot (ae (μ.restrict s)) := by simp [hμs]
-- 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∞)
h1 : Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) s univ) : ℝ≥0∞) (0 : ℝ≥0∞)
h2 :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞)
    (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ) 0
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
this : (ae (μ.restrict s)).NeBot
⊢ ∃ (a : α), Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
h2.exists

Premises used: Filter.Eventually.exists
-- 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∞)
h1 : Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) s univ) : ℝ≥0∞) (0 : ℝ≥0∞)
h2 :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞)
    (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ) 0
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
this : (ae (μ.restrict s)).NeBot
obtain :
  ∀ (a : α)
    (ha : Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)),
    False
⊢ False

Tactic:
obtain ⟨a, ha⟩ : ∃ a, κ a univ = 0 := h2.exists

Premises used: Filter.Eventually.exists
-- 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∞)
h1 : Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) s univ) : ℝ≥0∞) (0 : ℝ≥0∞)
h2 :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞)
    (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ) 0
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
this : (ae (μ.restrict s)).NeBot
a : α
ha : Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ False

Tactic:
absurd ha ?_

Premises used: absurd
-- 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∞)
h1 : Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) s univ) : ℝ≥0∞) (0 : ℝ≥0∞)
h2 :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞)
    (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ) 0
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
this : (ae (μ.restrict s)).NeBot
a : α
ha : Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
refine : ¬Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ False

Tactic:
refine absurd ha ?_

Premises used: absurd
-- 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∞)
h1 : Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) s univ) : ℝ≥0∞) (0 : ℝ≥0∞)
h2 :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞)
    (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ) 0
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
this : (ae (μ.restrict s)).NeBot
a : α
ha : Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
simp : ¬Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β) (0 : Measure β)
⊢ ¬Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp only [Measure.measure_univ_eq_zero]

Premises used: MeasureTheory.Measure.measure_univ_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 : 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∞)
h1 : Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) s univ) : ℝ≥0∞) (0 : ℝ≥0∞)
h2 :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞)
    (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ) 0
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
this : (ae (μ.restrict s)).NeBot
a : α
ha : Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ¬Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β) (0 : Measure β)

Tactic:
(h_zero a).out

Premises used: NeZero.out
-- 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∞)
h1 : Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) s univ) : ℝ≥0∞) (0 : ℝ≥0∞)
h2 :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞)
    (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ) 0
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
this : (ae (μ.restrict s)).NeBot
a : α
ha : Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ¬Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β) (0 : Measure β)

Tactic:
exact (h_zero a).out

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

Tactic:
⟨absolutelyContinuous_of_compProd, fun h ↦ h.compProd_left κ⟩

Premises used: MeasureTheory.Measure.absolutelyContinuous_of_compProd, Iff.intro, 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 : SFinite ν
inst_1 : IsSFiniteKernel η
hμν : μ ≪ ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
pos : ∀ (hμ : SFinite μ), μ ⊗ₘ κ ≪ ν ⊗ₘ η
neg : ∀ (hμ : ¬SFinite μ), μ ⊗ₘ κ ≪ ν ⊗ₘ η
⊢ μ ⊗ₘ κ ≪ ν ⊗ₘ η

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μν : μ ≪ ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hμ : ¬SFinite μ
neg : 0 ≪ ν ⊗ₘ η
⊢ μ ⊗ₘ κ ≪ ν ⊗ₘ η

Tactic:
rw [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μν : μ ≪ ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hμ : ¬SFinite μ
⊢ 0 ≪ ν ⊗ₘ η

Tactic:
simp
-- 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κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hμ : SFinite μ
⊢ μ ⊗ₘ κ ≪ ν ⊗ₘ η

Tactic:
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μν : μ ≪ ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hμ : 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 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μν : μ ≪ ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hμ : SFinite μ
s : Set (α × β)
hs : MeasurableSet s
hs_zero : Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
pos : Eq (α := ℝ≥0∞) ((μ ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
suffices (μ ⊗ₘ η) s = 0 from hκη this
-- 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κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hμ : SFinite μ
s : Set (α × β)
hs : MeasurableSet s
hs_zero : Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
pos :
  ∀ (hs_zero : ∀ᵐ (a : α) ∂ν, ∀ᵐ (b : β) ∂((η : (a : α) → Measure β) a : Measure β), (a, b) ∉ s),
    ∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂((η : (a : α) → Measure β) a : Measure β), (a, b) ∉ s
⊢ Eq (α := ℝ≥0∞) ((μ ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [measure_eq_zero_iff_ae_notMem, ae_compProd_iff hs.compl] at hs_zero ⊢

Premises used: MeasurableSet.compl, MeasureTheory.measure_eq_zero_iff_ae_notMem, MeasureTheory.Measure.ae_compProd_iff
-- 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κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hμ : SFinite μ
s : Set (α × β)
hs : MeasurableSet s
hs_zero : ∀ᵐ (a : α) ∂ν, ∀ᵐ (b : β) ∂((η : (a : α) → Measure β) a : Measure β), (a, b) ∉ s
⊢ ∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂((η : (a : α) → Measure β) a : Measure β), (a, b) ∉ s

Tactic:
hμν.ae_le hs_zero

Premises used: Filter.Eventually, MeasureTheory.Measure.AbsolutelyContinuous.ae_le
-- 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κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hμ : SFinite μ
s : Set (α × β)
hs : MeasurableSet s
hs_zero : ∀ᵐ (a : α) ∂ν, ∀ᵐ (b : β) ∂((η : (a : α) → Measure β) a : Measure β), (a, b) ∉ s
⊢ ∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂((η : (a : α) → Measure β) a : Measure β), (a, b) ∉ s

Tactic:
exact hμν.ae_le hs_zero

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

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 α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : ¬SFinite μ
neg : 0 ⟂ₘ ν ⊗ₘ η
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η

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

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 α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : ¬SFinite ν
neg : μ ⊗ₘ κ ⟂ₘ 0
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η

Tactic:
rw [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 α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : ¬SFinite ν
⊢ μ ⊗ₘ κ ⟂ₘ 0

Tactic:
simp