-- Mathlib/Probability/Kernel/Composition/CompProd.lean
theorem ae_null_of_compProd_null (h : (κ ⊗ₖ η) a s = 0) :
    (fun b => η (a, b) (Prod.mk b ⁻¹' s)) =ᵐ[κ a] 0

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
h : ((κ ⊗ₖ η) a) s = 0
⊢ (fun b => (η (a, b)) (Prod.mk b ⁻¹' s)) =ᶠ[ae (κ a)] 0

Tactic:
obtain ⟨t, hst, mt, ht⟩ := exists_measurable_superset_of_null h

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
h : ((κ ⊗ₖ η) a) s = 0
t : Set (β × γ)
hst : s ⊆ t
mt : MeasurableSet t
ht : ((κ ⊗ₖ η) a) t = 0
⊢ (fun b => (η (a, b)) (Prod.mk b ⁻¹' s)) =ᶠ[ae (κ a)] 0

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
h : ((κ ⊗ₖ η) a) s = 0
t : Set (β × γ)
hst : s ⊆ t
mt : MeasurableSet t
ht : ((κ ⊗ₖ η) a) t = 0
⊢ (fun b => (η (a, b)) (Prod.mk b ⁻¹' s)) =ᶠ[ae (κ a)] 0

Tactic:
simp_rw [compProd_null a mt] at ht

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
h : ((κ ⊗ₖ η) a) s = 0
t : Set (β × γ)
hst : s ⊆ t
mt : MeasurableSet t
ht : (fun b => (η (a, b)) (Prod.mk b ⁻¹' t)) =ᶠ[ae (κ a)] 0
⊢ (fun b => (η (a, b)) (Prod.mk b ⁻¹' s)) =ᶠ[ae (κ a)] 0

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
h : ((κ ⊗ₖ η) a) s = 0
t : Set (β × γ)
hst : s ⊆ t
mt : MeasurableSet t
ht : (fun b => (η (a, b)) (Prod.mk b ⁻¹' t)) =ᶠ[ae (κ a)] 0
⊢ (fun b => (η (a, b)) (Prod.mk b ⁻¹' s)) ≤ᶠ[ae (κ a)] 0 ∧ 0 ≤ᶠ[ae (κ a)] fun b => (η (a, b)) (Prod.mk b ⁻¹' s)

Tactic:
exact
  ⟨Filter.EventuallyLE.trans_eq
      (Filter.Eventually.of_forall fun x => measure_mono (Set.preimage_mono hst)) ht,
    Filter.Eventually.of_forall fun x => zero_le _⟩

Result:
no goals

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
h : ((κ ⊗ₖ η) a) s = 0
t : Set (β × γ)
hst : s ⊆ t
mt : MeasurableSet t
ht : (fun b => (η (a, b)) (Prod.mk b ⁻¹' t)) =ᶠ[ae (κ a)] 0
⊢ (fun b => (η (a, b)) (Prod.mk b ⁻¹' s)) =ᶠ[ae (κ a)] 0

Tactic:
rw [Filter.eventuallyLE_antisymm_iff]

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
h : ((κ ⊗ₖ η) a) s = 0
t : Set (β × γ)
hst : s ⊆ t
mt : MeasurableSet t
ht : (fun b => (η (a, b)) (Prod.mk b ⁻¹' t)) =ᶠ[ae (κ a)] 0
⊢ (fun b => (η (a, b)) (Prod.mk b ⁻¹' s)) ≤ᶠ[ae (κ a)] 0 ∧ 0 ≤ᶠ[ae (κ a)] fun b => (η (a, b)) (Prod.mk b ⁻¹' s)