awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
inst_1 : t.HaveLebesgueDecomposition μ
inst_2 : (s + t).HaveLebesgueDecomposition μ
rw :
  (s + t).singularPart μ + μ.withDensityᵥ ((s + t).rnDeriv μ) =
    (s + t).singularPart μ + μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
rw₁ : s + t = (s + t).singularPart μ + μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
rw₂ : s + t = (s + t).singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + μ.withDensityᵥ (t.rnDeriv μ))
rw₃ : s + t = s.singularPart μ + t.singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + μ.withDensityᵥ (t.rnDeriv μ))
rw₄ : s + t = s.singularPart μ + (t.singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + μ.withDensityᵥ (t.rnDeriv μ)))
rw₅ : s + t = s.singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + μ.withDensityᵥ (t.rnDeriv μ) + t.singularPart μ)
rw₆ : s + t = s.singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + (μ.withDensityᵥ (t.rnDeriv μ) + t.singularPart μ))
rw₇ : s + t = s.singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + (t.singularPart μ + μ.withDensityᵥ (t.rnDeriv μ)))
rw₈ : s + t = s.singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + t)
rw₉ : s + t = s.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ) + t
⊢ μ.withDensityᵥ ((s + t).rnDeriv μ) = μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
have rw₁₀ : s + t = s + t
Tactic: rw [← add_right_inj ((s + t).singularPart μ), singularPart_add_withDensity_rnDeriv_eq,
    withDensityᵥ_add (integrable_rnDeriv _ _) (integrable_rnDeriv _ _), singularPart_add,
    add_assoc, add_comm (t.singularPart μ), add_assoc, add_comm _ (t.singularPart μ),
    singularPart_add_withDensity_rnDeriv_eq, ← add_assoc,
    singularPart_add_withDensity_rnDeriv_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
inst_1 : t.HaveLebesgueDecomposition μ
hst : (s - t).HaveLebesgueDecomposition μ
⊢ (s - t).rnDeriv μ =ᶠ[ae μ] s.rnDeriv μ - t.rnDeriv μ
have hst₁ : (s + -t).HaveLebesgueDecomposition μ
Tactic: rw [sub_eq_add_neg] at hst
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
inst_1 : t.HaveLebesgueDecomposition μ
hst : (s + -t).HaveLebesgueDecomposition μ
⊢ (s - t).rnDeriv μ =ᶠ[ae μ] s.rnDeriv μ - t.rnDeriv μ
have rw : (s + -t).rnDeriv μ =ᶠ[ae μ] s.rnDeriv μ + -t.rnDeriv μ
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : Measure α
⊢ Integrable (c.rnDeriv μ) μ
have rw : MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.re : (a : ℂ) → ℝ) (c.rnDeriv μ x)) 1 μ ∧
  MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.im : (a : ℂ) → ℝ) (c.rnDeriv μ x)) 1 μ
