-- Mathlib/Probability/Kernel/Composition/AbsolutelyContinuous.lean
lemma AbsolutelyContinuous.kernel_of_compProd [SFinite μ] (h : μ ⊗ₘ κ ≪ ν ⊗ₘ η) :
    ∀ᵐ a ∂μ, κ a ≪ η a

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝³ : IsFiniteKernel κ
inst✝² : IsFiniteKernel η
inst✝¹ : MeasurableSpace.CountableOrCountablyGenerated α β
inst✝ : SFinite μ
h : μ ⊗ₘ η.withDensity (κ.rnDeriv η) ≪ ν ⊗ₘ η ∧ μ ⊗ₘ κ.singularPart η ≪ ν ⊗ₘ η
⊢ ∀ᵐ (a : α) ∂μ, (κ.singularPart η) a = 0

Tactic:
have : μ ⊗ₘ κ.singularPart η ⟂ₘ ν ⊗ₘ η :=
  MutuallySingular.compProd_of_right μ ν (.of_forall <| Kernel.mutuallySingular_singularPart _ _)

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝³ : IsFiniteKernel κ
inst✝² : IsFiniteKernel η
inst✝¹ : MeasurableSpace.CountableOrCountablyGenerated α β
inst✝ : SFinite μ
h : μ ⊗ₘ η.withDensity (κ.rnDeriv η) ≪ ν ⊗ₘ η ∧ μ ⊗ₘ κ.singularPart η ≪ ν ⊗ₘ η
this : μ ⊗ₘ κ.singularPart η ⟂ₘ ν ⊗ₘ η
⊢ ∀ᵐ (a : α) ∂μ, (κ.singularPart η) a = 0

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝³ : IsFiniteKernel κ
inst✝² : IsFiniteKernel η
inst✝¹ : MeasurableSpace.CountableOrCountablyGenerated α β
inst✝ : SFinite μ
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
this : ∀ᵐ (a : α) ∂μ, (κ.singularPart η) a = 0
a : α
ha : (κ.singularPart η) a = 0
⊢ κ a ≪ η a

Tactic:
rwa [Kernel.singularPart_eq_zero_iff_absolutelyContinuous] at ha

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝³ : IsFiniteKernel κ
inst✝² : IsFiniteKernel η
inst✝¹ : MeasurableSpace.CountableOrCountablyGenerated α β
inst✝ : SFinite μ
h : μ ⊗ₘ η.withDensity (κ.rnDeriv η) ≪ ν ⊗ₘ η ∧ μ ⊗ₘ κ.singularPart η ≪ ν ⊗ₘ η
this : μ ⊗ₘ κ.singularPart η ⟂ₘ ν ⊗ₘ η
⊢ ∀ᵐ (a : α) ∂μ, (κ.singularPart η) a = 0

Tactic:
refine compProd_eq_zero_iff.mp ?_

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝³ : IsFiniteKernel κ
inst✝² : IsFiniteKernel η
inst✝¹ : MeasurableSpace.CountableOrCountablyGenerated α β
inst✝ : SFinite μ
h : μ ⊗ₘ η.withDensity (κ.rnDeriv η) ≪ ν ⊗ₘ η ∧ μ ⊗ₘ κ.singularPart η ≪ ν ⊗ₘ η
this : μ ⊗ₘ κ.singularPart η ⟂ₘ ν ⊗ₘ η
⊢ μ ⊗ₘ κ.singularPart η = 0

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝³ : IsFiniteKernel κ
inst✝² : IsFiniteKernel η
inst✝¹ : MeasurableSpace.CountableOrCountablyGenerated α β
inst✝ : SFinite μ
h : μ ⊗ₘ η.withDensity (κ.rnDeriv η) ≪ ν ⊗ₘ η ∧ μ ⊗ₘ κ.singularPart η ≪ ν ⊗ₘ η
this : μ ⊗ₘ κ.singularPart η ⟂ₘ ν ⊗ₘ η
⊢ μ ⊗ₘ κ.singularPart η = 0

Tactic:
exact eq_zero_of_absolutelyContinuous_of_mutuallySingular h.2 this

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝³ : IsFiniteKernel κ
inst✝² : IsFiniteKernel η
inst✝¹ : MeasurableSpace.CountableOrCountablyGenerated α β
inst✝ : SFinite μ
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
⊢ ∀ᵐ (a : α) ∂μ, κ a ≪ η a

Tactic:
suffices ∀ᵐ a ∂μ, κ.singularPart η a = 0 by
  filter_upwards [this] with a ha
  rwa [Kernel.singularPart_eq_zero_iff_absolutelyContinuous] at ha

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝³ : IsFiniteKernel κ
inst✝² : IsFiniteKernel η
inst✝¹ : MeasurableSpace.CountableOrCountablyGenerated α β
inst✝ : SFinite μ
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
⊢ ∀ᵐ (a : α) ∂μ, (κ.singularPart η) a = 0

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝³ : IsFiniteKernel κ
inst✝² : IsFiniteKernel η
inst✝¹ : MeasurableSpace.CountableOrCountablyGenerated α β
inst✝ : SFinite μ
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
⊢ ∀ᵐ (a : α) ∂μ, (κ.singularPart η) a = 0

Tactic:
rw [← κ.rnDeriv_add_singularPart η, compProd_add_right, AbsolutelyContinuous.add_left_iff] at h

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝³ : IsFiniteKernel κ
inst✝² : IsFiniteKernel η
inst✝¹ : MeasurableSpace.CountableOrCountablyGenerated α β
inst✝ : SFinite μ
h : μ ⊗ₘ η.withDensity (κ.rnDeriv η) ≪ ν ⊗ₘ η ∧ μ ⊗ₘ κ.singularPart η ≪ ν ⊗ₘ η
⊢ ∀ᵐ (a : α) ∂μ, (κ.singularPart η) a = 0

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝³ : IsFiniteKernel κ
inst✝² : IsFiniteKernel η
inst✝¹ : MeasurableSpace.CountableOrCountablyGenerated α β
inst✝ : SFinite μ
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
this : ∀ᵐ (a : α) ∂μ, (κ.singularPart η) a = 0
⊢ ∀ᵐ (a : α) ∂μ, κ a ≪ η a

Tactic:
filter_upwards [this] with a ha

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝³ : IsFiniteKernel κ
inst✝² : IsFiniteKernel η
inst✝¹ : MeasurableSpace.CountableOrCountablyGenerated α β
inst✝ : SFinite μ
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
this : ∀ᵐ (a : α) ∂μ, (κ.singularPart η) a = 0
a : α
ha : (κ.singularPart η) a = 0
⊢ κ a ≪ η a