-- Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean
lemma absolutelyContinuous_of_compProd [SFinite μ] [IsSFiniteKernel κ] [h_zero : ∀ a, NeZero (κ a)]
    (h : μ ⊗ₘ κ ≪ ν ⊗ₘ η) :
    μ ≪ ν

Proof state:
case intro
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero (κ a)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : ν s = 0
h1 : (ν ⊗ₘ η) (s ×ˢ univ) = 0
h2 : (fun a => (κ a) univ) =ᶠ[ae (μ.restrict s)] 0
hμs : ¬μ s = 0
this : (ae (μ.restrict s)).NeBot
a : α
ha : (κ a) univ = 0
⊢ False

Tactic:
refine absurd ha ?_

Result:
case intro
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero (κ a)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : ν s = 0
h1 : (ν ⊗ₘ η) (s ×ˢ univ) = 0
h2 : (fun a => (κ a) univ) =ᶠ[ae (μ.restrict s)] 0
hμs : ¬μ s = 0
this : (ae (μ.restrict s)).NeBot
a : α
ha : (κ a) univ = 0
⊢ ¬(κ a) univ = 0

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero (κ a)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : ν s = 0
h1 : (ν ⊗ₘ η) (s ×ˢ univ) = 0
h2 : ∫⁻ (a : α) in s, (κ a) univ ∂μ = 0
⊢ Measurable fun a => (κ a) univ

Tactic:
exact Kernel.measurable_coe _ MeasurableSet.univ

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero (κ a)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : ν s = 0
h1 : (ν ⊗ₘ η) (s ×ˢ univ) = 0
h2 : (fun a => (κ a) univ) =ᶠ[ae (μ.restrict s)] 0
⊢ μ s = 0

α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero (κ a)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : ν s = 0
h1 : (ν ⊗ₘ η) (s ×ˢ univ) = 0
h2 : ∫⁻ (a : α) in s, (κ a) univ ∂μ = 0
⊢ Measurable fun a => (κ a) univ

Tactic:
swap

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero (κ a)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : ν s = 0
h1 : (ν ⊗ₘ η) (s ×ˢ univ) = 0
h2 : ∫⁻ (a : α) in s, (κ a) univ ∂μ = 0
⊢ Measurable fun a => (κ a) univ

α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero (κ a)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : ν s = 0
h1 : (ν ⊗ₘ η) (s ×ˢ univ) = 0
h2 : (fun a => (κ a) univ) =ᶠ[ae (μ.restrict s)] 0
⊢ μ s = 0

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero (κ a)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : ν s = 0
h1 : (ν ⊗ₘ η) (s ×ˢ univ) = 0
⊢ μ s = 0

Tactic:
have h2 : (μ ⊗ₘ κ) (s ×ˢ univ) = 0 := h h1

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero (κ a)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : ν s = 0
h1 : (ν ⊗ₘ η) (s ×ˢ univ) = 0
h2 : (μ ⊗ₘ κ) (s ×ˢ univ) = 0
⊢ μ s = 0

Proof state:
case intro
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero (κ a)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : ν s = 0
h1 : (ν ⊗ₘ η) (s ×ˢ univ) = 0
h2 : (fun a => (κ a) univ) =ᶠ[ae (μ.restrict s)] 0
hμs : ¬μ s = 0
this : (ae (μ.restrict s)).NeBot
a : α
ha : (κ a) univ = 0
⊢ ¬κ a = 0

Tactic:
exact (h_zero a).out

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero (κ a)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
⊢ μ ≪ ν

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

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero (κ a)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : ν s = 0
⊢ μ s = 0

Proof state:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero (κ a)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : ν s = 0
hν : SFinite ν
hη : ¬IsSFiniteKernel η
⊢ (ν ⊗ₘ η) (s ×ˢ univ) = 0

Tactic:
simp [compProd_of_not_isSFiniteKernel _ _ hη]

Result:
no goals

Proof state:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero (κ a)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : ν s = 0
hν : SFinite ν
hη : IsSFiniteKernel η
⊢ ∫⁻ (a : α) in s, (η a) univ ∂ν = 0

Tactic:
exact setLIntegral_measure_zero _ _ hs0

Result:
no goals

Proof state:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero (κ a)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : ν s = 0
hν : SFinite ν
hη : IsSFiniteKernel η
⊢ (ν ⊗ₘ η) (s ×ˢ univ) = 0

case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero (κ a)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : ν s = 0
hν : SFinite ν
hη : ¬IsSFiniteKernel η
⊢ (ν ⊗ₘ η) (s ×ˢ univ) = 0

Tactic:
swap

Result:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero (κ a)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : ν s = 0
hν : SFinite ν
hη : ¬IsSFiniteKernel η
⊢ (ν ⊗ₘ η) (s ×ˢ univ) = 0

case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero (κ a)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : ν s = 0
hν : SFinite ν
hη : IsSFiniteKernel η
⊢ (ν ⊗ₘ η) (s ×ˢ univ) = 0

Proof state:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero (κ a)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : ν s = 0
hν : SFinite ν
hη : IsSFiniteKernel η
⊢ (ν ⊗ₘ η) (s ×ˢ univ) = 0

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

Result:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero (κ a)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : ν s = 0
hν : SFinite ν
hη : IsSFiniteKernel η
⊢ ∫⁻ (a : α) in s, (η a) univ ∂ν = 0