Tactic: rw [← memLp_one_iff_integrable, ← memLp_re_im_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst : c.HaveLebesgueDecomposition μ
| c
have rw : SignedMeasure.toComplexMeasure ((re : (a : ComplexMeasure α) → SignedMeasure α) c)
  ((im : (a : ComplexMeasure α) → SignedMeasure α) c)
Tactic: rw [← c.toComplexMeasure_to_signedMeasure]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst : c.HaveLebesgueDecomposition μ
⊢ c.singularPart μ + μ.withDensityᵥ (c.rnDeriv μ) = c
have conv_rhs : c.singularPart μ + μ.withDensityᵥ (c.rnDeriv μ) =
  SignedMeasure.toComplexMeasure ((re : (a : ComplexMeasure α) → SignedMeasure α) c)
    ((im : (a : ComplexMeasure α) → SignedMeasure α) c)
Tactic: conv_rhs => rw [← c.toComplexMeasure_to_signedMeasure]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst : c.HaveLebesgueDecomposition μ
⊢ c.singularPart μ + μ.withDensityᵥ (c.rnDeriv μ) =
    SignedMeasure.toComplexMeasure ((re : (a : ComplexMeasure α) → SignedMeasure α) c)
      ((im : (a : ComplexMeasure α) → SignedMeasure α) c)
have h : ∀ (i : Set α) (hi : MeasurableSet i),
  (↑(c.singularPart μ + μ.withDensityᵥ (c.rnDeriv μ)) : Set α → ℂ) i =
    (↑(SignedMeasure.toComplexMeasure ((re : (a : ComplexMeasure α) → SignedMeasure α) c)
            ((im : (a : ComplexMeasure α) → SignedMeasure α) c)) :
        Set α → ℂ)
      i
Tactic: ext i hi : 1
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ (↑(c.singularPart μ) : Set α → ℂ) i + (↑(μ.withDensityᵥ (c.rnDeriv μ)) : Set α → ℂ) i =
    { re := (↑((re : (a : ComplexMeasure α) → SignedMeasure α) c) : Set α → ℝ) i,
      im := (↑((im : (a : ComplexMeasure α) → SignedMeasure α) c) : Set α → ℝ) i }
have h : ((↑(c.singularPart μ) : Set α → ℂ) i + (↑(μ.withDensityᵥ (c.rnDeriv μ)) : Set α → ℂ) i).re =
  { re := (↑((re : (a : ComplexMeasure α) → SignedMeasure α) c) : Set α → ℝ) i,
      im := (↑((im : (a : ComplexMeasure α) → SignedMeasure α) c) : Set α → ℝ) i }.re
Tactic: apply Complex.ext
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
h :
  ((↑(c.singularPart μ) : Set α → ℂ) i + (↑(μ.withDensityᵥ (c.rnDeriv μ)) : Set α → ℂ) i).re =
    { re := (↑((re : (a : ComplexMeasure α) → SignedMeasure α) c) : Set α → ℝ) i,
        im := (↑((im : (a : ComplexMeasure α) → SignedMeasure α) c) : Set α → ℝ) i }.re
⊢ (↑(c.singularPart μ) : Set α → ℂ) i + (↑(μ.withDensityᵥ (c.rnDeriv μ)) : Set α → ℂ) i =
    { re := (↑((re : (a : ComplexMeasure α) → SignedMeasure α) c) : Set α → ℝ) i,
      im := (↑((im : (a : ComplexMeasure α) → SignedMeasure α) c) : Set α → ℝ) i }
have h₁ : ((↑(c.singularPart μ) : Set α → ℂ) i + (↑(μ.withDensityᵥ (c.rnDeriv μ)) : Set α → ℂ) i).im =
  { re := (↑((re : (a : ComplexMeasure α) → SignedMeasure α) c) : Set α → ℝ) i,
      im := (↑((im : (a : ComplexMeasure α) → SignedMeasure α) c) : Set α → ℝ) i }.im
Tactic: apply Complex.ext
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ ((↑(c.singularPart μ) : Set α → ℂ) i + (↑(μ.withDensityᵥ (c.rnDeriv μ)) : Set α → ℂ) i).re =
    { re := (↑((re : (a : ComplexMeasure α) → SignedMeasure α) c) : Set α → ℝ) i,
        im := (↑((im : (a : ComplexMeasure α) → SignedMeasure α) c) : Set α → ℝ) i }.re
have h : ((↑(c.singularPart μ) : Set α → ℂ) i).re + (↑(μ.withDensityᵥ fun (x : α) ↦ (c.rnDeriv μ x).re) : Set α → ℝ) i =
  { re := (↑((re : (a : ComplexMeasure α) → SignedMeasure α) c) : Set α → ℝ) i,
      im := (↑((im : (a : ComplexMeasure α) → SignedMeasure α) c) : Set α → ℝ) i }.re
Tactic: rw [Complex.add_re, withDensityᵥ_apply (c.integrable_rnDeriv μ) hi, ← RCLike.re_eq_complex_re,
      ← integral_re (c.integrable_rnDeriv μ).integrableOn, RCLike.re_eq_complex_re,
      ← withDensityᵥ_apply _ hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
h :
  ((↑(c.singularPart μ) : Set α → ℂ) i).re + (↑(μ.withDensityᵥ fun (x : α) ↦ (c.rnDeriv μ x).re) : Set α → ℝ) i =
    { re := (↑((re : (a : ComplexMeasure α) → SignedMeasure α) c) : Set α → ℝ) i,
        im := (↑((im : (a : ComplexMeasure α) → SignedMeasure α) c) : Set α → ℝ) i }.re
⊢ ((↑(c.singularPart μ) : Set α → ℂ) i + (↑(μ.withDensityᵥ (c.rnDeriv μ)) : Set α → ℂ) i).re =
    { re := (↑((re : (a : ComplexMeasure α) → SignedMeasure α) c) : Set α → ℝ) i,
        im := (↑((im : (a : ComplexMeasure α) → SignedMeasure α) c) : Set α → ℝ) i }.re
have rw : Integrable (ε := ℝ) (fun (x : α) ↦ (c.rnDeriv μ x).re) μ
Tactic: rw [Complex.add_re, withDensityᵥ_apply (c.integrable_rnDeriv μ) hi, ← RCLike.re_eq_complex_re,
      ← integral_re (c.integrable_rnDeriv μ).integrableOn, RCLike.re_eq_complex_re,
      ← withDensityᵥ_apply _ hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ (↑(SignedMeasure.singularPart ((re : (a : ComplexMeasure α) → SignedMeasure α) c) μ +
            μ.withDensityᵥ (SignedMeasure.rnDeriv ((re : (a : ComplexMeasure α) → SignedMeasure α) c) μ)) :
        Set α → ℝ)
      i =
    { re := (↑((re : (a : ComplexMeasure α) → SignedMeasure α) c) : Set α → ℝ) i,
        im := (↑((im : (a : ComplexMeasure α) → SignedMeasure α) c) : Set α → ℝ) i }.re
have h : (↑((re : (a : ComplexMeasure α) → SignedMeasure α) c) : Set α → ℝ) i =
  { re := (↑((re : (a : ComplexMeasure α) → SignedMeasure α) c) : Set α → ℝ) i,
      im := (↑((im : (a : ComplexMeasure α) → SignedMeasure α) c) : Set α → ℝ) i : ℂ }.re
Tactic: rw [c.re.singularPart_add_withDensity_rnDeriv_eq μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ ((↑(c.singularPart μ) : Set α → ℂ) i + (↑(μ.withDensityᵥ (c.rnDeriv μ)) : Set α → ℂ) i).im =
    { re := (↑((re : (a : ComplexMeasure α) → SignedMeasure α) c) : Set α → ℝ) i,
        im := (↑((im : (a : ComplexMeasure α) → SignedMeasure α) c) : Set α → ℝ) i }.im
have h : ((↑(c.singularPart μ) : Set α → ℂ) i).im + (↑(μ.withDensityᵥ fun (x : α) ↦ (c.rnDeriv μ x).im) : Set α → ℝ) i =
  { re := (↑((re : (a : ComplexMeasure α) → SignedMeasure α) c) : Set α → ℝ) i,
      im := (↑((im : (a : ComplexMeasure α) → SignedMeasure α) c) : Set α → ℝ) i }.im
Tactic: rw [Complex.add_im, withDensityᵥ_apply (c.integrable_rnDeriv μ) hi, ← RCLike.im_eq_complex_im,
      ← integral_im (c.integrable_rnDeriv μ).integrableOn, RCLike.im_eq_complex_im,
      ← withDensityᵥ_apply _ hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
h :
  ((↑(c.singularPart μ) : Set α → ℂ) i).im + (↑(μ.withDensityᵥ fun (x : α) ↦ (c.rnDeriv μ x).im) : Set α → ℝ) i =
    { re := (↑((re : (a : ComplexMeasure α) → SignedMeasure α) c) : Set α → ℝ) i,
        im := (↑((im : (a : ComplexMeasure α) → SignedMeasure α) c) : Set α → ℝ) i }.im
⊢ ((↑(c.singularPart μ) : Set α → ℂ) i + (↑(μ.withDensityᵥ (c.rnDeriv μ)) : Set α → ℂ) i).im =
    { re := (↑((re : (a : ComplexMeasure α) → SignedMeasure α) c) : Set α → ℝ) i,
        im := (↑((im : (a : ComplexMeasure α) → SignedMeasure α) c) : Set α → ℝ) i }.im
have rw : Integrable (ε := ℝ) (fun (x : α) ↦ (c.rnDeriv μ x).im) μ
Tactic: rw [Complex.add_im, withDensityᵥ_apply (c.integrable_rnDeriv μ) hi, ← RCLike.im_eq_complex_im,
      ← integral_im (c.integrable_rnDeriv μ).integrableOn, RCLike.im_eq_complex_im,
      ← withDensityᵥ_apply _ hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ (↑(SignedMeasure.singularPart ((im : (a : ComplexMeasure α) → SignedMeasure α) c) μ +
            μ.withDensityᵥ (SignedMeasure.rnDeriv ((im : (a : ComplexMeasure α) → SignedMeasure α) c) μ)) :
        Set α → ℝ)
      i =
    { re := (↑((re : (a : ComplexMeasure α) → SignedMeasure α) c) : Set α → ℝ) i,
        im := (↑((im : (a : ComplexMeasure α) → SignedMeasure α) c) : Set α → ℝ) i }.im
have h : (↑((im : (a : ComplexMeasure α) → SignedMeasure α) c) : Set α → ℝ) i =
  { re := (↑((re : (a : ComplexMeasure α) → SignedMeasure α) c) : Set α → ℝ) i,
      im := (↑((im : (a : ComplexMeasure α) → SignedMeasure α) c) : Set α → ℝ) i : ℂ }.im
Tactic: rw [c.im.singularPart_add_withDensity_rnDeriv_eq μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : SigmaFinite μ
h : s ≪ᵥ μ.toENNRealVectorMeasure
⊢ μ.withDensityᵥ (s.rnDeriv μ) = s
have rw : ∀ (h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ), μ.withDensityᵥ (s.rnDeriv μ) = s
Tactic: rw [absolutelyContinuous_ennreal_iff, (_ : μ.toENNRealVectorMeasure.ennrealToMeasure = μ),
    totalVariation_absolutelyContinuous_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : SigmaFinite μ
h : s ≪ᵥ μ.toENNRealVectorMeasure
rw : ∀ (h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ), μ.withDensityᵥ (s.rnDeriv μ) = s
⊢ μ.withDensityᵥ (s.rnDeriv μ) = s
have rw₁ : ∀ (h : s.totalVariation ≪ μ.toENNRealVectorMeasure.ennrealToMeasure), μ.toENNRealVectorMeasure.ennrealToMeasure = μ
Tactic: rw [absolutelyContinuous_ennreal_iff, (_ : μ.toENNRealVectorMeasure.ennrealToMeasure = μ),
    totalVariation_absolutelyContinuous_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
⊢ μ.withDensityᵥ (s.rnDeriv μ) = s
have h₁ : ∀ (i : Set α) (hi : MeasurableSet i), (↑(μ.withDensityᵥ (s.rnDeriv μ)) : Set α → ℝ) i = (↑s : Set α → ℝ) i
Tactic: ext1 i hi
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ (↑(μ.withDensityᵥ (s.rnDeriv μ)) : Set α → ℝ) i = (↑s : Set α → ℝ) i
have h₁ : s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i = (↑s : Set α → ℝ) i
Tactic: rw [withDensityᵥ_apply (integrable_rnDeriv _ _) hi, rnDeriv_def, integral_sub,
      setIntegral_toReal_rnDeriv h.1 i, setIntegral_toReal_rnDeriv h.2 i]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
h₁ : s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i = (↑s : Set α → ℝ) i
⊢ (↑(μ.withDensityᵥ (s.rnDeriv μ)) : Set α → ℝ) i = (↑s : Set α → ℝ) i
have h₂ : Integrable (ε := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal) (μ.restrict i)
Tactic: rw [withDensityᵥ_apply (integrable_rnDeriv _ _) hi, rnDeriv_def, integral_sub,
      setIntegral_toReal_rnDeriv h.1 i, setIntegral_toReal_rnDeriv h.2 i]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
h₁ : s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i = (↑s : Set α → ℝ) i
h₂ : Integrable (ε := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal) (μ.restrict i)
⊢ (↑(μ.withDensityᵥ (s.rnDeriv μ)) : Set α → ℝ) i = (↑s : Set α → ℝ) i
have h₃ : Integrable (ε := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal) (μ.restrict i)
Tactic: rw [withDensityᵥ_apply (integrable_rnDeriv _ _) hi, rnDeriv_def, integral_sub,
      setIntegral_toReal_rnDeriv h.1 i, setIntegral_toReal_rnDeriv h.2 i]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
| (↑s : Set α → ℝ) i
have rw : (↑s.toJordanDecomposition.toSignedMeasure : Set α → ℝ) i
Tactic: rw [← s.toSignedMeasure_toJordanDecomposition]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i = (↑s : Set α → ℝ) i
have h₁ : s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i =
  (↑s.toJordanDecomposition.toSignedMeasure : Set α → ℝ) i
Tactic: conv_rhs => rw [← s.toSignedMeasure_toJordanDecomposition]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i =
    (↑s.toJordanDecomposition.toSignedMeasure : Set α → ℝ) i
have h₁ : s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i =
  (↑(s.toJordanDecomposition.posPart.toSignedMeasure - s.toJordanDecomposition.negPart.toSignedMeasure) : Set α → ℝ) i
Tactic: rw [JordanDecomposition.toSignedMeasure, VectorMeasure.sub_apply,
        toSignedMeasure_apply_measurable hi, toSignedMeasure_apply_measurable hi, measureReal_def,
        measureReal_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
h₁ :
  s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i =
    (↑(s.toJordanDecomposition.posPart.toSignedMeasure - s.toJordanDecomposition.negPart.toSignedMeasure) : Set α → ℝ) i
⊢ s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i =
    (↑s.toJordanDecomposition.toSignedMeasure : Set α → ℝ) i
have h₂ : s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i =
  (↑s.toJordanDecomposition.posPart.toSignedMeasure : Set α → ℝ) i -
    (↑s.toJordanDecomposition.negPart.toSignedMeasure : Set α → ℝ) i
Tactic: rw [JordanDecomposition.toSignedMeasure, VectorMeasure.sub_apply,
        toSignedMeasure_apply_measurable hi, toSignedMeasure_apply_measurable hi, measureReal_def,
        measureReal_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
h₁ :
  s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i =
    (↑(s.toJordanDecomposition.posPart.toSignedMeasure - s.toJordanDecomposition.negPart.toSignedMeasure) : Set α → ℝ) i
h₂ :
  s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i =
    (↑s.toJordanDecomposition.posPart.toSignedMeasure : Set α → ℝ) i -
      (↑s.toJordanDecomposition.negPart.toSignedMeasure : Set α → ℝ) i
⊢ s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i =
    (↑s.toJordanDecomposition.toSignedMeasure : Set α → ℝ) i
have h₃ : s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i =
  s.toJordanDecomposition.posPart.real i - (↑s.toJordanDecomposition.negPart.toSignedMeasure : Set α → ℝ) i
Tactic: rw [JordanDecomposition.toSignedMeasure, VectorMeasure.sub_apply,
        toSignedMeasure_apply_measurable hi, toSignedMeasure_apply_measurable hi, measureReal_def,
        measureReal_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
h₁ :
  s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i =
    (↑(s.toJordanDecomposition.posPart.toSignedMeasure - s.toJordanDecomposition.negPart.toSignedMeasure) : Set α → ℝ) i
h₂ :
  s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i =
    (↑s.toJordanDecomposition.posPart.toSignedMeasure : Set α → ℝ) i -
      (↑s.toJordanDecomposition.negPart.toSignedMeasure : Set α → ℝ) i
h₃ :
  s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i =
    s.toJordanDecomposition.posPart.real i - (↑s.toJordanDecomposition.negPart.toSignedMeasure : Set α → ℝ) i
⊢ s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i =
    (↑s.toJordanDecomposition.toSignedMeasure : Set α → ℝ) i
have h₄ : s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i =
  s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i
Tactic: rw [JordanDecomposition.toSignedMeasure, VectorMeasure.sub_apply,
        toSignedMeasure_apply_measurable hi, toSignedMeasure_apply_measurable hi, measureReal_def,
        measureReal_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
h₁ :
  s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i =
    (↑(s.toJordanDecomposition.posPart.toSignedMeasure - s.toJordanDecomposition.negPart.toSignedMeasure) : Set α → ℝ) i
h₂ :
  s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i =
    (↑s.toJordanDecomposition.posPart.toSignedMeasure : Set α → ℝ) i -
      (↑s.toJordanDecomposition.negPart.toSignedMeasure : Set α → ℝ) i
h₃ :
  s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i =
    s.toJordanDecomposition.posPart.real i - (↑s.toJordanDecomposition.negPart.toSignedMeasure : Set α → ℝ) i
h₄ :
  s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i =
    s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i
⊢ s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i =
    (↑s.toJordanDecomposition.toSignedMeasure : Set α → ℝ) i
have h₅ : ENNReal.toReal ((s.toJordanDecomposition.posPart : (a : Set α) → ENNReal) i) - s.toJordanDecomposition.negPart.real i =
  ENNReal.toReal ((s.toJordanDecomposition.posPart : (a : Set α) → ENNReal) i) - s.toJordanDecomposition.negPart.real i
Tactic: rw [JordanDecomposition.toSignedMeasure, VectorMeasure.sub_apply,
        toSignedMeasure_apply_measurable hi, toSignedMeasure_apply_measurable hi, measureReal_def,
        measureReal_def]