awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
inr :
  ((-r).toNNReal • s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure -
      ((-r).toNNReal • s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure =
    r •
      ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure)
⊢ ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
    r •
      ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure)

Tactic:
conv_lhs =>
      congr
      · congr
        · rw [toJordanDecomposition_smul_real,
            JordanDecomposition.real_smul_posPart_neg _ _ hr, singularPart_smul]
      · congr
        · rw [toJordanDecomposition_smul_real,
            JordanDecomposition.real_smul_negPart_neg _ _ hr, singularPart_smul]

Premises used: MeasureTheory.SignedMeasure.singularPart_smul, MeasureTheory.SignedMeasure.toJordanDecomposition_smul_real, MeasureTheory.JordanDecomposition.real_smul_posPart_neg, MeasureTheory.JordanDecomposition.real_smul_negPart_neg
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
⊢ 0 ≤ r ∨ r < 0

Tactic:
cases le_or_gt 0 r with
  | inl hr =>
    lift r to ℝ≥0 using hr
    exact singularPart_smul_nnreal s μ r
  | inr hr =>
    rw [singularPart, singularPart]
    conv_lhs =>
      congr
      · congr
        · rw [toJordanDecomposition_smul_real,
            JordanDecomposition.real_smul_posPart_neg _ _ hr, singularPart_smul]
      · congr
        · rw [toJordanDecomposition_smul_real,
            JordanDecomposition.real_smul_negPart_neg _ _ hr, singularPart_smul]
    rw [toSignedMeasure_smul, toSignedMeasure_smul, ← neg_sub, ← smul_sub, NNReal.smul_def,
      ← neg_smul, Real.coe_toNNReal _ (le_of_lt (neg_pos.mpr hr)), neg_neg]

Premises used: neg_smul, neg_sub, MeasureTheory.SignedMeasure.singularPart_smul, MeasureTheory.SignedMeasure.toJordanDecomposition_smul_real, neg_neg, MeasureTheory.Measure.toSignedMeasure_smul, smul_sub, NNReal.smul_def, le_or_gt, MeasureTheory.SignedMeasure.singularPart, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
inst_1 : t.HaveLebesgueDecomposition μ
⊢ (s + t).singularPart μ = s.singularPart μ + t.singularPart μ

Tactic:
(eq_singularPart _ (s.rnDeriv μ + t.rnDeriv μ)
        ((mutuallySingular_singularPart s μ).add_left (mutuallySingular_singularPart t μ))
        ?_).symm

Premises used: MeasureTheory.SignedMeasure.mutuallySingular_singularPart, MeasureTheory.SignedMeasure.rnDeriv, MeasureTheory.SignedMeasure.eq_singularPart, HAdd.hAdd, MeasureTheory.VectorMeasure.MutuallySingular.add_left, Eq.symm
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
inst_1 : t.HaveLebesgueDecomposition μ
_ : s + t = s.singularPart μ + t.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
⊢ (s + t).singularPart μ = s.singularPart μ + t.singularPart μ

Tactic:
refine
    (eq_singularPart _ (s.rnDeriv μ + t.rnDeriv μ)
        ((mutuallySingular_singularPart s μ).add_left (mutuallySingular_singularPart t μ))
        ?_).symm

Premises used: MeasureTheory.SignedMeasure.mutuallySingular_singularPart, MeasureTheory.SignedMeasure.rnDeriv, MeasureTheory.SignedMeasure.eq_singularPart, HAdd.hAdd, MeasureTheory.VectorMeasure.MutuallySingular.add_left, Eq.symm
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
inst_1 : t.HaveLebesgueDecomposition μ
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
rw₇ rw₈ : s + t = s + t
⊢ s + t = s.singularPart μ + t.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)

Tactic:
rw [withDensityᵥ_add (integrable_rnDeriv s μ) (integrable_rnDeriv t μ), add_assoc,
    add_comm (t.singularPart μ), add_assoc, add_comm _ (t.singularPart μ),
    singularPart_add_withDensity_rnDeriv_eq, ← add_assoc,
    singularPart_add_withDensity_rnDeriv_eq]

