awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) s univ) : ℝ≥0∞) (0 : ℝ≥0∞)
have neg : ∀ (hη : ¬IsSFiniteKernel η),
  Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) s univ) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: by_cases hη : IsSFiniteKernel η
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
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∞)
have pos : ∫⁻ (a : α) in s, (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ ∂ν = 0
Tactic: rw [Measure.compProd_apply_prod hs MeasurableSet.univ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (hypothesis)
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∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have h1 : 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
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (hypothesis)
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∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have h2 : Eq (α := ℝ≥0∞) ((μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) s univ) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have h2 : (μ ⊗ₘ κ) (s ×ˢ univ) = 0 := h h1
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have 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∞)
Tactic: rw [Measure.compProd_apply_prod hs MeasurableSet.univ, lintegral_eq_zero_iff] at h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have 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
Tactic: rw [Measure.compProd_apply_prod hs MeasurableSet.univ, lintegral_eq_zero_iff] at h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
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
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have by_contra : ∀ (hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), False
Tactic: by_contra hμs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (hypothesis)
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∞)
⊢ False
have this : (ae (μ.restrict s)).NeBot
Tactic: have : Filter.NeBot (ae (μ.restrict s)) := by simp [hμs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
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
⊢ False
have obtain : ∀ (a : α)
  (ha : Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)), False
