awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_meas : Measurable (μ.rnDeriv ν)
h_sing : μ.singularPart ν ⟂ₘ ν
hμν : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
x : α
hx1 :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x =
    ((μ.singularPart ν).rnDeriv κ + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ) x
hx2 : (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x = μ.rnDeriv ν x * ν.rnDeriv κ x
hx3 : (μ.singularPart ν).rnDeriv κ x = 0 x
h : (μ.rnDeriv ν * ν.rnDeriv κ) x = ((μ.singularPart ν).rnDeriv κ + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ) x
⊢ (μ.rnDeriv ν * ν.rnDeriv κ) x = (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x
have h₁ : (μ.rnDeriv ν * ν.rnDeriv κ) x = (μ.singularPart ν).rnDeriv κ x + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x
Tactic: rw [hx1, Pi.add_apply, hx2, Pi.mul_apply, hx3, Pi.zero_apply, zero_add]
-- 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_meas : Measurable (μ.rnDeriv ν)
h_sing : μ.singularPart ν ⟂ₘ ν
hμν : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
x : α
hx1 :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x =
    ((μ.singularPart ν).rnDeriv κ + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ) x
hx2 : (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x = μ.rnDeriv ν x * ν.rnDeriv κ x
hx3 : (μ.singularPart ν).rnDeriv κ x = 0 x
h : (μ.rnDeriv ν * ν.rnDeriv κ) x = ((μ.singularPart ν).rnDeriv κ + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ) x
h₁ : (μ.rnDeriv ν * ν.rnDeriv κ) x = (μ.singularPart ν).rnDeriv κ x + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x
⊢ (μ.rnDeriv ν * ν.rnDeriv κ) x = (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x
have h₂ : (μ.rnDeriv ν * ν.rnDeriv κ) x = (μ.singularPart ν).rnDeriv κ x + μ.rnDeriv ν x * ν.rnDeriv κ x
Tactic: rw [hx1, Pi.add_apply, hx2, Pi.mul_apply, hx3, Pi.zero_apply, zero_add]
-- 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_meas : Measurable (μ.rnDeriv ν)
h_sing : μ.singularPart ν ⟂ₘ ν
hμν : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
x : α
hx1 :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x =
    ((μ.singularPart ν).rnDeriv κ + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ) x
hx2 : (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x = μ.rnDeriv ν x * ν.rnDeriv κ x
hx3 : (μ.singularPart ν).rnDeriv κ x = 0 x
h : (μ.rnDeriv ν * ν.rnDeriv κ) x = ((μ.singularPart ν).rnDeriv κ + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ) x
h₁ : (μ.rnDeriv ν * ν.rnDeriv κ) x = (μ.singularPart ν).rnDeriv κ x + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x
h₂ : (μ.rnDeriv ν * ν.rnDeriv κ) x = (μ.singularPart ν).rnDeriv κ x + μ.rnDeriv ν x * ν.rnDeriv κ x
⊢ (μ.rnDeriv ν * ν.rnDeriv κ) x = (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x
have h₃ : μ.rnDeriv ν x * ν.rnDeriv κ x = (μ.singularPart ν).rnDeriv κ x + μ.rnDeriv ν x * ν.rnDeriv κ x
Tactic: rw [hx1, Pi.add_apply, hx2, Pi.mul_apply, hx3, Pi.zero_apply, zero_add]
-- 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_meas : Measurable (μ.rnDeriv ν)
h_sing : μ.singularPart ν ⟂ₘ ν
hμν : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
x : α
hx1 :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x =
    ((μ.singularPart ν).rnDeriv κ + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ) x
hx2 : (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x = μ.rnDeriv ν x * ν.rnDeriv κ x
hx3 : (μ.singularPart ν).rnDeriv κ x = 0 x
h : (μ.rnDeriv ν * ν.rnDeriv κ) x = ((μ.singularPart ν).rnDeriv κ + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ) x
h₁ : (μ.rnDeriv ν * ν.rnDeriv κ) x = (μ.singularPart ν).rnDeriv κ x + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x
h₂ : (μ.rnDeriv ν * ν.rnDeriv κ) x = (μ.singularPart ν).rnDeriv κ x + μ.rnDeriv ν x * ν.rnDeriv κ x
h₃ : μ.rnDeriv ν x * ν.rnDeriv κ x = (μ.singularPart ν).rnDeriv κ x + μ.rnDeriv ν x * ν.rnDeriv κ x
⊢ (μ.rnDeriv ν * ν.rnDeriv κ) x = (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x
have h₄ : μ.rnDeriv ν x * ν.rnDeriv κ x = 0 x + μ.rnDeriv ν x * ν.rnDeriv κ x
Tactic: rw [hx1, Pi.add_apply, hx2, Pi.mul_apply, hx3, Pi.zero_apply, zero_add]
-- 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_meas : Measurable (μ.rnDeriv ν)
h_sing : μ.singularPart ν ⟂ₘ ν
hμν : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
x : α
hx1 :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x =
    ((μ.singularPart ν).rnDeriv κ + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ) x
hx2 : (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x = μ.rnDeriv ν x * ν.rnDeriv κ x
hx3 : (μ.singularPart ν).rnDeriv κ x = 0 x
h : (μ.rnDeriv ν * ν.rnDeriv κ) x = ((μ.singularPart ν).rnDeriv κ + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ) x
h₁ : (μ.rnDeriv ν * ν.rnDeriv κ) x = (μ.singularPart ν).rnDeriv κ x + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x
h₂ : (μ.rnDeriv ν * ν.rnDeriv κ) x = (μ.singularPart ν).rnDeriv κ x + μ.rnDeriv ν x * ν.rnDeriv κ x
h₃ : μ.rnDeriv ν x * ν.rnDeriv κ x = (μ.singularPart ν).rnDeriv κ x + μ.rnDeriv ν x * ν.rnDeriv κ x
h₄ : μ.rnDeriv ν x * ν.rnDeriv κ x = 0 x + μ.rnDeriv ν x * ν.rnDeriv κ x
⊢ (μ.rnDeriv ν * ν.rnDeriv κ) x = (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x
have h₅ : μ.rnDeriv ν x * ν.rnDeriv κ x = 0 + μ.rnDeriv ν x * ν.rnDeriv κ x
Tactic: rw [hx1, Pi.add_apply, hx2, Pi.mul_apply, hx3, Pi.zero_apply, zero_add]
-- 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_meas : Measurable (μ.rnDeriv ν)
h_sing : μ.singularPart ν ⟂ₘ ν
hμν : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
x : α
hx1 :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x =
    ((μ.singularPart ν).rnDeriv κ + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ) x
hx2 : (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x = μ.rnDeriv ν x * ν.rnDeriv κ x
hx3 : (μ.singularPart ν).rnDeriv κ x = 0 x
h : (μ.rnDeriv ν * ν.rnDeriv κ) x = ((μ.singularPart ν).rnDeriv κ + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ) x
h₁ : (μ.rnDeriv ν * ν.rnDeriv κ) x = (μ.singularPart ν).rnDeriv κ x + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x
h₂ : (μ.rnDeriv ν * ν.rnDeriv κ) x = (μ.singularPart ν).rnDeriv κ x + μ.rnDeriv ν x * ν.rnDeriv κ x
h₃ : μ.rnDeriv ν x * ν.rnDeriv κ x = (μ.singularPart ν).rnDeriv κ x + μ.rnDeriv ν x * ν.rnDeriv κ x
h₄ : μ.rnDeriv ν x * ν.rnDeriv κ x = 0 x + μ.rnDeriv ν x * ν.rnDeriv κ x
h₅ : μ.rnDeriv ν x * ν.rnDeriv κ x = 0 + μ.rnDeriv ν x * ν.rnDeriv κ x
⊢ (μ.rnDeriv ν * ν.rnDeriv κ) x = (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x
have h₆ : μ.rnDeriv ν x * ν.rnDeriv κ x = μ.rnDeriv ν x * ν.rnDeriv κ x
Tactic: rw [hx1, Pi.add_apply, hx2, Pi.mul_apply, hx3, Pi.zero_apply, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hμν : μ ≤ ν
inst : SigmaFinite ν
⊢ μ.rnDeriv ν ≤ᶠ[ae ν] 1
have refine : ∀ (s : Set α),
  MeasurableSet s →
    LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
      ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν ≤ ∫⁻ (x : α) in s, 1 x ∂ν
Tactic: refine ae_le_of_forall_setLIntegral_le_of_sigmaFinite (μ.measurable_rnDeriv ν) fun s _ _ ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hμν : μ ≤ ν
inst : SigmaFinite ν
s : Set α
h : MeasurableSet s
h_1 : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν ≤ ∫⁻ (x : α) in s, 1 x ∂ν
have simp : ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν ≤ (ν : (a : Set α) → ℝ≥0∞) s
Tactic: simp only [Pi.one_apply, MeasureTheory.setLIntegral_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
⊢ μ.rnDeriv ν ≤ᶠ[ae ν] 1 ↔ μ ≤ ν
have refine : ∀ (h : μ.rnDeriv ν ≤ᶠ[ae ν] 1) (s : Set α),
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: refine ⟨fun h s ↦ ?_, fun h ↦ rnDeriv_le_one_of_le h⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
h : μ.rnDeriv ν ≤ᶠ[ae ν] 1
s : Set α
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : ∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν ≤ ∫⁻ (x : α) in s, 1 ∂ν
Tactic: rw [← withDensity_rnDeriv_eq _ _ hμν, withDensity_apply', ← setLIntegral_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
⊢ μ.rnDeriv ν =ᶠ[ae ν] 1 ↔ μ = ν
have refine : ∀ (h : μ.rnDeriv ν =ᶠ[ae ν] 1), μ = ν
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ h ▸ ν.rnDeriv_self⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
h : μ.rnDeriv ν =ᶠ[ae ν] 1
⊢ μ = ν
have rw : ν.withDensity (μ.rnDeriv ν) = ν
Tactic: rw [← withDensity_rnDeriv_eq _ _ hμν, withDensity_congr_ae h, withDensity_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
h : μ.rnDeriv ν =ᶠ[ae ν] 1
rw : ν.withDensity (μ.rnDeriv ν) = ν
⊢ μ = ν
have rw₁ : ν.withDensity 1 = ν
Tactic: rw [← withDensity_rnDeriv_eq _ _ hμν, withDensity_congr_ae h, withDensity_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
h : μ.rnDeriv ν =ᶠ[ae ν] 1
rw : ν.withDensity (μ.rnDeriv ν) = ν
rw₁ : ν.withDensity 1 = ν
⊢ μ = ν
have rw₂ : ν = ν
Tactic: rw [← withDensity_rnDeriv_eq _ _ hμν, withDensity_congr_ae h, withDensity_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
⊢ μ.rnDeriv (ν + μ) =ᶠ[ae μ] fun (x : α) ↦ (ν.rnDeriv μ x + 1)⁻¹
have hν_ac : μ ≪ ν + μ
Tactic: have hν_ac : μ ≪ ν + μ := rfl.absolutelyContinuous.add_right' _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hν_ac : μ ≪ ν + μ
⊢ μ.rnDeriv (ν + μ) =ᶠ[ae μ] fun (x : α) ↦ (ν.rnDeriv μ x + 1)⁻¹
have h : ∀ (a : α) (h1 : (ν + μ).rnDeriv μ a = (ν.rnDeriv μ + μ.rnDeriv μ) a) (h2 : μ.rnDeriv μ a = 1)
  (h3 : (μ.rnDeriv (ν + μ))⁻¹ a = (ν + μ).rnDeriv μ a), μ.rnDeriv (ν + μ) a = (ν.rnDeriv μ a + 1)⁻¹
Tactic: filter_upwards [ν.rnDeriv_add' μ μ, μ.rnDeriv_self, Measure.inv_rnDeriv hν_ac] with a h1 h2 h3
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hν_ac : μ ≪ ν + μ
a : α
h1 : (ν + μ).rnDeriv μ a = (ν.rnDeriv μ + μ.rnDeriv μ) a
h2 : μ.rnDeriv μ a = 1
h3 : μ.rnDeriv (ν + μ) a = (ν.rnDeriv μ a + 1)⁻¹
⊢ μ.rnDeriv (ν + μ) a = (ν.rnDeriv μ a + 1)⁻¹
have h : (ν.rnDeriv μ a + 1)⁻¹ = (ν.rnDeriv μ a + 1)⁻¹
Tactic: rw [h3]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
⊢ μ.rnDeriv (μ + ν) =ᶠ[ae ν] fun (x : α) ↦ μ.rnDeriv ν x / (μ.rnDeriv ν x + 1)
have h_add : (μ + ν).rnDeriv (μ + ν) =ᶠ[ae ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
Tactic: have h_add : (μ + ν).rnDeriv (μ + ν) =ᵐ[ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν) :=
    (ae_add_measure_iff.mp (μ.rnDeriv_add' ν (μ + ν))).2
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
h_add : (μ + ν).rnDeriv (μ + ν) =ᶠ[ae ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
⊢ μ.rnDeriv (μ + ν) =ᶠ[ae ν] fun (x : α) ↦ μ.rnDeriv ν x / (μ.rnDeriv ν x + 1)
have h_one_add : ∀ᵐ (x : α) ∂ν, (μ + ν).rnDeriv (μ + ν) x = (fun (x : α) ↦ (1 : ℝ≥0∞)) x
Tactic: have h_one_add := (ae_add_measure_iff.mp (μ + ν).rnDeriv_self).2
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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
⊢ μ.rnDeriv (μ + ν) =ᶠ[ae ν] fun (x : α) ↦ 1 - (μ.rnDeriv ν x + 1)⁻¹
have h : ∀ (a : α) (h4 : (μ + ν).rnDeriv (μ + ν) a = (μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)) a)
  (h5 : (μ + ν).rnDeriv (μ + ν) a = 1) (h6 : ν.rnDeriv (μ + ν) a = (μ.rnDeriv ν a + 1)⁻¹),
  μ.rnDeriv (μ + ν) a = 1 - (μ.rnDeriv ν a + 1)⁻¹
Tactic: filter_upwards [h_add, h_one_add, rnDeriv_add_self ν μ] with a h4 h5 h6
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
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
a : α
h4 : (μ + ν).rnDeriv (μ + ν) a = (μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)) a
h5 : (μ + ν).rnDeriv (μ + ν) a = 1
h6 : ν.rnDeriv (μ + ν) a = (μ.rnDeriv ν a + 1)⁻¹
⊢ μ.rnDeriv (μ + ν) a = 1 - (μ.rnDeriv ν a + 1)⁻¹
have h4₁ : 1 = μ.rnDeriv (μ + ν) a + ν.rnDeriv (μ + ν) a
Tactic: rw [h5, Pi.add_apply] at h4
Cleared hypotheses: h4, h5, h6
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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
a : α
h4 : 1 = μ.rnDeriv (μ + ν) a + ν.rnDeriv (μ + ν) a
h5 : (μ + ν).rnDeriv (μ + ν) a = 1
h6 : ν.rnDeriv (μ + ν) a = (μ.rnDeriv ν a + 1)⁻¹
⊢ μ.rnDeriv (μ + ν) a = 1 - (μ.rnDeriv ν a + 1)⁻¹
have h : μ.rnDeriv (μ + ν) a = μ.rnDeriv (μ + ν) a + (μ.rnDeriv ν a + 1)⁻¹ - (μ.rnDeriv ν a + 1)⁻¹
Tactic: nth_rw 1 [h4, h6]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
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
⊢ μ.rnDeriv (μ + ν) =ᶠ[ae ν] fun (x : α) ↦ μ.rnDeriv ν x / (μ.rnDeriv ν x + 1)
have this : μ.rnDeriv (μ + ν) =ᶠ[ae ν] fun (x : α) ↦ 1 - (μ.rnDeriv ν x + 1)⁻¹
Tactic: have : (μ.rnDeriv (μ + ν)) =ᵐ[ν] fun x ↦ 1 - (μ.rnDeriv ν x + 1)⁻¹ := by
    filter_upwards [h_add, h_one_add, rnDeriv_add_self ν μ] with a h4 h5 h6
    rw [h5, Pi.add_apply] at h4
    nth_rw 1 [h4, h6]
    simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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)⁻¹
⊢ μ.rnDeriv (μ + ν) =ᶠ[ae ν] fun (x : α) ↦ μ.rnDeriv ν x / (μ.rnDeriv ν x + 1)
have h : ∀ (a : α) (ha : μ.rnDeriv (μ + ν) a = 1 - (μ.rnDeriv ν a + 1)⁻¹) (ha_lt_top : μ.rnDeriv ν a < ∞),
  μ.rnDeriv (μ + ν) a = μ.rnDeriv ν a / (μ.rnDeriv ν a + 1)
Tactic: filter_upwards [this, μ.rnDeriv_lt_top ν] with a ha ha_lt_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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 = μ.rnDeriv ν a / (μ.rnDeriv ν a + 1)
have h : 1 - (μ.rnDeriv ν a + 1)⁻¹ = μ.rnDeriv ν a * (μ.rnDeriv ν a + 1)⁻¹
Tactic: rw [ha, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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 < ∞
⊢ 1 - (μ.rnDeriv ν a + 1)⁻¹ = μ.rnDeriv ν a * (μ.rnDeriv ν a + 1)⁻¹
have h : 1 = μ.rnDeriv ν a * (μ.rnDeriv ν a + 1)⁻¹ + (μ.rnDeriv ν a + 1)⁻¹
Tactic: refine ENNReal.sub_eq_of_eq_add (by simp) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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 < ∞
⊢ 1 = μ.rnDeriv ν a * (μ.rnDeriv ν a + 1)⁻¹ + (μ.rnDeriv ν a + 1)⁻¹
have h : 1 = μ.rnDeriv ν a * (μ.rnDeriv ν a + 1)⁻¹ + 1 * (μ.rnDeriv ν a + 1)⁻¹
Tactic: nth_rewrite 2 [← one_mul (μ.rnDeriv ν a + 1)⁻¹]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
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 < ∞
⊢ 1 = μ.rnDeriv ν a * (μ.rnDeriv ν a + 1)⁻¹ + 1 * (μ.rnDeriv ν a + 1)⁻¹
have h : (μ.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)⁻¹
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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)⁻¹
⊢ 1 = μ.rnDeriv ν a * (μ.rnDeriv ν a + 1)⁻¹ + 1 * (μ.rnDeriv ν a + 1)⁻¹
have h₁ : ∀ (h : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
⊢ μ.rnDeriv ν =ᶠ[ae ν] fun (x : α) ↦ μ.rnDeriv (μ + ν) x / ν.rnDeriv (μ + ν) x
have 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
Tactic: filter_upwards [rnDeriv_add_self ν μ, rnDeriv_self_add μ ν, μ.rnDeriv_lt_top ν]
      with a ha1 ha2 ha_lt_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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 = μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a
have h : μ.rnDeriv ν a + 1 ≠ 0
Tactic: rw [ha1, ha2, ENNReal.div_eq_inv_mul, inv_inv, ENNReal.div_eq_inv_mul, ← mul_assoc,
      ENNReal.mul_inv_cancel, one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
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
⊢ μ.rnDeriv ν a = μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a
have h₁ : μ.rnDeriv ν a + 1 ≠ ∞
Tactic: rw [ha1, ha2, ENNReal.div_eq_inv_mul, inv_inv, ENNReal.div_eq_inv_mul, ← mul_assoc,
      ENNReal.mul_inv_cancel, one_mul]
-- 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ν : ν ≪ ξ
⊢ (ae (μ + ν)).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ μ.rnDeriv ξ x / ν.rnDeriv ξ x) fun (x : α) ↦
    μ.rnDeriv (μ + ν) x / ν.rnDeriv (μ + ν) x
have h1 : μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᶠ[ae ξ] μ.rnDeriv ξ
Tactic: have h1 : μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᵐ[ξ] μ.rnDeriv ξ :=
    Measure.rnDeriv_mul_rnDeriv (rfl.absolutelyContinuous.add_right _)
-- 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 ξ
⊢ (ae (μ + ν)).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ μ.rnDeriv ξ x / ν.rnDeriv ξ x) fun (x : α) ↦
    μ.rnDeriv (μ + ν) x / ν.rnDeriv (μ + ν) x
have h2 : ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᶠ[ae ξ] ν.rnDeriv ξ
Tactic: have h2 : ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᵐ[ξ] ν.rnDeriv ξ :=
    Measure.rnDeriv_mul_rnDeriv (rfl.absolutelyContinuous.add_right' _)