Premises used: add_assoc, add_comm, MeasureTheory.withDensityᵥ_add, MeasureTheory.SignedMeasure.singularPart_add_withDensity_rnDeriv_eq, MeasureTheory.SignedMeasure.integrable_rnDeriv, MeasureTheory.SignedMeasure.singularPart
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
inst_1 : t.HaveLebesgueDecomposition μ
rw : (s + -t).singularPart μ = s.singularPart μ - t.singularPart μ
rw₁ : (s + -t).singularPart μ = s.singularPart μ + -t.singularPart μ
rw₂ : s.singularPart μ + (-t).singularPart μ = s.singularPart μ + -t.singularPart μ
rw₃ rw₄ : s.singularPart μ + -t.singularPart μ = s.singularPart μ + -t.singularPart μ
⊢ (s - t).singularPart μ = s.singularPart μ - t.singularPart μ

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, singularPart_add, singularPart_neg]

Premises used: sub_eq_add_neg, MeasureTheory.SignedMeasure.singularPart_add, MeasureTheory.SignedMeasure.singularPart_neg
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
f' : α → ℝ := AEStronglyMeasurable.mk f ⋯
⊢ s = t + μ.withDensityᵥ f

Tactic:
hadd
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
f' : α → ℝ := AEStronglyMeasurable.mk f ⋯
h : μ.withDensityᵥ f' = μ.withDensityᵥ f
⊢ s = t + μ.withDensityᵥ f'

Tactic:
convert! hadd using 2
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
f' : α → ℝ := AEStronglyMeasurable.mk f ⋯
⊢ μ.withDensityᵥ f' = μ.withDensityᵥ f

Tactic:
WithDensityᵥEq.congr_ae hfi.1.ae_eq_mk.symm

Premises used: MeasureTheory.AEStronglyMeasurable.ae_eq_mk, And.left, MeasureTheory.WithDensityᵥEq.congr_ae, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
f' : α → ℝ := AEStronglyMeasurable.mk f ⋯
⊢ μ.withDensityᵥ f' = μ.withDensityᵥ f

Tactic:
exact WithDensityᵥEq.congr_ae hfi.1.ae_eq_mk.symm

Premises used: MeasureTheory.AEStronglyMeasurable.ae_eq_mk, And.left, MeasureTheory.WithDensityᵥEq.congr_ae, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
f' : α → ℝ := AEStronglyMeasurable.mk f ⋯
⊢ s = t + μ.withDensityᵥ f'

Tactic:
have hadd' : s = t + μ.withDensityᵥ f' := by
    convert! hadd using 2
    exact WithDensityᵥEq.congr_ae hfi.1.ae_eq_mk.symm
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
f' : α → ℝ := AEStronglyMeasurable.mk f ⋯
hadd' : s = t + μ.withDensityᵥ f'
⊢ s.HaveLebesgueDecomposition μ

Tactic:
have := haveLebesgueDecomposition_mk μ hfi.1.measurable_mk htμ hadd'
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
f' : α → ℝ := AEStronglyMeasurable.mk f ⋯
hadd' : s = t + μ.withDensityᵥ f'
this : s.HaveLebesgueDecomposition μ
⊢ f =ᶠ[ae μ] s.rnDeriv μ

Tactic:
(Integrable.ae_eq_of_withDensityᵥ_eq (integrable_rnDeriv _ _) hfi ?_).symm

Premises used: MeasureTheory.Integrable.ae_eq_of_withDensityᵥ_eq, MeasureTheory.SignedMeasure.integrable_rnDeriv, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
f' : α → ℝ := AEStronglyMeasurable.mk f ⋯
hadd' : s = t + μ.withDensityᵥ f'
this : s.HaveLebesgueDecomposition μ
refine : μ.withDensityᵥ (s.rnDeriv μ) = μ.withDensityᵥ f
⊢ f =ᶠ[ae μ] s.rnDeriv μ

