awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
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 ξ
⊢ (ae (μ + ν)).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ μ.rnDeriv ξ x / ν.rnDeriv ξ x) fun (x : α) ↦
    μ.rnDeriv (μ + ν) x / ν.rnDeriv (μ + ν) x
have h_ac : μ + ν ≪ ξ
Tactic: have h_ac : μ + ν ≪ ξ := hμ.add_left hν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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 : μ + ν ≪ ξ
⊢ (ae (μ + ν)).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ μ.rnDeriv ξ x / ν.rnDeriv ξ x) fun (x : α) ↦
    μ.rnDeriv (μ + ν) x / ν.rnDeriv (μ + ν) x
have 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
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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
⊢ μ.rnDeriv ξ a / ν.rnDeriv ξ a = μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a
have h : (μ.rnDeriv (μ + ν) * (μ + ν).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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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
⊢ μ.rnDeriv ξ a / ν.rnDeriv ξ a = μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a
have h₁ : (μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a / (ν.rnDeriv (μ + ν) * (μ + ν).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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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
⊢ μ.rnDeriv ξ a / ν.rnDeriv ξ a = μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a
have h₂ : μ.rnDeriv (μ + ν) a * (μ + ν).rnDeriv ξ a / (ν.rnDeriv (μ + ν) * (μ + ν).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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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
⊢ μ.rnDeriv ξ a / ν.rnDeriv ξ a = μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a
have h₃ : μ.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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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
⊢ μ.rnDeriv ξ a / ν.rnDeriv ξ a = μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a
have h₄ : μ.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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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
⊢ μ.rnDeriv ξ a / ν.rnDeriv ξ a = μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a
have h₅ : μ.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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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
⊢ μ.rnDeriv ξ a / ν.rnDeriv ξ a = μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a
have h₆ : μ.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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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)⁻¹
⊢ μ.rnDeriv ξ a / ν.rnDeriv ξ a = μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a
have h₇ : μ.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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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)⁻¹
⊢ μ.rnDeriv ξ a / ν.rnDeriv ξ a = μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a
have h₈ : μ.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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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)⁻¹
⊢ μ.rnDeriv ξ a / ν.rnDeriv ξ a = μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a
have h₉ : μ.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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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)⁻¹
⊢ μ.rnDeriv ξ a / ν.rnDeriv ξ a = μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a
have h₁₀ : μ.rnDeriv (μ + ν) a * ((ν.rnDeriv (μ + ν) a)⁻¹ * 1) = μ.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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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)⁻¹
⊢ μ.rnDeriv ξ a / ν.rnDeriv ξ a = μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a
have h₁₁ : μ.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]