-- Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean
lemma AbsolutelyContinuous.compProd_of_compProd [SFinite ν] [IsSFiniteKernel η]
    (hμν : μ ≪ ν) (hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η) :
    μ ⊗ₘ κ ≪ ν ⊗ₘ η

Proof state:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite ν
inst✝ : IsSFiniteKernel η
hμν : μ ≪ ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hμ : ¬SFinite μ
⊢ μ ⊗ₘ κ ≪ ν ⊗ₘ η

Tactic:
rw [compProd_of_not_sfinite _ _ hμ]

Result:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite ν
inst✝ : IsSFiniteKernel η
hμν : μ ≪ ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hμ : ¬SFinite μ
⊢ 0 ≪ ν ⊗ₘ η

Proof state:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite ν
inst✝ : IsSFiniteKernel η
hμν : μ ≪ ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hμ : SFinite μ
s : Set (α × β)
hs : MeasurableSet s
hs_zero : ∀ᵐ (a : α) ∂ν, ∀ᵐ (b : β) ∂η a, (a, b) ∉ s
⊢ ∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂η a, (a, b) ∉ s

Tactic:
exact hμν.ae_le hs_zero

Result:
no goals

Proof state:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite ν
inst✝ : IsSFiniteKernel η
hμν : μ ≪ ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hμ : SFinite μ
⊢ μ ⊗ₘ κ ≪ ν ⊗ₘ η

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

Result:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite ν
inst✝ : IsSFiniteKernel η
hμν : μ ≪ ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hμ : SFinite μ
s : Set (α × β)
hs : MeasurableSet s
hs_zero : (ν ⊗ₘ η) s = 0
⊢ (μ ⊗ₘ κ) s = 0

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

Tactic:
suffices (μ ⊗ₘ η) s = 0 from hκη this

Result:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite ν
inst✝ : IsSFiniteKernel η
hμν : μ ≪ ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hμ : SFinite μ
s : Set (α × β)
hs : MeasurableSet s
hs_zero : (ν ⊗ₘ η) s = 0
⊢ (μ ⊗ₘ η) s = 0

Proof state:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite ν
inst✝ : IsSFiniteKernel η
hμν : μ ≪ ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hμ : SFinite μ
⊢ μ ⊗ₘ κ ≪ ν ⊗ₘ η

case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite ν
inst✝ : IsSFiniteKernel η
hμν : μ ≪ ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hμ : ¬SFinite μ
⊢ μ ⊗ₘ κ ≪ ν ⊗ₘ η

Tactic:
swap

Result:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite ν
inst✝ : IsSFiniteKernel η
hμν : μ ≪ ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hμ : ¬SFinite μ
⊢ μ ⊗ₘ κ ≪ ν ⊗ₘ η

case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite ν
inst✝ : IsSFiniteKernel η
hμν : μ ≪ ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hμ : SFinite μ
⊢ μ ⊗ₘ κ ≪ ν ⊗ₘ η

Proof state:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite ν
inst✝ : IsSFiniteKernel η
hμν : μ ≪ ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hμ : ¬SFinite μ
⊢ 0 ≪ ν ⊗ₘ η

Tactic:
simp

Result:
no goals

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

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

Result:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite ν
inst✝ : IsSFiniteKernel η
hμν : μ ≪ ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hμ : SFinite μ
s : Set (α × β)
hs : MeasurableSet s
hs_zero : ∀ᵐ (a : α) ∂ν, ∀ᵐ (b : β) ∂η a, (a, b) ∉ s
⊢ ∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂η a, (a, b) ∉ s

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite ν
inst✝ : IsSFiniteKernel η
hμν : μ ≪ ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
⊢ μ ⊗ₘ κ ≪ ν ⊗ₘ η

Tactic:
by_cases hμ : SFinite μ

Result:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite ν
inst✝ : IsSFiniteKernel η
hμν : μ ≪ ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hμ : SFinite μ
⊢ μ ⊗ₘ κ ≪ ν ⊗ₘ η

case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite ν
inst✝ : IsSFiniteKernel η
hμν : μ ≪ ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hμ : ¬SFinite μ
⊢ μ ⊗ₘ κ ≪ ν ⊗ₘ η