Tactic: obtain ⟨a, ha⟩ : ∃ a, κ a univ = 0 := h2.exists
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
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
have refine : ¬Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine absurd ha ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
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 (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
have simp : ¬Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β) (0 : Measure β)
Tactic: simp only [Measure.measure_univ_eq_zero]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SFinite ν
inst_1 : IsSFiniteKernel η
hμν : μ ≪ ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
⊢ μ ⊗ₘ κ ≪ ν ⊗ₘ η
have pos : ∀ (hμ : SFinite μ), μ ⊗ₘ κ ≪ ν ⊗ₘ η
Tactic: by_cases hμ : SFinite μ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SFinite ν
inst_1 : IsSFiniteKernel η
hμν : μ ≪ ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
pos : ∀ (hμ : SFinite μ), μ ⊗ₘ κ ≪ ν ⊗ₘ η
⊢ μ ⊗ₘ κ ≪ ν ⊗ₘ η
have neg : ∀ (hμ : ¬SFinite μ), μ ⊗ₘ κ ≪ ν ⊗ₘ η
Tactic: by_cases hμ : SFinite μ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SFinite ν
inst_1 : IsSFiniteKernel η
hμν : μ ≪ ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hμ : ¬SFinite μ
⊢ μ ⊗ₘ κ ≪ ν ⊗ₘ η
have neg : 0 ≪ ν ⊗ₘ η
Tactic: rw [compProd_of_not_sfinite _ _ hμ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SFinite ν
inst_1 : IsSFiniteKernel η
hμν : μ ≪ ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hμ : SFinite μ
⊢ μ ⊗ₘ κ ≪ ν ⊗ₘ η
have 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 ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have pos : Eq (α := ℝ≥0∞) ((μ ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: suffices (μ ⊗ₘ η) s = 0 from hκη this
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have pos : ∀ (hs_zero : ∀ᵐ (a : α) ∂ν, ∀ᵐ (b : β) ∂((η : (a : α) → Measure β) a : Measure β), (a, b) ∉ s),
  ∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂((η : (a : α) → Measure β) a : Measure β), (a, b) ∉ s
Tactic: rw [measure_eq_zero_iff_ae_notMem, ae_compProd_iff hs.compl] at hs_zero ⊢
Cleared hypotheses: hs_zero
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
have pos : ∀ (hμ : SFinite μ), μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
Tactic: by_cases hμ : SFinite μ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
pos : ∀ (hμ : SFinite μ), μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
have neg : ∀ (hμ : ¬SFinite μ), μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
Tactic: by_cases hμ : SFinite μ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : ¬SFinite μ
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
have neg : 0 ⟂ₘ ν ⊗ₘ η
Tactic: rw [compProd_of_not_sfinite _ _ hμ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
have pos : ∀ (hν : SFinite ν), μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
Tactic: by_cases hν : SFinite ν
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
pos : ∀ (hν : SFinite ν), μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
have neg : ∀ (hν : ¬SFinite ν), μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
Tactic: by_cases hν : SFinite ν
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : ¬SFinite ν
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
have neg : μ ⊗ₘ κ ⟂ₘ 0
Tactic: rw [compProd_of_not_sfinite _ _ hν]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : SFinite ν
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
have pos : ∀ (hκ : IsSFiniteKernel κ), μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
Tactic: by_cases hκ : IsSFiniteKernel κ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : SFinite ν
pos : ∀ (hκ : IsSFiniteKernel κ), μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
have neg : ∀ (hκ : ¬IsSFiniteKernel κ), μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
Tactic: by_cases hκ : IsSFiniteKernel κ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : SFinite ν
hκ : ¬IsSFiniteKernel κ
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
have neg : 0 ⟂ₘ ν ⊗ₘ η
Tactic: rw [compProd_of_not_isSFiniteKernel _ _ hκ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : SFinite ν
hκ : IsSFiniteKernel κ
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
have pos : ∀ (hη : IsSFiniteKernel η), μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
Tactic: by_cases hη : IsSFiniteKernel η
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : SFinite ν
hκ : IsSFiniteKernel κ
pos : ∀ (hη : IsSFiniteKernel η), μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
have neg : ∀ (hη : ¬IsSFiniteKernel η), μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
Tactic: by_cases hη : IsSFiniteKernel η
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : SFinite ν
hκ : IsSFiniteKernel κ
hη : ¬IsSFiniteKernel η
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
have neg : μ ⊗ₘ κ ⟂ₘ 0
Tactic: rw [compProd_of_not_isSFiniteKernel _ _ hη]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : SFinite ν
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
have 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, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : SFinite ν
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
⊢ 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∞)
have 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∞)
Tactic: rw [compProd_apply_prod hμν.measurableSet_nullSet .univ, compl_prod_eq_union]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
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 ∧
    Eq (α := ℝ≥0∞)
      ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞)
          (SProd.sprod (β := Set β) hμν.nullSetᶜ univ ∪ SProd.sprod (α := Set α) (β := Set β) univ univᶜ) :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
have pos : Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) hμν.nullSetᶜ univ) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp only [MutuallySingular.restrict_nullSet, lintegral_zero_measure, compl_univ,
    prod_empty, union_empty, true_and]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : SFinite ν
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
⊢ Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) hμν.nullSetᶜ univ) : ℝ≥0∞) (0 : ℝ≥0∞)
have pos : ∫⁻ (a : α) in hμν.nullSetᶜ, (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ ∂ν = 0
Tactic: rw [compProd_apply_prod hμν.measurableSet_nullSet.compl .univ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (hypothesis)
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ν : ξ ≪ ν
⊢ ∀ᵐ (x : α) ∂ξ, @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) x) ((η : (a : α) → Measure β) x)
have hs : MeasurableSet h.nullSet
Tactic: have hs : MeasurableSet h.nullSet := h.measurableSet_nullSet
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (hypothesis)
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
⊢ ∀ᵐ (x : α) ∂ξ, @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) x) ((η : (a : α) → Measure β) x)
have hμ_zero : Eq (α := ℝ≥0∞) ((μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) h.nullSet : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have hμ_zero : (μ ⊗ₘ κ) h.nullSet = 0 := h.measure_nullSet
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (hypothesis)
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∞)
⊢ ∀ᵐ (x : α) ∂ξ, @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) x) ((η : (a : α) → Measure β) x)
have hν_zero : Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) h.nullSetᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have hν_zero : (ν ⊗ₘ η) h.nullSetᶜ = 0 := h.measure_compl_nullSet