awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ν ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_key :
  ∀ (t₁ : Set α) (t₂ : Set β),
    MeasurableSet t₁ →
      MeasurableSet t₂ →
        ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
          ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
t : Set (α × β)
ht : MeasurableSet t
ht_eq : ∫⁻ (x : α × β) in t, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in t, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
refine_3 : ∫⁻ (x : α × β), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β), μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
⊢ ∫⁻ (x : α × β), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ - ∫⁻ (x : α × β) in t, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ =
    ∫⁻ (x : α × β), μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ - ∫⁻ (x : α × β) in t, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ

Tactic:
congr 1
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ν ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_key :
  ∀ (t₁ : Set α) (t₂ : Set β),
    MeasurableSet t₁ →
      MeasurableSet t₂ →
        ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
          ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
t : Set (α × β)
ht : MeasurableSet t
ht_eq : ∫⁻ (x : α × β) in t, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in t, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
⊢ ∫⁻ (x : α × β) in SProd.sprod (α := Set α) (β := Set β) univ univ, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
    ∫⁻ (x : α × β) in SProd.sprod (α := Set α) (β := Set β) univ univ, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ

Tactic:
specialize h_key .univ .univ .univ .univ

Premises used: Set.univ, MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ν ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set (α × β)
ht : MeasurableSet t
ht_eq : ∫⁻ (x : α × β) in t, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in t, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
h_key :
  ∫⁻ (x : α × β) in SProd.sprod (α := Set α) (β := Set β) univ univ, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
    ∫⁻ (x : α × β) in SProd.sprod (α := Set α) (β := Set β) univ univ, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
⊢ ∫⁻ (x : α × β), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β), μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ

Tactic:
simpa only [univ_prod_univ, Measure.restrict_univ] using h_key

Premises used: Set.univ_prod_univ, MeasureTheory.Measure.restrict_univ
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ν ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_key :
  ∀ (t₁ : Set α) (t₂ : Set β),
    MeasurableSet t₁ →
      MeasurableSet t₂ →
        ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
          ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
t : Set (α × β)
ht : MeasurableSet t
ht_eq : ∫⁻ (x : α × β) in t, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in t, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
refine_3 : ∫⁻ (x : α × β) in t, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ ≠ ∞
⊢ ∫⁻ (x : α × β) in t, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ ≠ ∞

Tactic:
rw [← ht_eq]
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ν ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_key :
  ∀ (t₁ : Set α) (t₂ : Set β),
    MeasurableSet t₁ →
      MeasurableSet t₂ →
        ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
          ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
t : Set (α × β)
ht : MeasurableSet t
ht_eq : ∫⁻ (x : α × β) in t, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in t, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
⊢ ∫⁻ (x : α × β) in t, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ ≠ ∞

Tactic:
((Measure.setLIntegral_rnDeriv_le _).trans_lt (measure_lt_top _ _)).ne

Premises used: MeasureTheory.measure_lt_top, LE.le.trans_lt, MeasureTheory.Measure.setLIntegral_rnDeriv_le, LT.lt.ne
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ν ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_key :
  ∀ (t₁ : Set α) (t₂ : Set β),
    MeasurableSet t₁ →
      MeasurableSet t₂ →
        ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
          ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
t : Set (α × β)
ht : MeasurableSet t
ht_eq : ∫⁻ (x : α × β) in t, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in t, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
⊢ ∫⁻ (x : α × β) in t, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ ≠ ∞

Tactic:
exact ((Measure.setLIntegral_rnDeriv_le _).trans_lt (measure_lt_top _ _)).ne

Premises used: MeasureTheory.measure_lt_top, LE.le.trans_lt, MeasureTheory.Measure.setLIntegral_rnDeriv_le, LT.lt.ne
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ν ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_key :
  ∀ (t₁ : Set α) (t₂ : Set β),
    MeasurableSet t₁ →
      MeasurableSet t₂ →
        ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
          ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
