awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
inst : SFinite μ
rw :
  Eq (α := Measure (Unit × β)) (map (Prod.mk ()) ((Kernel.const Unit μ : (a : Unit) → Measure β) ()))
    (map (Prod.mk ()) μ)
⊢ Eq (α := Measure (Unit × β)) (dirac () ⊗ₘ Kernel.const Unit μ) (map (Prod.mk ()) μ)
have rw₁ : Eq (α := Measure (Unit × β)) (map (Prod.mk ()) μ) (map (Prod.mk ()) μ)
Tactic: rw [dirac_unit_compProd, Kernel.const_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
⊢ map (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) (μ ⊗ₘ (κ ⊗ₖ η)) = μ ⊗ₘ κ ⊗ₘ η
have pos : ∀ (hμ : SFinite μ),
  map (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) (μ ⊗ₘ (κ ⊗ₖ η)) = μ ⊗ₘ κ ⊗ₘ η
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 α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
pos :
  ∀ (hμ : SFinite μ),
    map (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) (μ ⊗ₘ (κ ⊗ₖ η)) =
      μ ⊗ₘ κ ⊗ₘ η
⊢ map (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) (μ ⊗ₘ (κ ⊗ₖ η)) = μ ⊗ₘ κ ⊗ₘ η
have neg : ∀ (hμ : ¬SFinite μ),
  map (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) (μ ⊗ₘ (κ ⊗ₖ η)) = μ ⊗ₘ κ ⊗ₘ η
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 α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
⊢ map (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) (μ ⊗ₘ (κ ⊗ₖ η)) = μ ⊗ₘ κ ⊗ₘ η
have pos : ∀ (hκ : IsSFiniteKernel κ),
  map (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) (μ ⊗ₘ (κ ⊗ₖ η)) = μ ⊗ₘ κ ⊗ₘ η
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 α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
pos :
  ∀ (hκ : IsSFiniteKernel κ),
    map (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) (μ ⊗ₘ (κ ⊗ₖ η)) =
      μ ⊗ₘ κ ⊗ₘ η
⊢ map (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) (μ ⊗ₘ (κ ⊗ₖ η)) = μ ⊗ₘ κ ⊗ₘ η
have neg : ∀ (hκ : ¬IsSFiniteKernel κ),
  map (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) (μ ⊗ₘ (κ ⊗ₖ η)) = μ ⊗ₘ κ ⊗ₘ η
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 α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
⊢ map (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) (μ ⊗ₘ (κ ⊗ₖ η)) = μ ⊗ₘ κ ⊗ₘ η
have pos : ∀ (hη : IsSFiniteKernel η),
  map (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) (μ ⊗ₘ (κ ⊗ₖ η)) = μ ⊗ₘ κ ⊗ₘ η
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 α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
pos :
  ∀ (hη : IsSFiniteKernel η),
    map (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) (μ ⊗ₘ (κ ⊗ₖ η)) =
      μ ⊗ₘ κ ⊗ₘ η
⊢ map (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) (μ ⊗ₘ (κ ⊗ₖ η)) = μ ⊗ₘ κ ⊗ₘ η
have neg : ∀ (hη : ¬IsSFiniteKernel η),
  map (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) (μ ⊗ₘ (κ ⊗ₖ η)) = μ ⊗ₘ κ ⊗ₘ η
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 α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
⊢ map (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) (μ ⊗ₘ (κ ⊗ₖ η)) = μ ⊗ₘ κ ⊗ₘ η
have pos : ∀ (s : Set ((α × β) × γ)) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞)
    ((map (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) (μ ⊗ₘ (κ ⊗ₖ η)) :
          (a : Set ((α × β) × γ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((μ ⊗ₘ κ ⊗ₘ η : (a : Set ((α × β) × γ)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
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
⊢ Eq (α := ℝ≥0∞)
    ((map (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) (μ ⊗ₘ (κ ⊗ₖ η)) :
          (a : Set ((α × β) × γ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((μ ⊗ₘ κ ⊗ₘ η : (a : Set ((α × β) × γ)) → ℝ≥0∞) s : ℝ≥0∞)
have 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 ∂μ
Tactic: rw [Measure.compProd_apply hs, Measure.map_apply (by fun_prop) hs,
    Measure.compProd_apply (hs.preimage (by fun_prop)), Measure.lintegral_compProd]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
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 ∂μ
⊢ Eq (α := ℝ≥0∞)
    ((map (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) (μ ⊗ₘ (κ ⊗ₖ η)) :
          (a : Set ((α × β) × γ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((μ ⊗ₘ κ ⊗ₘ η : (a : Set ((α × β) × γ)) → ℝ≥0∞) s : ℝ≥0∞)
have pos₁ : Measurable (β := ℝ≥0∞) fun (a : α × β) ↦
  (((η : (a : α × β) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk a ⁻¹' s)
Tactic: rw [Measure.compProd_apply hs, Measure.map_apply (by fun_prop) hs,
    Measure.compProd_apply (hs.preimage (by fun_prop)), Measure.lintegral_compProd]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
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 : α),
      (((κ ⊗ₖ η : (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 ∂μ
have 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
Tactic: congr with a
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
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 : α
⊢ (((κ ⊗ₖ η : (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
have 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
Tactic: rw [Kernel.compProd_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
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
⊢ (((κ ⊗ₖ η : (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
have pos₁ : MeasurableSet (α := β × γ)
  (Prod.mk a ⁻¹' (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) ⁻¹' s)
Tactic: rw [Kernel.compProd_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst : SFinite ν
hμν : μ ≪ ν
κ : Kernel α β
⊢ μ ⊗ₘ κ ≪ ν ⊗ₘ κ
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 α
inst : SFinite ν
hμν : μ ≪ ν
κ : Kernel α β
pos : ∀ (hκ : IsSFiniteKernel κ), μ ⊗ₘ κ ≪ ν ⊗ₘ κ
⊢ μ ⊗ₘ κ ≪ ν ⊗ₘ κ
have neg : ∀ (hκ : ¬IsSFiniteKernel κ), μ ⊗ₘ κ ≪ ν ⊗ₘ κ
Tactic: by_cases hκ : IsSFiniteKernel κ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst : SFinite ν
hμν : μ ≪ ν
κ : Kernel α β
hκ : IsSFiniteKernel κ
⊢ μ ⊗ₘ κ ≪ ν ⊗ₘ κ
have this : SFinite μ
Tactic: have : SFinite μ := sFinite_of_absolutelyContinuous hμν
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst : SFinite ν
hμν : μ ≪ ν
κ : Kernel α β
hκ : IsSFiniteKernel κ
this : 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 Measure.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 α
inst : SFinite ν
hμν : μ ≪ ν
κ : Kernel α β
hκ : IsSFiniteKernel κ
this : 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 :
    (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: rw [Measure.compProd_apply hs, lintegral_eq_zero_iff (Kernel.measurable_kernel_prodMk_left hs)]
      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 α
κ η : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel η
hκη :
  ∀ᵐ (a : α) ∂μ,
    AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
⊢ μ ⊗ₘ κ ≪ μ ⊗ₘ η
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 α
κ η : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel η
hκη :
  ∀ᵐ (a : α) ∂μ,
    AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
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 α
κ η : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel η
hκη :
  ∀ᵐ (a : α) ∂μ,
    AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hκ : IsSFiniteKernel κ
⊢ μ ⊗ₘ κ ≪ μ ⊗ₘ η
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 Measure.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κη :
  ∀ᵐ (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∞)
⊢ Eq (α := ℝ≥0∞) ((μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have 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
Tactic: rw [Measure.compProd_apply hs, lintegral_eq_zero_iff (Kernel.measurable_kernel_prodMk_left hs)]
      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 α
κ η : 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
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞)
    (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s)) 0
have 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
Tactic: filter_upwards [hs_zero, hκη] with a ha_zero ha_ac using ha_ac ha_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κη :
  ∀ᵐ (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
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞)
    (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s)) 0
have h₁ : ∀ (a : α),
  Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) : ℝ≥0∞)
      (0 a : ℝ≥0∞) →
    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: filter_upwards [hs_zero, hκη] with a ha_zero ha_ac using ha_ac ha_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_zero : ∀ (a : α), NeZero.{u_2} (R := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
⊢ μ ≪ ν
have 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 ↦ ?_)
-- 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∞)
⊢ Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) s univ) : ℝ≥0∞) (0 : ℝ≥0∞)
have pos : ∀ (hν : SFinite ν),
  Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) s univ) : ℝ≥0∞) (0 : ℝ≥0∞)
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_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∞)
⊢ Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) s univ) : ℝ≥0∞) (0 : ℝ≥0∞)
have neg : ∀ (hν : ¬SFinite ν),
  Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) s univ) : ℝ≥0∞) (0 : ℝ≥0∞)
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_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∞)
have pos : ∀ (hη : IsSFiniteKernel η),
  Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) s univ) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: by_cases hη : IsSFiniteKernel η