awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
hfneg : Measurable (β := ℝ≥0∞) fun (x : α) ↦ ENNReal.ofReal (-f x)
e_a e_a₁ :
  { posPart := t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x),
        negPart := t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x),
        posPart_finite := ⋯, negPart_finite := ⋯, mutuallySingular := ⋯ : JordanDecomposition α }.negPart =
    t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)
⊢ s.toJordanDecomposition.negPart = t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)

Tactic:
rw [toJordanDecomposition_eq_of_eq_add_withDensity hf hfi htμ' hadd]

Premises used: MeasureTheory.SignedMeasure.toJordanDecomposition_eq_of_eq_add_withDensity
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
pos : ∀ (hfi : Integrable f μ), t = s.singularPart μ
neg : ∀ (hfi : ¬Integrable f μ), t = s.singularPart μ
⊢ t = s.singularPart μ

Tactic:
by_cases hfi : Integrable f μ

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

Tactic:
eq_singularPart' t hfi.1.measurable_mk (hfi.congr hfi.1.ae_eq_mk) htμ ?_

Premises used: MeasureTheory.AEStronglyMeasurable.ae_eq_mk, And.left, MeasureTheory.Integrable.congr, _private.0.MeasureTheory.SignedMeasure.eq_singularPart', MeasureTheory.AEStronglyMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
hfi : Integrable f μ
pos : s = t + μ.withDensityᵥ (AEStronglyMeasurable.mk f ⋯)
⊢ t = s.singularPart μ

Tactic:
refine eq_singularPart' t hfi.1.measurable_mk (hfi.congr hfi.1.ae_eq_mk) htμ ?_

Premises used: MeasureTheory.AEStronglyMeasurable.ae_eq_mk, And.left, MeasureTheory.Integrable.congr, _private.0.MeasureTheory.SignedMeasure.eq_singularPart', MeasureTheory.AEStronglyMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
hfi : Integrable f μ
⊢ s = t + μ.withDensityᵥ f

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

Tactic:
convert! hadd using 2
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
hfi : Integrable f μ
⊢ μ.withDensityᵥ (AEStronglyMeasurable.mk 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 : α → ℝ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
hfi : Integrable f μ
⊢ μ.withDensityᵥ (AEStronglyMeasurable.mk 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 : α → ℝ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
hfi : ¬Integrable f μ
⊢ s = t

Tactic:
rw [withDensityᵥ, dif_neg hfi, add_zero] at hadd

Premises used: MeasureTheory.Measure.withDensityᵥ, dif_neg, add_zero
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
hfi : ¬Integrable f μ
hadd₁ : s = t
⊢ ¬Integrable f μ

Tactic:
rw [withDensityᵥ, dif_neg hfi, add_zero] at hadd

Premises used: MeasureTheory.Measure.withDensityᵥ, dif_neg, add_zero
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t
hfi : ¬Integrable f μ
⊢ t = s.singularPart μ

Tactic:
eq_singularPart' t measurable_zero (integrable_zero _ _ μ) htμ ?_

Premises used: MeasureTheory.integrable_zero, measurable_zero, _private.0.MeasureTheory.SignedMeasure.eq_singularPart'
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t
hfi : ¬Integrable f μ
neg : s = t + μ.withDensityᵥ 0
⊢ t = s.singularPart μ

Tactic:
refine eq_singularPart' t measurable_zero (integrable_zero _ _ μ) htμ ?_

Premises used: MeasureTheory.integrable_zero, measurable_zero, _private.0.MeasureTheory.SignedMeasure.eq_singularPart'
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t
hfi : ¬Integrable f μ
neg : s = t + 0
neg₁ neg₂ neg₃ neg₄ : s = t
⊢ s = t + μ.withDensityᵥ 0

Tactic:
rwa [withDensityᵥ_zero, add_zero]

Premises used: MeasureTheory.withDensityᵥ_zero, add_zero
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
⊢ singularPart 0 μ = 0

Tactic:
(eq_singularPart 0 0 VectorMeasure.MutuallySingular.zero_left ?_).symm

Premises used: MeasureTheory.VectorMeasure.MutuallySingular.zero_left, MeasureTheory.SignedMeasure.eq_singularPart, OfNat.ofNat, Eq.symm
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
refine : 0 = HAdd.hAdd (α := SignedMeasure α) 0 (μ.withDensityᵥ 0)
⊢ singularPart 0 μ = 0

Tactic:
refine (eq_singularPart 0 0 VectorMeasure.MutuallySingular.zero_left ?_).symm

Premises used: MeasureTheory.VectorMeasure.MutuallySingular.zero_left, MeasureTheory.SignedMeasure.eq_singularPart, OfNat.ofNat, Eq.symm
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
rw : Eq (α := SignedMeasure α) 0 (μ.withDensityᵥ 0)
rw₁ rw₂ : Eq.{u_1 + 1} (α := SignedMeasure α) 0 0
⊢ 0 = HAdd.hAdd (α := SignedMeasure α) 0 (μ.withDensityᵥ 0)

Tactic:
rw [zero_add, withDensityᵥ_zero]

Premises used: zero_add, MeasureTheory.withDensityᵥ_zero
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ (-s).singularPart μ = -s.singularPart μ

Tactic:
simp [singularPart, toJordanDecomposition_neg]

Premises used: MeasureTheory.SignedMeasure.toJordanDecomposition_neg, MeasureTheory.SignedMeasure.singularPart
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
rw :
  ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
    (r • s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      (r • s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
⊢ (r • s).singularPart μ = r • s.singularPart μ

Tactic:
rw [singularPart, singularPart, smul_sub, ← toSignedMeasure_smul, ← toSignedMeasure_smul]

Premises used: MeasureTheory.Measure.toSignedMeasure_smul, smul_sub, MeasureTheory.SignedMeasure.singularPart
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
a : ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure
a₁ : ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
| ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
    ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure

Tactic:
congr
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
a : (r • s).toJordanDecomposition.posPart.singularPart μ
| ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure

Tactic:
congr
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
a : r • s.toJordanDecomposition.posPart.singularPart μ
| (r • s).toJordanDecomposition.posPart.singularPart μ

Tactic:
rw [toJordanDecomposition_smul, JordanDecomposition.smul_posPart, singularPart_smul]

Premises used: MeasureTheory.JordanDecomposition.smul_posPart, MeasureTheory.SignedMeasure.toJordanDecomposition_smul, MeasureTheory.Measure.singularPart_smul
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
a : (r • s.toJordanDecomposition).posPart.singularPart μ
a₁ : (r • s.toJordanDecomposition.posPart).singularPart μ
a₂ : r • s.toJordanDecomposition.posPart.singularPart μ
| (r • s).toJordanDecomposition.posPart.singularPart μ

Tactic:
· rw [toJordanDecomposition_smul, JordanDecomposition.smul_posPart, singularPart_smul]

Premises used: MeasureTheory.JordanDecomposition.smul_posPart, MeasureTheory.SignedMeasure.toJordanDecomposition_smul, MeasureTheory.Measure.singularPart_smul
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
a : (r • s).toJordanDecomposition.posPart.singularPart μ
| ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure

Tactic:
congr
      · rw [toJordanDecomposition_smul, JordanDecomposition.smul_posPart, singularPart_smul]

Premises used: MeasureTheory.JordanDecomposition.smul_posPart, MeasureTheory.SignedMeasure.toJordanDecomposition_smul, MeasureTheory.Measure.singularPart_smul
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
| ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure

Tactic:
· congr
      · rw [toJordanDecomposition_smul, JordanDecomposition.smul_posPart, singularPart_smul]

Premises used: MeasureTheory.JordanDecomposition.smul_posPart, MeasureTheory.SignedMeasure.toJordanDecomposition_smul, MeasureTheory.Measure.singularPart_smul
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
a : (r • s).toJordanDecomposition.negPart.singularPart μ
| ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure

Tactic:
congr
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
a : r • s.toJordanDecomposition.negPart.singularPart μ
| (r • s).toJordanDecomposition.negPart.singularPart μ

Tactic:
rw [toJordanDecomposition_smul, JordanDecomposition.smul_negPart, singularPart_smul]

Premises used: MeasureTheory.JordanDecomposition.smul_negPart, MeasureTheory.SignedMeasure.toJordanDecomposition_smul, MeasureTheory.Measure.singularPart_smul
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
a : r • s.toJordanDecomposition.negPart.singularPart μ
| ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure

Tactic:
congr
      rw [toJordanDecomposition_smul, JordanDecomposition.smul_negPart, singularPart_smul]

Premises used: MeasureTheory.JordanDecomposition.smul_negPart, MeasureTheory.SignedMeasure.toJordanDecomposition_smul, MeasureTheory.Measure.singularPart_smul
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
a : (r • s).toJordanDecomposition.negPart.singularPart μ
a₁ : r • s.toJordanDecomposition.negPart.singularPart μ
| ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure

Tactic:
· congr
      rw [toJordanDecomposition_smul, JordanDecomposition.smul_negPart, singularPart_smul]

Premises used: MeasureTheory.JordanDecomposition.smul_negPart, MeasureTheory.SignedMeasure.toJordanDecomposition_smul, MeasureTheory.Measure.singularPart_smul
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
a : ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure
a₁ a₂ : ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
| ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
    ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure

Tactic:
congr
    · congr
      · rw [toJordanDecomposition_smul, JordanDecomposition.smul_posPart, singularPart_smul]
    · congr
      rw [toJordanDecomposition_smul, JordanDecomposition.smul_negPart, singularPart_smul]

Premises used: MeasureTheory.JordanDecomposition.smul_posPart, MeasureTheory.JordanDecomposition.smul_negPart, MeasureTheory.SignedMeasure.toJordanDecomposition_smul, MeasureTheory.Measure.singularPart_smul
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
conv_lhs :
  ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
    (r • s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      (r • s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
conv_lhs₁ :
  (r • s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      (r • s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
    (r • s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      (r • s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
⊢ ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
    (r • s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      (r • s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure

Tactic:
conv_lhs =>
    congr
    · congr
      · rw [toJordanDecomposition_smul, JordanDecomposition.smul_posPart, singularPart_smul]
    · congr
      rw [toJordanDecomposition_smul, JordanDecomposition.smul_negPart, singularPart_smul]

Premises used: MeasureTheory.JordanDecomposition.smul_posPart, MeasureTheory.JordanDecomposition.smul_negPart, MeasureTheory.SignedMeasure.toJordanDecomposition_smul, MeasureTheory.Measure.singularPart_smul
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ r

Tactic:
hr
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : 0 ≤ r
inl : ∀ (r : ℝ≥0), ((↑r : ℝ) • s).singularPart μ = (↑r : ℝ) • s.singularPart μ
⊢ (r • s).singularPart μ = r • s.singularPart μ

Tactic:
lift r to ℝ≥0 using hr
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
⊢ ((↑r : ℝ) • s).singularPart μ = (↑r : ℝ) • s.singularPart μ

Tactic:
singularPart_smul_nnreal s μ r

Premises used: MeasureTheory.SignedMeasure.singularPart_smul_nnreal
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
⊢ ((↑r : ℝ) • s).singularPart μ = (↑r : ℝ) • s.singularPart μ

Tactic:
exact singularPart_smul_nnreal s μ r

Premises used: MeasureTheory.SignedMeasure.singularPart_smul_nnreal
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
a : ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure
a₁ : ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
| ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
    ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure

Tactic:
congr
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
a : (r • s).toJordanDecomposition.posPart.singularPart μ
| ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure

Tactic:
congr
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
a : (-r).toNNReal • s.toJordanDecomposition.negPart.singularPart μ
| (r • s).toJordanDecomposition.posPart.singularPart μ

Tactic:
rw [toJordanDecomposition_smul_real,
            JordanDecomposition.real_smul_posPart_neg _ _ hr, singularPart_smul]

Premises used: MeasureTheory.SignedMeasure.singularPart_smul, MeasureTheory.SignedMeasure.toJordanDecomposition_smul_real, MeasureTheory.JordanDecomposition.real_smul_posPart_neg
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
a : (r • s.toJordanDecomposition).posPart.singularPart μ
a₁ : ((-r).toNNReal • s.toJordanDecomposition.negPart).singularPart μ
a₂ : (-r).toNNReal • s.toJordanDecomposition.negPart.singularPart μ
| (r • s).toJordanDecomposition.posPart.singularPart μ

Tactic:
· rw [toJordanDecomposition_smul_real,
            JordanDecomposition.real_smul_posPart_neg _ _ hr, singularPart_smul]

Premises used: MeasureTheory.SignedMeasure.singularPart_smul, MeasureTheory.SignedMeasure.toJordanDecomposition_smul_real, MeasureTheory.JordanDecomposition.real_smul_posPart_neg
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
a : (r • s).toJordanDecomposition.posPart.singularPart μ
| ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure

Tactic:
congr
        · rw [toJordanDecomposition_smul_real,
            JordanDecomposition.real_smul_posPart_neg _ _ hr, singularPart_smul]

Premises used: MeasureTheory.SignedMeasure.singularPart_smul, MeasureTheory.SignedMeasure.toJordanDecomposition_smul_real, MeasureTheory.JordanDecomposition.real_smul_posPart_neg
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
| ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure

Tactic:
· congr
        · rw [toJordanDecomposition_smul_real,
            JordanDecomposition.real_smul_posPart_neg _ _ hr, singularPart_smul]

Premises used: MeasureTheory.SignedMeasure.singularPart_smul, MeasureTheory.SignedMeasure.toJordanDecomposition_smul_real, MeasureTheory.JordanDecomposition.real_smul_posPart_neg
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
a : (r • s).toJordanDecomposition.negPart.singularPart μ
| ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure

Tactic:
congr
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
a : (-r).toNNReal • s.toJordanDecomposition.posPart.singularPart μ
| (r • s).toJordanDecomposition.negPart.singularPart μ

Tactic:
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_negPart_neg
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
a : (r • s.toJordanDecomposition).negPart.singularPart μ
a₁ : ((-r).toNNReal • s.toJordanDecomposition.posPart).singularPart μ
a₂ : (-r).toNNReal • s.toJordanDecomposition.posPart.singularPart μ
| (r • s).toJordanDecomposition.negPart.singularPart μ

Tactic:
· 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_negPart_neg
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
a : (r • s).toJordanDecomposition.negPart.singularPart μ
| ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure

Tactic:
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_negPart_neg
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
a : (r • s).toJordanDecomposition.negPart.singularPart μ
| ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure

Tactic:
· 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_negPart_neg
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
a : ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure
a₁ a₂ : ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
| ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
    ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure

Tactic:
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