-- Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean
lemma mutuallySingular_compProd_left_iff [SFinite μ] [SigmaFinite ν]
    [IsSFiniteKernel κ] [hκ : ∀ x, NeZero (κ x)] :
    μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ ↔ μ ⟂ₘ ν

Proof state:
case refine_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst✝² : SFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero (κ x)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
⊢ ν.withDensity (μ.rnDeriv ν) ≪ μ

Tactic:
exact absolutelyContinuous_of_le (μ.withDensity_rnDeriv_le ν)

Result:
no goals

Proof state:
case refine_3
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst✝² : SFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero (κ x)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
hh : ∀ᵐ (x : α) ∂ν.withDensity (μ.rnDeriv ν), False
⊢ ν.withDensity (μ.rnDeriv ν) = 0

Tactic:
exact ae_eq_bot.mp (Filter.eventually_false_iff_eq_bot.mp hh)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst✝² : SFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero (κ x)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
⊢ μ ⟂ₘ ν

Tactic:
rw [← withDensity_rnDeriv_eq_zero]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst✝² : SFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero (κ x)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
⊢ ν.withDensity (μ.rnDeriv ν) = 0

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst✝² : SFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero (κ x)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
⊢ ν.withDensity (μ.rnDeriv ν) = 0

Tactic:
have hh := mutuallySingular_of_mutuallySingular_compProd h ?_ ?_
  (ξ := ν.withDensity (μ.rnDeriv ν))

Result:
case refine_3
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst✝² : SFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero (κ x)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
hh : ∀ᵐ (x : α) ∂ν.withDensity (μ.rnDeriv ν), κ x ⟂ₘ κ x
⊢ ν.withDensity (μ.rnDeriv ν) = 0

case refine_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst✝² : SFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero (κ x)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
⊢ ν.withDensity (μ.rnDeriv ν) ≪ μ

case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst✝² : SFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero (κ x)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
⊢ ν.withDensity (μ.rnDeriv ν) ≪ ν

Proof state:
case refine_3
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst✝² : SFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero (κ x)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
hh : ∀ᵐ (x : α) ∂ν.withDensity (μ.rnDeriv ν), κ x ⟂ₘ κ x
⊢ ν.withDensity (μ.rnDeriv ν) = 0

Tactic:
simp_rw [MutuallySingular.self_iff, (hκ _).ne] at hh

Result:
case refine_3
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst✝² : SFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero (κ x)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
hh : ∀ᵐ (x : α) ∂ν.withDensity (μ.rnDeriv ν), False
⊢ ν.withDensity (μ.rnDeriv ν) = 0

Proof state:
case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst✝² : SFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero (κ x)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
⊢ ν.withDensity (μ.rnDeriv ν) ≪ ν

Tactic:
exact withDensity_absolutelyContinuous _ _

Result:
no goals

Proof state:
case refine_3
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst✝² : SFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero (κ x)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
hh : ∀ᵐ (x : α) ∂ν.withDensity (μ.rnDeriv ν), κ x ⟂ₘ κ x
⊢ ν.withDensity (μ.rnDeriv ν) = 0

case refine_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst✝² : SFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero (κ x)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
⊢ ν.withDensity (μ.rnDeriv ν) ≪ μ

case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst✝² : SFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero (κ x)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
⊢ ν.withDensity (μ.rnDeriv ν) ≪ ν

Tactic:
rotate_left

Result:
case refine_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst✝² : SFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero (κ x)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
⊢ ν.withDensity (μ.rnDeriv ν) ≪ μ

case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst✝² : SFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero (κ x)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
⊢ ν.withDensity (μ.rnDeriv ν) ≪ ν

case refine_3
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst✝² : SFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero (κ x)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
hh : ∀ᵐ (x : α) ∂ν.withDensity (μ.rnDeriv ν), κ x ⟂ₘ κ x
⊢ ν.withDensity (μ.rnDeriv ν) = 0

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst✝² : SFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero (κ x)
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ ↔ μ ⟂ₘ ν

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

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst✝² : SFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero (κ x)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
⊢ μ ⟂ₘ ν