-- Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean
theorem haveLebesgueDecomposition_mk' (μ : Measure α) {f : α → ℝ} (hf : Measurable f)
    (hfi : Integrable f μ) (htμ : t ⟂ᵥ μ.toENNRealVectorMeasure) (hadd : s = t + μ.withDensityᵥ f) :
    s.HaveLebesgueDecomposition μ

Proof state:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
htμ : t.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
⊢ s.toJordanDecomposition.negPart.HaveLebesgueDecomposition μ

Tactic:
use ⟨t.toJordanDecomposition.negPart, fun x => ENNReal.ofReal (-f x)⟩

Result:
case h
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
htμ : t.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
⊢ Measurable (t.toJordanDecomposition.negPart, fun x => ENNReal.ofReal (-f x)).2 ∧
    (t.toJordanDecomposition.negPart, fun x => ENNReal.ofReal (-f x)).1 ⟂ₘ μ ∧
      s.toJordanDecomposition.negPart =
        (t.toJordanDecomposition.negPart, fun x => ENNReal.ofReal (-f x)).1 +
          μ.withDensity (t.toJordanDecomposition.negPart, fun x => ENNReal.ofReal (-f x)).2

Proof state:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t.totalVariation ⟂ₘ μ.toENNRealVectorMeasure.ennrealToMeasure
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
⊢ s.HaveLebesgueDecomposition μ

Tactic:
change _ ⟂ₘ VectorMeasure.equivMeasure.toFun (VectorMeasure.equivMeasure.invFun μ) at htμ

Result:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
htμ : t.totalVariation ⟂ₘ VectorMeasure.equivMeasure.toFun (VectorMeasure.equivMeasure.invFun μ)
⊢ s.HaveLebesgueDecomposition μ

Proof state:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
htμ : t.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
⊢ s.toJordanDecomposition.posPart.HaveLebesgueDecomposition μ

Tactic:
use ⟨t.toJordanDecomposition.posPart, fun x => ENNReal.ofReal (f x)⟩

Result:
case h
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
htμ : t.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
⊢ Measurable (t.toJordanDecomposition.posPart, fun x => ENNReal.ofReal (f x)).2 ∧
    (t.toJordanDecomposition.posPart, fun x => ENNReal.ofReal (f x)).1 ⟂ₘ μ ∧
      s.toJordanDecomposition.posPart =
        (t.toJordanDecomposition.posPart, fun x => ENNReal.ofReal (f x)).1 +
          μ.withDensity (t.toJordanDecomposition.posPart, fun x => ENNReal.ofReal (f x)).2

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
htμ : t.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
⊢ Measurable (t.toJordanDecomposition.negPart, fun x => ENNReal.ofReal (-f x)).2 ∧
    (t.toJordanDecomposition.negPart, fun x => ENNReal.ofReal (-f x)).1 ⟂ₘ μ ∧
      s.toJordanDecomposition.negPart =
        (t.toJordanDecomposition.negPart, fun x => ENNReal.ofReal (-f x)).1 +
          μ.withDensity (t.toJordanDecomposition.negPart, fun x => ENNReal.ofReal (-f x)).2

Tactic:
refine ⟨hf.neg.ennreal_ofReal, htμ.2, ?_⟩

Result:
case h
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
htμ : t.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
⊢ s.toJordanDecomposition.negPart =
    (t.toJordanDecomposition.negPart, fun x => ENNReal.ofReal (-f x)).1 +
      μ.withDensity (t.toJordanDecomposition.negPart, fun x => ENNReal.ofReal (-f x)).2

Proof state:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
htμ : t.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
⊢ s.HaveLebesgueDecomposition μ

Tactic:
refine
  { posPart := by
      use ⟨t.toJordanDecomposition.posPart, fun x => ENNReal.ofReal (f x)⟩
      refine ⟨hf.ennreal_ofReal, htμ.1, ?_⟩
      rw [toJordanDecomposition_eq_of_eq_add_withDensity hf hfi htμ' hadd]
    negPart := by
      use ⟨t.toJordanDecomposition.negPart, fun x => ENNReal.ofReal (-f x)⟩
      refine ⟨hf.neg.ennreal_ofReal, htμ.2, ?_⟩
      rw [toJordanDecomposition_eq_of_eq_add_withDensity hf hfi htμ' hadd] }

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
⊢ s.HaveLebesgueDecomposition μ

Tactic:
have htμ' := htμ

Result:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
⊢ s.HaveLebesgueDecomposition μ

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
htμ : t.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
⊢ s.toJordanDecomposition.negPart =
    (t.toJordanDecomposition.negPart, fun x => ENNReal.ofReal (-f x)).1 +
      μ.withDensity (t.toJordanDecomposition.negPart, fun x => ENNReal.ofReal (-f x)).2

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

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
htμ : t.totalVariation ⟂ₘ VectorMeasure.equivMeasure.toFun (VectorMeasure.equivMeasure.invFun μ)
⊢ s.HaveLebesgueDecomposition μ

Tactic:
rw [VectorMeasure.equivMeasure.right_inv, totalVariation_mutuallySingular_iff] at htμ

Result:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
htμ : t.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
⊢ s.HaveLebesgueDecomposition μ

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
htμ : t.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
⊢ s.toJordanDecomposition.posPart =
    (t.toJordanDecomposition.posPart, fun x => ENNReal.ofReal (f x)).1 +
      μ.withDensity (t.toJordanDecomposition.posPart, fun x => ENNReal.ofReal (f x)).2

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

Result:
no goals