f' : ℕ → Set (α × β)
hf_disj : Pairwise (Function.onFun Disjoint f')
hf_meas : ∀ (i : ℕ), MeasurableSet (f' i)
hf_eq :
  ∀ (i : ℕ),
    ∫⁻ (x : α × β) in f' i, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in f' i, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
refine_4 :
  Eq (α := ℝ≥0∞) (∑' (i : ℕ), ∫⁻ (a : α × β) in f' i, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) a ∂ν ⊗ₘ κ)
    (∑' (i : ℕ), ∫⁻ (a : α × β) in f' i, μ.rnDeriv ν a.1 ∂ν ⊗ₘ κ)
⊢ ∫⁻ (x : α × β) in ⋃ (i : ℕ), f' i, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
    ∫⁻ (x : α × β) in ⋃ (i : ℕ), f' i, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ

Tactic:
rw [lintegral_iUnion hf_meas hf_disj, lintegral_iUnion hf_meas hf_disj]

Premises used: MeasureTheory.lintegral_iUnion
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ν ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_key :
  ∀ (t₁ : Set α) (t₂ : Set β),
    MeasurableSet t₁ →
      MeasurableSet t₂ →
        ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
          ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
f' : ℕ → Set (α × β)
hf_disj : Pairwise (Function.onFun Disjoint f')
hf_meas : ∀ (i : ℕ), MeasurableSet (f' i)
hf_eq :
  ∀ (i : ℕ),
    ∫⁻ (x : α × β) in f' i, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in f' i, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
refine_4 :
  ∀ (i : ℕ),
    ∫⁻ (a : α × β) in f' i, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) a ∂ν ⊗ₘ κ = ∫⁻ (a : α × β) in f' i, μ.rnDeriv ν a.1 ∂ν ⊗ₘ κ
⊢ Eq (α := ℝ≥0∞) (∑' (i : ℕ), ∫⁻ (a : α × β) in f' i, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) a ∂ν ⊗ₘ κ)
    (∑' (i : ℕ), ∫⁻ (a : α × β) in f' i, μ.rnDeriv ν a.1 ∂ν ⊗ₘ κ)

Tactic:
congr with i
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ν ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_key :
  ∀ (t₁ : Set α) (t₂ : Set β),
    MeasurableSet t₁ →
      MeasurableSet t₂ →
        ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
          ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
f' : ℕ → Set (α × β)
hf_disj : Pairwise (Function.onFun Disjoint f')
hf_meas : ∀ (i : ℕ), MeasurableSet (f' i)
hf_eq :
  ∀ (i : ℕ),
    ∫⁻ (x : α × β) in f' i, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in f' i, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
i : ℕ
⊢ ∫⁻ (a : α × β) in f' i, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) a ∂ν ⊗ₘ κ = ∫⁻ (a : α × β) in f' i, μ.rnDeriv ν a.1 ∂ν ⊗ₘ κ

Tactic:
hf_eq i
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ν ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_key :
  ∀ (t₁ : Set α) (t₂ : Set β),
    MeasurableSet t₁ →
      MeasurableSet t₂ →
        ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
          ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
f' : ℕ → Set (α × β)
hf_disj : Pairwise (Function.onFun Disjoint f')
hf_meas : ∀ (i : ℕ), MeasurableSet (f' i)
hf_eq :
  ∀ (i : ℕ),
    ∫⁻ (x : α × β) in f' i, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in f' i, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
i : ℕ
⊢ ∫⁻ (a : α × β) in f' i, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) a ∂ν ⊗ₘ κ = ∫⁻ (a : α × β) in f' i, μ.rnDeriv ν a.1 ∂ν ⊗ₘ κ

Tactic:
exact hf_eq i
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
rw : ((μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)
| (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)

Tactic:
rw [Measure.haveLebesgueDecomposition_add μ ν]

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_add
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
conv_rhs :
  (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)]
    ((μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)
⊢ (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)] (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)

Tactic:
conv_rhs => rw [Measure.haveLebesgueDecomposition_add μ ν]

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_add
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
rw :
  (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)]
    (μ.singularPart ν ⊗ₘ κ + ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)
⊢ (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)]
    ((μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)

Tactic:
rw [Measure.compProd_add_left]

Premises used: MeasureTheory.Measure.compProd_add_left
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
⊢ (μ.singularPart ν ⊗ₘ κ + ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)]
    (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) + (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)

Tactic:
have h := Measure.rnDeriv_add' (μ.singularPart ν ⊗ₘ κ) (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ)
    (ν ⊗ₘ η)
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
h :
  (μ.singularPart ν ⊗ₘ κ + ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)]
    (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) + (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)
⊢ (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)] 0

Tactic:
Measure.rnDeriv_eq_zero_of_mutuallySingular ?_ ?_

Premises used: MeasureTheory.Measure.rnDeriv_eq_zero_of_mutuallySingular
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
h :
  (μ.singularPart ν ⊗ₘ κ + ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)]
    (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) + (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)
refine_1 : μ.singularPart ν ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
refine_2 : ν ⊗ₘ η ≪ ν ⊗ₘ η
⊢ (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)] 0