Tactic:
refine (Integrable.ae_eq_of_withDensityᵥ_eq (integrable_rnDeriv _ _) hfi ?_).symm

Premises used: MeasureTheory.Integrable.ae_eq_of_withDensityᵥ_eq, MeasureTheory.SignedMeasure.integrable_rnDeriv, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
f' : α → ℝ := AEStronglyMeasurable.mk f ⋯
hadd' : s = t + μ.withDensityᵥ f'
this : s.HaveLebesgueDecomposition μ
rw : t + μ.withDensityᵥ (s.rnDeriv μ) = t + μ.withDensityᵥ f
rw₁ : t + μ.withDensityᵥ (s.rnDeriv μ) = s
rw₂ : s.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ) = s
rw₃ rw₄ : s = s
⊢ μ.withDensityᵥ (s.rnDeriv μ) = μ.withDensityᵥ f

Tactic:
rw [← add_right_inj t, ← hadd, eq_singularPart _ f htμ hadd,
    singularPart_add_withDensity_rnDeriv_eq]

Premises used: MeasureTheory.SignedMeasure.eq_singularPart, MeasureTheory.SignedMeasure.singularPart_add_withDensity_rnDeriv_eq, add_right_inj
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
⊢ (-s).rnDeriv μ =ᶠ[ae μ] -s.rnDeriv μ

Tactic:
Integrable.ae_eq_of_withDensityᵥ_eq (integrable_rnDeriv _ _) (integrable_rnDeriv _ _).neg ?_

Premises used: MeasureTheory.Integrable.neg, MeasureTheory.Integrable.ae_eq_of_withDensityᵥ_eq, MeasureTheory.SignedMeasure.integrable_rnDeriv
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
_ : μ.withDensityᵥ ((-s).rnDeriv μ) = μ.withDensityᵥ (-s.rnDeriv μ)
⊢ (-s).rnDeriv μ =ᶠ[ae μ] -s.rnDeriv μ

Tactic:
refine
    Integrable.ae_eq_of_withDensityᵥ_eq (integrable_rnDeriv _ _) (integrable_rnDeriv _ _).neg ?_

Premises used: MeasureTheory.Integrable.neg, MeasureTheory.Integrable.ae_eq_of_withDensityᵥ_eq, MeasureTheory.SignedMeasure.integrable_rnDeriv
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
rw : μ.withDensityᵥ ((-s).rnDeriv μ) = -μ.withDensityᵥ (s.rnDeriv μ)
rw₁ : (-s).singularPart μ + μ.withDensityᵥ ((-s).rnDeriv μ) = (-s).singularPart μ + -μ.withDensityᵥ (s.rnDeriv μ)
rw₂ : -s = (-s).singularPart μ + -μ.withDensityᵥ (s.rnDeriv μ)
rw₃ : -s = -s.singularPart μ + -μ.withDensityᵥ (s.rnDeriv μ)
rw₄ : -s = -(s.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ))
rw₅ rw₆ : -s = -s
⊢ μ.withDensityᵥ ((-s).rnDeriv μ) = μ.withDensityᵥ (-s.rnDeriv μ)

Tactic:
rw [withDensityᵥ_neg, ← add_right_inj ((-s).singularPart μ),
    singularPart_add_withDensity_rnDeriv_eq, singularPart_neg, ← neg_add,
    singularPart_add_withDensity_rnDeriv_eq]

Premises used: neg_add, MeasureTheory.SignedMeasure.singularPart_neg, MeasureTheory.withDensityᵥ_neg, MeasureTheory.SignedMeasure.singularPart_add_withDensity_rnDeriv_eq, MeasureTheory.SignedMeasure.singularPart, add_right_inj, Neg.neg
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
r : ℝ
⊢ (r • s).rnDeriv μ =ᶠ[ae μ] r • s.rnDeriv μ

Tactic:
Integrable.ae_eq_of_withDensityᵥ_eq (integrable_rnDeriv _ _)
      ((integrable_rnDeriv _ _).smul r) ?_

