-- Mathlib/Probability/Kernel/Composition/CompProd.lean
lemma compProd_eq_zero_iff {κ : Kernel α β} {η : Kernel (α × β) γ}
    [IsSFiniteKernel κ] [IsSFiniteKernel η] :
    κ ⊗ₖ η = 0 ↔ ∀ a, ∀ᵐ b ∂(κ a), η (a, b) = 0

Proof state:
case refine_1.refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : κ ⊗ₖ η = 0
a : α
⊢ ∫⁻ (a_1 : β), (η (a, a_1)) Set.univ ∂κ a = 0

Tactic:
rw [← setLIntegral_univ, ← Kernel.compProd_apply_prod .univ .univ, h]

Result:
case refine_1.refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : κ ⊗ₖ η = 0
a : α
⊢ (0 a) (Set.univ ×ˢ Set.univ) = 0

Proof state:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : ∀ (a : α), ∀ᵐ (b : β) ∂κ a, η (a, b) = 0
⊢ κ ⊗ₖ η = κ ⊗ₖ 0

Tactic:
exact Kernel.compProd_congr h

Result:
no goals

Proof state:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : κ ⊗ₖ η = 0
⊢ ∀ (a : α), ∀ᵐ (b : β) ∂κ a, (η (a, b)) Set.univ = 0

Tactic:
refine fun a ↦ (lintegral_eq_zero_iff ?_).mp ?_

Result:
case refine_1.refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : κ ⊗ₖ η = 0
a : α
⊢ Measurable fun b => (η (a, b)) Set.univ

case refine_1.refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : κ ⊗ₖ η = 0
a : α
⊢ ∫⁻ (a_1 : β), (η (a, a_1)) Set.univ ∂κ a = 0

Proof state:
case refine_1.refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : κ ⊗ₖ η = 0
a : α
⊢ (0 a) (Set.univ ×ˢ Set.univ) = 0

Tactic:
simp

Result:
no goals

Proof state:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : ∀ (a : α), ∀ᵐ (b : β) ∂κ a, η (a, b) = 0
⊢ κ ⊗ₖ η = 0

Tactic:
rw [← Kernel.compProd_zero_right κ]

Result:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : ∀ (a : α), ∀ᵐ (b : β) ∂κ a, η (a, b) = 0
⊢ κ ⊗ₖ η = κ ⊗ₖ 0

Proof state:
case refine_1.refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : κ ⊗ₖ η = 0
a : α
⊢ Measurable fun b => (η (a, b)) Set.univ

Tactic:
exact (η.measurable_coe .univ).comp measurable_prod_mk_left

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
⊢ κ ⊗ₖ η = 0 ↔ ∀ (a : α), ∀ᵐ (b : β) ∂κ a, η (a, b) = 0

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Result:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : κ ⊗ₖ η = 0
⊢ ∀ (a : α), ∀ᵐ (b : β) ∂κ a, η (a, b) = 0

case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : ∀ (a : α), ∀ᵐ (b : β) ∂κ a, η (a, b) = 0
⊢ κ ⊗ₖ η = 0

Proof state:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : κ ⊗ₖ η = 0
⊢ ∀ (a : α), ∀ᵐ (b : β) ∂κ a, η (a, b) = 0

Tactic:
simp_rw [← Measure.measure_univ_eq_zero]

Result:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : κ ⊗ₖ η = 0
⊢ ∀ (a : α), ∀ᵐ (b : β) ∂κ a, (η (a, b)) Set.univ = 0