Tactic:
refine Measure.rnDeriv_eq_zero_of_mutuallySingular ?_ ?_

Premises used: MeasureTheory.Measure.rnDeriv_eq_zero_of_mutuallySingular
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
h :
  (μ.singularPart ν ⊗ₘ κ + ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)]
    (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) + (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)
⊢ μ.singularPart ν ⊗ₘ κ ⟂ₘ ν ⊗ₘ η

Tactic:
Measure.MutuallySingular.compProd_of_left (μ.mutuallySingular_singularPart _) _ _

Premises used: MeasureTheory.Measure.MutuallySingular.compProd_of_left, MeasureTheory.Measure.mutuallySingular_singularPart
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
h :
  (μ.singularPart ν ⊗ₘ κ + ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)]
    (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) + (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)
⊢ μ.singularPart ν ⊗ₘ κ ⟂ₘ ν ⊗ₘ η

Tactic:
exact Measure.MutuallySingular.compProd_of_left (μ.mutuallySingular_singularPart _) _ _

Premises used: MeasureTheory.Measure.MutuallySingular.compProd_of_left, MeasureTheory.Measure.mutuallySingular_singularPart
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
h :
  (μ.singularPart ν ⊗ₘ κ + ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)]
    (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) + (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)
⊢ ν ⊗ₘ η ≪ ν ⊗ₘ η

Tactic:
Measure.AbsolutelyContinuous.rfl

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.rfl
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
h :
  (μ.singularPart ν ⊗ₘ κ + ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)]
    (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) + (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)
⊢ ν ⊗ₘ η ≪ ν ⊗ₘ η

Tactic:
exact Measure.AbsolutelyContinuous.rfl

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.rfl
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
h :
  (μ.singularPart ν ⊗ₘ κ + ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)]
    (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) + (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)
⊢ (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)] 0

Tactic:
have h2 : (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᵐ[ν ⊗ₘ η] 0 := by
    refine Measure.rnDeriv_eq_zero_of_mutuallySingular ?_ ?_
    · exact Measure.MutuallySingular.compProd_of_left (μ.mutuallySingular_singularPart _) _ _
    · exact Measure.AbsolutelyContinuous.rfl
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
h :
  (μ.singularPart ν ⊗ₘ κ + ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)]
    (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) + (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)
