awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
h_add : (μ + ν).rnDeriv (μ + ν) =ᶠ[ae ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
h_one_add : ∀ᵐ (x : α) ∂ν, (μ + ν).rnDeriv (μ + ν) x = (fun (x : α) ↦ (1 : ℝ≥0∞)) x
this : μ.rnDeriv (μ + ν) =ᶠ[ae ν] fun (x : α) ↦ 1 - (μ.rnDeriv ν x + 1)⁻¹
a : α
ha : μ.rnDeriv (μ + ν) a = 1 - (μ.rnDeriv ν a + 1)⁻¹
ha_lt_top : μ.rnDeriv ν a < ∞
⊢ (μ.rnDeriv ν a + 1)⁻¹ ≠ ∞

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
h_add : (μ + ν).rnDeriv (μ + ν) =ᶠ[ae ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
h_one_add : ∀ᵐ (x : α) ∂ν, (μ + ν).rnDeriv (μ + ν) x = (fun (x : α) ↦ (1 : ℝ≥0∞)) x
this : μ.rnDeriv (μ + ν) =ᶠ[ae ν] fun (x : α) ↦ 1 - (μ.rnDeriv ν x + 1)⁻¹
a : α
ha : μ.rnDeriv (μ + ν) a = 1 - (μ.rnDeriv ν a + 1)⁻¹
ha_lt_top : μ.rnDeriv ν a < ∞
h : 1 = μ.rnDeriv ν a * (μ.rnDeriv ν a + 1)⁻¹ + (μ.rnDeriv ν a + 1)⁻¹
⊢ 1 - (μ.rnDeriv ν a + 1)⁻¹ = μ.rnDeriv ν a * (μ.rnDeriv ν a + 1)⁻¹

Tactic:
refine ENNReal.sub_eq_of_eq_add (by simp) ?_

Premises used: ENNReal.sub_eq_of_eq_add
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
h_add : (μ + ν).rnDeriv (μ + ν) =ᶠ[ae ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
h_one_add : ∀ᵐ (x : α) ∂ν, (μ + ν).rnDeriv (μ + ν) x = (fun (x : α) ↦ (1 : ℝ≥0∞)) x
this : μ.rnDeriv (μ + ν) =ᶠ[ae ν] fun (x : α) ↦ 1 - (μ.rnDeriv ν x + 1)⁻¹
a : α
ha : μ.rnDeriv (μ + ν) a = 1 - (μ.rnDeriv ν a + 1)⁻¹
ha_lt_top : μ.rnDeriv ν a < ∞
h : 1 = μ.rnDeriv ν a * (μ.rnDeriv ν a + 1)⁻¹ + 1 * (μ.rnDeriv ν a + 1)⁻¹
⊢ 1 = μ.rnDeriv ν a * (μ.rnDeriv ν a + 1)⁻¹ + (μ.rnDeriv ν a + 1)⁻¹

Tactic:
nth_rewrite 2 [← one_mul (μ.rnDeriv ν a + 1)⁻¹]

Premises used: MeasureTheory.Measure.rnDeriv, Inv.inv, HAdd.hAdd, OfNat.ofNat, one_mul
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
h_add : (μ + ν).rnDeriv (μ + ν) =ᶠ[ae ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
h_one_add : ∀ᵐ (x : α) ∂ν, (μ + ν).rnDeriv (μ + ν) x = (fun (x : α) ↦ (1 : ℝ≥0∞)) x
this : μ.rnDeriv (μ + ν) =ᶠ[ae ν] fun (x : α) ↦ 1 - (μ.rnDeriv ν x + 1)⁻¹
a : α
ha : μ.rnDeriv (μ + ν) a = 1 - (μ.rnDeriv ν a + 1)⁻¹
ha_lt_top : μ.rnDeriv ν a < ∞
⊢ (μ.rnDeriv ν a + 1) * (μ.rnDeriv ν a + 1)⁻¹ = μ.rnDeriv ν a * (μ.rnDeriv ν a + 1)⁻¹ + 1 * (μ.rnDeriv ν a + 1)⁻¹

Tactic:
have h := add_mul (μ.rnDeriv ν a) 1 (μ.rnDeriv ν a + 1)⁻¹
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
h_add : (μ + ν).rnDeriv (μ + ν) =ᶠ[ae ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
h_one_add : ∀ᵐ (x : α) ∂ν, (μ + ν).rnDeriv (μ + ν) x = (fun (x : α) ↦ (1 : ℝ≥0∞)) x
this : μ.rnDeriv (μ + ν) =ᶠ[ae ν] fun (x : α) ↦ 1 - (μ.rnDeriv ν x + 1)⁻¹
a : α
ha : μ.rnDeriv (μ + ν) a = 1 - (μ.rnDeriv ν a + 1)⁻¹
ha_lt_top : μ.rnDeriv ν a < ∞
h : (μ.rnDeriv ν a + 1) * (μ.rnDeriv ν a + 1)⁻¹ = μ.rnDeriv ν a * (μ.rnDeriv ν a + 1)⁻¹ + 1 * (μ.rnDeriv ν a + 1)⁻¹
⊢ μ.rnDeriv ν a + 1 ≠ 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
h_add : (μ + ν).rnDeriv (μ + ν) =ᶠ[ae ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
h_one_add : ∀ᵐ (x : α) ∂ν, (μ + ν).rnDeriv (μ + ν) x = (fun (x : α) ↦ (1 : ℝ≥0∞)) x
this : μ.rnDeriv (μ + ν) =ᶠ[ae ν] fun (x : α) ↦ 1 - (μ.rnDeriv ν x + 1)⁻¹
a : α
ha : μ.rnDeriv (μ + ν) a = 1 - (μ.rnDeriv ν a + 1)⁻¹
ha_lt_top : μ.rnDeriv ν a < ∞
h : (μ.rnDeriv ν a + 1) * (μ.rnDeriv ν a + 1)⁻¹ = μ.rnDeriv ν a * (μ.rnDeriv ν a + 1)⁻¹ + 1 * (μ.rnDeriv ν a + 1)⁻¹
⊢ μ.rnDeriv ν a + 1 ≠ ∞

Tactic:
simp [ha_lt_top.ne]

Premises used: LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
h_add : (μ + ν).rnDeriv (μ + ν) =ᶠ[ae ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
h_one_add : ∀ᵐ (x : α) ∂ν, (μ + ν).rnDeriv (μ + ν) x = (fun (x : α) ↦ (1 : ℝ≥0∞)) x
this : μ.rnDeriv (μ + ν) =ᶠ[ae ν] fun (x : α) ↦ 1 - (μ.rnDeriv ν x + 1)⁻¹
a : α
ha : μ.rnDeriv (μ + ν) a = 1 - (μ.rnDeriv ν a + 1)⁻¹
ha_lt_top : μ.rnDeriv ν a < ∞
h : (μ.rnDeriv ν a + 1) * (μ.rnDeriv ν a + 1)⁻¹ = μ.rnDeriv ν a * (μ.rnDeriv ν a + 1)⁻¹ + 1 * (μ.rnDeriv ν a + 1)⁻¹
h₁ h₂ h₃ h₄ :
  ∀ (h : 1 = μ.rnDeriv ν a * (μ.rnDeriv ν a + 1)⁻¹ + 1 * (μ.rnDeriv ν a + 1)⁻¹),
    1 = μ.rnDeriv ν a * (μ.rnDeriv ν a + 1)⁻¹ + 1 * (μ.rnDeriv ν a + 1)⁻¹
⊢ 1 = μ.rnDeriv ν a * (μ.rnDeriv ν a + 1)⁻¹ + 1 * (μ.rnDeriv ν a + 1)⁻¹

Tactic:
rwa [ENNReal.mul_inv_cancel (by simp) (by simp [ha_lt_top.ne])] at h

Premises used: ENNReal.mul_inv_cancel
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
h :
  ∀ (a : α) (ha1 : ν.rnDeriv (μ + ν) a = (μ.rnDeriv ν a + 1)⁻¹)
    (ha2 : μ.rnDeriv (μ + ν) a = μ.rnDeriv ν a / (μ.rnDeriv ν a + 1)) (ha_lt_top : μ.rnDeriv ν a < ∞),
    μ.rnDeriv ν a = μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a
⊢ μ.rnDeriv ν =ᶠ[ae ν] fun (x : α) ↦ μ.rnDeriv (μ + ν) x / ν.rnDeriv (μ + ν) x

Tactic:
filter_upwards [rnDeriv_add_self ν μ, rnDeriv_self_add μ ν, μ.rnDeriv_lt_top ν]
      with a ha1 ha2 ha_lt_top

Premises used: MeasureTheory.Measure.rnDeriv_add_self, MeasureTheory.Measure.rnDeriv_lt_top, MeasureTheory.Measure.rnDeriv_self_add
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
a : α
ha1 : ν.rnDeriv (μ + ν) a = (μ.rnDeriv ν a + 1)⁻¹
ha2 : μ.rnDeriv (μ + ν) a = μ.rnDeriv ν a / (μ.rnDeriv ν a + 1)
ha_lt_top : μ.rnDeriv ν a < ∞
h : μ.rnDeriv ν a + 1 ≠ 0
h₁ : μ.rnDeriv ν a + 1 ≠ ∞
⊢ μ.rnDeriv ν a = μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a

Tactic:
rw [ha1, ha2, ENNReal.div_eq_inv_mul, inv_inv, ENNReal.div_eq_inv_mul, ← mul_assoc,
      ENNReal.mul_inv_cancel, one_mul]

Premises used: mul_assoc, ENNReal.mul_inv_cancel, inv_inv, one_mul, ENNReal.div_eq_inv_mul
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
a : α
ha1 : ν.rnDeriv (μ + ν) a = (μ.rnDeriv ν a + 1)⁻¹
ha2 : μ.rnDeriv (μ + ν) a = μ.rnDeriv ν a / (μ.rnDeriv ν a + 1)
ha_lt_top : μ.rnDeriv ν a < ∞
⊢ μ.rnDeriv ν a + 1 ≠ 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
a : α
ha1 : ν.rnDeriv (μ + ν) a = (μ.rnDeriv ν a + 1)⁻¹
ha2 : μ.rnDeriv (μ + ν) a = μ.rnDeriv ν a / (μ.rnDeriv ν a + 1)
ha_lt_top : μ.rnDeriv ν a < ∞
⊢ μ.rnDeriv ν a + 1 ≠ ∞

Tactic:
simp [ha_lt_top.ne]

Premises used: LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ξ
hμ : μ ≪ ξ
hν : ν ≪ ξ
⊢ μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᶠ[ae ξ] μ.rnDeriv ξ

Tactic:
have h1 : μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᵐ[ξ] μ.rnDeriv ξ :=
    Measure.rnDeriv_mul_rnDeriv (rfl.absolutelyContinuous.add_right _)
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ξ
hμ : μ ≪ ξ
hν : ν ≪ ξ
h1 : μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᶠ[ae ξ] μ.rnDeriv ξ
⊢ ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᶠ[ae ξ] ν.rnDeriv ξ

Tactic:
have h2 : ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᵐ[ξ] ν.rnDeriv ξ :=
    Measure.rnDeriv_mul_rnDeriv (rfl.absolutelyContinuous.add_right' _)
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ξ
hμ : μ ≪ ξ
hν : ν ≪ ξ
h1 : μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᶠ[ae ξ] μ.rnDeriv ξ
h2 : ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᶠ[ae ξ] ν.rnDeriv ξ
⊢ μ + ν ≪ ξ

Tactic:
have h_ac : μ + ν ≪ ξ := hμ.add_left hν
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ξ
hμ : μ ≪ ξ
hν : ν ≪ ξ
h1 : μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᶠ[ae ξ] μ.rnDeriv ξ
h2 : ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᶠ[ae ξ] ν.rnDeriv ξ
h_ac : μ + ν ≪ ξ
h :
  ∀ (a : α) (h1 : (μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a = μ.rnDeriv ξ a)
    (h2 : (ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a = ν.rnDeriv ξ a) (h_lt_top1 : (μ + ν).rnDeriv ξ a < ∞)
    (h_lt_top2 : ν.rnDeriv (μ + ν) a < ∞) (h_pos : 0 < (μ + ν).rnDeriv ξ a),
    μ.rnDeriv ξ a / ν.rnDeriv ξ a = μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a
⊢ (ae (μ + ν)).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ μ.rnDeriv ξ x / ν.rnDeriv ξ x) fun (x : α) ↦
    μ.rnDeriv (μ + ν) x / ν.rnDeriv (μ + ν) x

Tactic:
filter_upwards [h_ac h1, h_ac h2, h_ac <| (μ + ν).rnDeriv_lt_top ξ, ν.rnDeriv_lt_top (μ + ν),
    Measure.rnDeriv_pos h_ac] with a h1 h2 h_lt_top1 h_lt_top2 h_pos

Premises used: MeasureTheory.Measure.rnDeriv_lt_top, MeasureTheory.Measure.rnDeriv_pos, HAdd.hAdd
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ξ
hμ : μ ≪ ξ
hν : ν ≪ ξ
h1_1 : μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᶠ[ae ξ] μ.rnDeriv ξ
h2_1 : ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᶠ[ae ξ] ν.rnDeriv ξ
h_ac : μ + ν ≪ ξ
a : α
h1 : (μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a = μ.rnDeriv ξ a
h2 : (ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a = ν.rnDeriv ξ a
h_lt_top1 : (μ + ν).rnDeriv ξ a < ∞
h_lt_top2 : ν.rnDeriv (μ + ν) a < ∞
h_pos : 0 < (μ + ν).rnDeriv ξ a
h : (μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a / ν.rnDeriv ξ a = μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a
h₁ :
  (μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a / (ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a =
    μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a
h₂ :
  μ.rnDeriv (μ + ν) a * (μ + ν).rnDeriv ξ a / (ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a =
    μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a
h₃ :
  μ.rnDeriv (μ + ν) a * (μ + ν).rnDeriv ξ a / (ν.rnDeriv (μ + ν) a * (μ + ν).rnDeriv ξ a) =
    μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a
h₄ :
  μ.rnDeriv (μ + ν) a * (μ + ν).rnDeriv ξ a * (ν.rnDeriv (μ + ν) a * (μ + ν).rnDeriv ξ a)⁻¹ =
    μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a
h₅ :
  μ.rnDeriv (μ + ν) a * (μ + ν).rnDeriv ξ a * ((ν.rnDeriv (μ + ν) a)⁻¹ * ((μ + ν).rnDeriv ξ a)⁻¹) =
    μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a
h₆ :
  μ.rnDeriv (μ + ν) a * (μ + ν).rnDeriv ξ a * ((ν.rnDeriv (μ + ν) a)⁻¹ * ((μ + ν).rnDeriv ξ a)⁻¹) =
    μ.rnDeriv (μ + ν) a * (ν.rnDeriv (μ + ν) a)⁻¹
h₇ :
  μ.rnDeriv (μ + ν) a * ((μ + ν).rnDeriv ξ a * ((ν.rnDeriv (μ + ν) a)⁻¹ * ((μ + ν).rnDeriv ξ a)⁻¹)) =
    μ.rnDeriv (μ + ν) a * (ν.rnDeriv (μ + ν) a)⁻¹
h₈ :
  μ.rnDeriv (μ + ν) a * ((ν.rnDeriv (μ + ν) a)⁻¹ * ((μ + ν).rnDeriv ξ a)⁻¹ * (μ + ν).rnDeriv ξ a) =
    μ.rnDeriv (μ + ν) a * (ν.rnDeriv (μ + ν) a)⁻¹
h₉ :
  μ.rnDeriv (μ + ν) a * ((ν.rnDeriv (μ + ν) a)⁻¹ * (((μ + ν).rnDeriv ξ a)⁻¹ * (μ + ν).rnDeriv ξ a)) =
    μ.rnDeriv (μ + ν) a * (ν.rnDeriv (μ + ν) a)⁻¹
h₁₀ : μ.rnDeriv (μ + ν) a * ((ν.rnDeriv (μ + ν) a)⁻¹ * 1) = μ.rnDeriv (μ + ν) a * (ν.rnDeriv (μ + ν) a)⁻¹
h₁₁ h₁₂ : μ.rnDeriv (μ + ν) a * (ν.rnDeriv (μ + ν) a)⁻¹ = μ.rnDeriv (μ + ν) a * (ν.rnDeriv (μ + ν) a)⁻¹
⊢ μ.rnDeriv ξ a / ν.rnDeriv ξ a = μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a

Tactic:
rw [← h1, ← h2, Pi.mul_apply, Pi.mul_apply, div_eq_mul_inv,
    ENNReal.mul_inv (Or.inr h_lt_top1.ne) (Or.inl h_lt_top2.ne), div_eq_mul_inv, mul_assoc,
    mul_comm ((μ + ν).rnDeriv ξ a), mul_assoc, ENNReal.inv_mul_cancel h_pos.ne' h_lt_top1.ne,
    mul_one]

Premises used: Pi.mul_apply, mul_assoc, MeasureTheory.Measure.rnDeriv, div_eq_mul_inv, LT.lt.ne', HAdd.hAdd, mul_comm, Or.inl, ENNReal.inv_mul_cancel, mul_one, ENNReal.mul_inv, Or.inr, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ξ
hμ : μ ≪ ξ
hν : ν ≪ ξ
⊢ ν ≪ μ + ν

Tactic:
have hν_ac : ν ≪ μ + ν := rfl.absolutelyContinuous.add_right' _
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ξ
hμ : μ ≪ ξ
hν : ν ≪ ξ
hν_ac : ν ≪ μ + ν
a : α
h1 : μ.rnDeriv ν a = μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a
h2 : μ.rnDeriv ξ a / ν.rnDeriv ξ a = μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a
⊢ μ.rnDeriv ν a = μ.rnDeriv ξ a / ν.rnDeriv ξ a

Tactic:
h1.trans h2.symm

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ξ
hμ : μ ≪ ξ
hν : ν ≪ ξ
hν_ac : ν ≪ μ + ν
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α)
            {x : α | (fun (x : α) ↦ μ.rnDeriv ν x = (fun (x : α) ↦ μ.rnDeriv (μ + ν) x / ν.rnDeriv (μ + ν) x) x) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α)
                  {x : α |
                    (fun (x : α) ↦
                        Eq (α := ℝ≥0∞) ((fun (x : α) ↦ μ.rnDeriv ξ x / ν.rnDeriv ξ x) x)
                          ((fun (x : α) ↦ μ.rnDeriv (μ + ν) x / ν.rnDeriv (μ + ν) x) x))
                      x}
                  x →
                Membership.mem (γ := Set α)
                  {x : α | (fun (x : α) ↦ μ.rnDeriv ν x = (fun (x : α) ↦ μ.rnDeriv ξ x / ν.rnDeriv ξ x) x) x} x}
            x}
      a
h₁ h₂ :
  ∀ (a : α) (h1 : μ.rnDeriv ν a = μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a)
    (h2 : μ.rnDeriv ξ a / ν.rnDeriv ξ a = μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a),
    μ.rnDeriv ν a = μ.rnDeriv ξ a / ν.rnDeriv ξ a
⊢ μ.rnDeriv ν =ᶠ[ae ν] fun (x : α) ↦ μ.rnDeriv ξ x / ν.rnDeriv ξ x

Tactic:
filter_upwards [μ.rnDeriv_eq_div_rnDeriv_add ν,
    hν_ac (rnDeriv_div_rnDeriv_eq_div_rnDeriv_add hμ hν)] with a h1 h2 using h1.trans h2.symm

Premises used: MeasureTheory.Measure.rnDeriv_div_rnDeriv_eq_div_rnDeriv_add, MeasureTheory.Measure.rnDeriv_eq_div_rnDeriv_add
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
⊢ (fun (x : α) ↦ rnDeriv (m := mβ) (map f μ) (map f ν) (f x)) =ᶠ[ae ν] μ.rnDeriv ν

Tactic:
ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite ?_ ?_ (fun s _ _ ↦ ?_)

Premises used: MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
refine_1 : Measurable (β := ℝ≥0∞) fun (x : α) ↦ rnDeriv (m := mβ) (map f μ) (map f ν) (f x)
refine_2 : Measurable (μ.rnDeriv ν)
refine_3 :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, rnDeriv (m := mβ) (map f μ) (map f ν) (f x) ∂ν = ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν
⊢ (fun (x : α) ↦ rnDeriv (m := mβ) (map f μ) (map f ν) (f x)) =ᶠ[ae ν] μ.rnDeriv ν

Tactic:
refine ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite ?_ ?_ (fun s _ _ ↦ ?_)

Premises used: MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ rnDeriv (m := mβ) (map f μ) (map f ν) (f x)

Tactic:
(Measure.measurable_rnDeriv _ _).comp hf.measurable

Premises used: Measurable.comp, MeasurableEmbedding.measurable, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ rnDeriv (m := mβ) (map f μ) (map f ν) (f x)

Tactic:
exact (Measure.measurable_rnDeriv _ _).comp hf.measurable

Premises used: Measurable.comp, MeasurableEmbedding.measurable, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
⊢ Measurable (μ.rnDeriv ν)

Tactic:
Measure.measurable_rnDeriv _ _

Premises used: MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
⊢ Measurable (μ.rnDeriv ν)

Tactic:
exact Measure.measurable_rnDeriv _ _

Premises used: MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
s : Set α
h : MeasurableSet s
h_1 : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_3 : ∫⁻ (a : β), rnDeriv (m := mβ) (map f μ) (map f ν) a ∂map f (ν.restrict s) = (μ : (a : Set α) → ℝ≥0∞) s
⊢ ∫⁻ (x : α) in s, rnDeriv (m := mβ) (map f μ) (map f ν) (f x) ∂ν = ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν

Tactic:
rw [← hf.lintegral_map, Measure.setLIntegral_rnDeriv hμν]

Premises used: MeasureTheory.Measure.setLIntegral_rnDeriv, MeasurableEmbedding.lintegral_map
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
s : Set α
h : MeasurableSet s
h_1 : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw rw₁ : s = s
⊢ s = f ⁻¹' f '' s

Tactic:
rw [hf.injective.preimage_image]

Premises used: MeasurableEmbedding.injective, Function.Injective.preimage_image
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
s : Set α
h : MeasurableSet s
h_1 : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ s = f ⁻¹' f '' s

Tactic:
have hs_eq : s = f ⁻¹' f '' s := by rw [hf.injective.preimage_image]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
s : Set α
h : MeasurableSet s
h_1 : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hs_eq : s = f ⁻¹' f '' s
⊢ SigmaFinite (m0 := mβ) (map f ν)

Tactic:
have : SigmaFinite (ν.map f) := hf.sigmaFinite_map
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
s : Set α
h : MeasurableSet s
h_1 : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hs_eq : s = f ⁻¹' f '' s
this : SigmaFinite (m0 := mβ) (map f ν)
refine_3 :
  ∫⁻ (a : β), rnDeriv (m := mβ) (map f μ) (map f ν) a ∂map f (ν.restrict (f ⁻¹' f '' s)) =
    (μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' f '' s)
refine_3₁ :
  ∫⁻ (a : β) in f '' s, rnDeriv (m := mβ) (map f μ) (map f ν) a ∂map f ν = (μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' f '' s)
refine_3₂ :
  Eq (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' f '' s) : ℝ≥0∞)
refine_3₃ refine_3₄ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' f '' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' f '' s) : ℝ≥0∞)
⊢ ∫⁻ (a : β), rnDeriv (m := mβ) (map f μ) (map f ν) a ∂map f (ν.restrict s) = (μ : (a : Set α) → ℝ≥0∞) s

Tactic:
rw [hs_eq, ← hf.restrict_map, Measure.setLIntegral_rnDeriv (hf.absolutelyContinuous_map hμν),
    hf.map_apply]

Premises used: MeasureTheory.Measure.setLIntegral_rnDeriv, MeasurableEmbedding.restrict_map, MeasurableEmbedding.map_apply, MeasurableEmbedding.absolutelyContinuous_map
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
rw :
  (fun (x : α) ↦
      (HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν)) (map f (ν.withDensity (μ.rnDeriv ν)))).rnDeriv (map f ν)
        (f x)) =ᶠ[ae ν]
    (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
⊢ (fun (x : α) ↦ rnDeriv (m := mβ) (map f μ) (map f ν) (f x)) =ᶠ[ae ν] μ.rnDeriv ν

Tactic:
rw [μ.haveLebesgueDecomposition_add ν, Measure.map_add _ _ hf.measurable]

Premises used: MeasureTheory.Measure.map_add, MeasureTheory.Measure.haveLebesgueDecomposition_add, MeasurableEmbedding.measurable
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
⊢ SigmaFinite (m0 := mβ) (map f ν)

Tactic:
have : SigmaFinite (map f ν) := hf.sigmaFinite_map
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
this : SigmaFinite (m0 := mβ) (map f ν)
⊢ SigmaFinite (m0 := mβ) (map f (μ.singularPart ν))

Tactic:
have : SigmaFinite (map f (μ.singularPart ν)) := hf.sigmaFinite_map
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
this_1 : SigmaFinite (m0 := mβ) (map f ν)
this : SigmaFinite (m0 := mβ) (map f (μ.singularPart ν))
⊢ SigmaFinite (m0 := mβ) (map f (ν.withDensity (μ.rnDeriv ν)))

Tactic:
have : SigmaFinite (map f (ν.withDensity (μ.rnDeriv ν))) := hf.sigmaFinite_map
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
this_1 : SigmaFinite (m0 := mβ) (map f ν)
this_2 : SigmaFinite (m0 := mβ) (map f (μ.singularPart ν))
this : SigmaFinite (m0 := mβ) (map f (ν.withDensity (μ.rnDeriv ν)))
⊢ (HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν)) (map f (ν.withDensity (μ.rnDeriv ν)))).rnDeriv
      (map f ν) =ᶠ[ae (F := Measure β) (map f ν)]
    rnDeriv (m := mβ) (map f (μ.singularPart ν)) (map f ν) +
      rnDeriv (m := mβ) (map f (ν.withDensity (μ.rnDeriv ν))) (map f ν)

Tactic:
have h_add := Measure.rnDeriv_add' ((μ.singularPart ν).map f)
    ((ν.withDensity (μ.rnDeriv ν)).map f) (ν.map f)