Premises used: MeasureTheory.Integrable.smul, MeasureTheory.Integrable.ae_eq_of_withDensityᵥ_eq, MeasureTheory.SignedMeasure.integrable_rnDeriv
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
r : ℝ
_ : μ.withDensityᵥ ((r • s).rnDeriv μ) = μ.withDensityᵥ (r • s.rnDeriv μ)
⊢ (r • s).rnDeriv μ =ᶠ[ae μ] r • s.rnDeriv μ

Tactic:
refine
    Integrable.ae_eq_of_withDensityᵥ_eq (integrable_rnDeriv _ _)
      ((integrable_rnDeriv _ _).smul r) ?_

Premises used: MeasureTheory.Integrable.smul, MeasureTheory.Integrable.ae_eq_of_withDensityᵥ_eq, MeasureTheory.SignedMeasure.integrable_rnDeriv
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
r : ℝ
rw : μ.withDensityᵥ ((r • s).rnDeriv μ) = HSMul.hSMul (β := VectorMeasure α ℝ) r (μ.withDensityᵥ (s.rnDeriv μ))
rw₁ :
  (r • s).singularPart μ + μ.withDensityᵥ ((r • s).rnDeriv μ) =
    (r • s).singularPart μ + HSMul.hSMul (β := VectorMeasure α ℝ) r (μ.withDensityᵥ (s.rnDeriv μ))
rw₂ : r • s = (r • s).singularPart μ + HSMul.hSMul (β := VectorMeasure α ℝ) r (μ.withDensityᵥ (s.rnDeriv μ))
rw₃ : r • s = r • s.singularPart μ + HSMul.hSMul (β := VectorMeasure α ℝ) r (μ.withDensityᵥ (s.rnDeriv μ))
rw₄ : r • s = r • (s.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ))
rw₅ rw₆ : r • s = r • s
⊢ μ.withDensityᵥ ((r • s).rnDeriv μ) = μ.withDensityᵥ (r • s.rnDeriv μ)

Tactic:
rw [withDensityᵥ_smul (rnDeriv s μ) r, ← add_right_inj ((r • s).singularPart μ),
    singularPart_add_withDensity_rnDeriv_eq, singularPart_smul, ← smul_add,
    singularPart_add_withDensity_rnDeriv_eq]

Premises used: MeasureTheory.SignedMeasure.singularPart_smul, MeasureTheory.SignedMeasure.rnDeriv, MeasureTheory.SignedMeasure.singularPart_add_withDensity_rnDeriv_eq, MeasureTheory.withDensityᵥ_smul, HSMul.hSMul, MeasureTheory.SignedMeasure.singularPart, add_right_inj, smul_add
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
inst_1 : t.HaveLebesgueDecomposition μ
inst_2 : (s + t).HaveLebesgueDecomposition μ
⊢ (s + t).rnDeriv μ =ᶠ[ae μ] s.rnDeriv μ + t.rnDeriv μ

Tactic:
Integrable.ae_eq_of_withDensityᵥ_eq (integrable_rnDeriv _ _)
      ((integrable_rnDeriv _ _).add (integrable_rnDeriv _ _)) ?_

Premises used: MeasureTheory.Integrable.ae_eq_of_withDensityᵥ_eq, MeasureTheory.Integrable.add, MeasureTheory.SignedMeasure.integrable_rnDeriv
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
inst_1 : t.HaveLebesgueDecomposition μ
inst_2 : (s + t).HaveLebesgueDecomposition μ
_ : μ.withDensityᵥ ((s + t).rnDeriv μ) = μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
⊢ (s + t).rnDeriv μ =ᶠ[ae μ] s.rnDeriv μ + t.rnDeriv μ

Tactic:
refine
    Integrable.ae_eq_of_withDensityᵥ_eq (integrable_rnDeriv _ _)
      ((integrable_rnDeriv _ _).add (integrable_rnDeriv _ _)) ?_