h2 : (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)] 0
h₁ :
  ∀ (x : α × β)
    (hx :
      (μ.singularPart ν ⊗ₘ κ + ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x =
        ((μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) + (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)) x)
    (hx2 : (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x = 0 x),
    (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x =
      (μ.singularPart ν ⊗ₘ κ + ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x
⊢ (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)]
    (μ.singularPart ν ⊗ₘ κ + ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)

Tactic:
filter_upwards [h, h2] with x hx hx2
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
h :
  (μ.singularPart ν ⊗ₘ κ + ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)]
    (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) + (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)
h2 : (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)] 0
x : α × β
hx :
  (μ.singularPart ν ⊗ₘ κ + ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x =
    ((μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) + (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)) x
hx2 : (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x = 0 x
⊢ (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x =
    (μ.singularPart ν ⊗ₘ κ + ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x

Tactic:
simp [hx, hx2]
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
⊢ (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) =ᶠ[ae (ν ⊗ₘ κ)] (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ)

Tactic:
(rnDeriv_compProd_withDensity_rnDeriv μ ν κ κ).symm

Premises used: ProbabilityTheory.rnDeriv_compProd_withDensity_rnDeriv, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
⊢ (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) =ᶠ[ae (ν ⊗ₘ κ)] fun (p : α × β) ↦
    (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν p.1

Tactic:
rnDeriv_measure_compProd_left_of_ac
      (MeasureTheory.withDensity_absolutelyContinuous ν (μ.rnDeriv ν)) κ

Premises used: _private.0.ProbabilityTheory.rnDeriv_measure_compProd_left_of_ac, MeasureTheory.Measure.rnDeriv, MeasureTheory.withDensity_absolutelyContinuous
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
⊢ Measurable ((ν.withDensity (μ.rnDeriv ν)).rnDeriv ν)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
⊢ Measurable (μ.rnDeriv ν)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
⊢ (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) =ᶠ[ae (ν ⊗ₘ κ)] fun (p : α × β) ↦ μ.rnDeriv ν p.1

Tactic:
calc (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ)
  _ =ᵐ[ν ⊗ₘ κ] (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) :=
    (rnDeriv_compProd_withDensity_rnDeriv μ ν κ κ).symm
  _ =ᵐ[ν ⊗ₘ κ] (fun p ↦ (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν p.1) :=
    rnDeriv_measure_compProd_left_of_ac
      (MeasureTheory.withDensity_absolutelyContinuous ν (μ.rnDeriv ν)) κ
  _ =ᵐ[ν ⊗ₘ κ] fun p ↦ μ.rnDeriv ν p.1 :=
    Measure.ae_eq_compProd_of_ae_eq_fst _ (by fun_prop) (by fun_prop)
      (Measure.rnDeriv_withDensity ν (by fun_prop))

Premises used: _private.0.ProbabilityTheory.rnDeriv_measure_compProd_left_of_ac, MeasureTheory.Measure.withDensity, MeasureTheory.Measure.rnDeriv, MeasureTheory.Measure.rnDeriv_withDensity, MeasureTheory.withDensity_absolutelyContinuous, MeasureTheory.Measure.compProd, ProbabilityTheory.rnDeriv_compProd_withDensity_rnDeriv, Filter.EventuallyEq.symm, MeasureTheory.Measure.ae_eq_compProd_of_ae_eq_fst
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : IsFiniteKernel η
h_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η
ν : Measure α
inst_3 : IsFiniteMeasure ν
⊢ (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)] fun (p : α × β) ↦ μ.rnDeriv ν p.1 * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) p

Tactic:
Filter.EventuallyEq.trans (Measure.rnDeriv_mul_rnDeriv h_ac).symm ?_

Premises used: Filter.EventuallyEq.trans, MeasureTheory.Measure.rnDeriv_mul_rnDeriv, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : IsFiniteKernel η
h_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η
ν : Measure α
inst_3 : IsFiniteMeasure ν
refine :
  (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) * (μ ⊗ₘ η).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)] fun (p : α × β) ↦
    μ.rnDeriv ν p.1 * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) p
⊢ (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)] fun (p : α × β) ↦ μ.rnDeriv ν p.1 * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) p

Tactic:
refine Filter.EventuallyEq.trans (Measure.rnDeriv_mul_rnDeriv h_ac).symm ?_

Premises used: Filter.EventuallyEq.trans, MeasureTheory.Measure.rnDeriv_mul_rnDeriv, Filter.EventuallyEq.symm