Premises used: MeasureTheory.Integrable.ae_eq_of_withDensityᵥ_eq, MeasureTheory.Integrable.add, MeasureTheory.SignedMeasure.integrable_rnDeriv
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
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
rw₁₀ rw₁₁ : s + t = s + t
⊢ μ.withDensityᵥ ((s + t).rnDeriv μ) = μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)

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]

Premises used: add_assoc, MeasureTheory.SignedMeasure.singularPart_add, add_comm, HAdd.hAdd, MeasureTheory.withDensityᵥ_add, MeasureTheory.SignedMeasure.singularPart_add_withDensity_rnDeriv_eq, MeasureTheory.SignedMeasure.integrable_rnDeriv, MeasureTheory.SignedMeasure.singularPart, add_right_inj
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
inst_1 : t.HaveLebesgueDecomposition μ
hst : (s - t).HaveLebesgueDecomposition μ
⊢ (s + -t).HaveLebesgueDecomposition μ

Tactic:
rw [sub_eq_add_neg] at hst

Premises used: sub_eq_add_neg
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
inst_1 : t.HaveLebesgueDecomposition μ
hst : (s + -t).HaveLebesgueDecomposition μ
rw : (s + -t).rnDeriv μ =ᶠ[ae μ] s.rnDeriv μ + -t.rnDeriv μ
⊢ (s - t).rnDeriv μ =ᶠ[ae μ] s.rnDeriv μ - t.rnDeriv μ

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : Measure α
rw :
  MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.re : (a : ℂ) → ℝ) (c.rnDeriv μ x)) 1 μ ∧
    MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.im : (a : ℂ) → ℝ) (c.rnDeriv μ x)) 1 μ
⊢ Integrable (c.rnDeriv μ) μ

Tactic:
rw [← memLp_one_iff_integrable, ← memLp_re_im_iff]

Premises used: MeasureTheory.memLp_one_iff_integrable, MeasureTheory.memLp_re_im_iff
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : Measure α
⊢ MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.re : (a : ℂ) → ℝ) (c.rnDeriv μ x)) 1 μ ∧
    MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.im : (a : ℂ) → ℝ) (c.rnDeriv μ x)) 1 μ

Tactic:
⟨memLp_one_iff_integrable.2 (SignedMeasure.integrable_rnDeriv _ _),
      memLp_one_iff_integrable.2 (SignedMeasure.integrable_rnDeriv _ _)⟩

Premises used: Iff.mpr, And.intro, MeasureTheory.SignedMeasure.integrable_rnDeriv, MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst : c.HaveLebesgueDecomposition μ
rw :
  SignedMeasure.toComplexMeasure ((re : (a : ComplexMeasure α) → SignedMeasure α) c)
    ((im : (a : ComplexMeasure α) → SignedMeasure α) c)
| c

Tactic:
rw [← c.toComplexMeasure_to_signedMeasure]

Premises used: MeasureTheory.ComplexMeasure.toComplexMeasure_to_signedMeasure
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst : c.HaveLebesgueDecomposition μ
conv_rhs :
  c.singularPart μ + μ.withDensityᵥ (c.rnDeriv μ) =
    SignedMeasure.toComplexMeasure ((re : (a : ComplexMeasure α) → SignedMeasure α) c)
      ((im : (a : ComplexMeasure α) → SignedMeasure α) c)
⊢ c.singularPart μ + μ.withDensityᵥ (c.rnDeriv μ) = c

Tactic:
conv_rhs => rw [← c.toComplexMeasure_to_signedMeasure]

Premises used: MeasureTheory.ComplexMeasure.toComplexMeasure_to_signedMeasure
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst : c.HaveLebesgueDecomposition μ
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
⊢ c.singularPart μ + μ.withDensityᵥ (c.rnDeriv μ) =
    SignedMeasure.toComplexMeasure ((re : (a : ComplexMeasure α) → SignedMeasure α) c)
      ((im : (a : ComplexMeasure α) → SignedMeasure α) c)

Tactic:
ext i hi : 1
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
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
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
⊢ (↑(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 }

Tactic:
apply Complex.ext

Premises used: Complex.ext