awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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).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
rw : Integrable (ε := ℝ) (fun (x : α) ↦ (c.rnDeriv μ x).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

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]

Premises used: Complex.add_re, MeasureTheory.ComplexMeasure.integrable_rnDeriv, MeasureTheory.withDensityᵥ_apply, RCLike.re_eq_complex_re, MeasureTheory.Integrable.integrableOn, integral_re
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
h 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
⊢ (↑(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

Tactic:
rw [c.re.singularPart_add_withDensity_rnDeriv_eq μ]

Premises used: MeasureTheory.ComplexMeasure.re, MeasureTheory.SignedMeasure.singularPart_add_withDensity_rnDeriv_eq, DFunLike.coe
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (c.rnDeriv μ x).re) μ

Tactic:
SignedMeasure.integrable_rnDeriv _ _

Premises used: MeasureTheory.SignedMeasure.rnDeriv, MeasureTheory.SignedMeasure.integrable_rnDeriv
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (c.rnDeriv μ x).re) μ

Tactic:
exact SignedMeasure.integrable_rnDeriv _ _

Premises used: MeasureTheory.SignedMeasure.integrable_rnDeriv
-- 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).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
rw : Integrable (ε := ℝ) (fun (x : α) ↦ (c.rnDeriv μ x).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

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]

Premises used: Complex.add_im, MeasureTheory.ComplexMeasure.integrable_rnDeriv, MeasureTheory.withDensityᵥ_apply, MeasureTheory.Integrable.integrableOn, RCLike.im_eq_complex_im, integral_im
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
h 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
⊢ (↑(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

Tactic:
rw [c.im.singularPart_add_withDensity_rnDeriv_eq μ]

Premises used: MeasureTheory.SignedMeasure.singularPart_add_withDensity_rnDeriv_eq, DFunLike.coe, MeasureTheory.ComplexMeasure.im
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (c.rnDeriv μ x).im) μ

Tactic:
SignedMeasure.integrable_rnDeriv _ _

Premises used: MeasureTheory.SignedMeasure.rnDeriv, MeasureTheory.SignedMeasure.integrable_rnDeriv
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (c.rnDeriv μ x).im) μ

Tactic:
exact SignedMeasure.integrable_rnDeriv _ _

Premises used: MeasureTheory.SignedMeasure.integrable_rnDeriv
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym
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
rw₁ :
  ∀ (h : s.totalVariation ≪ μ.toENNRealVectorMeasure.ennrealToMeasure), μ.toENNRealVectorMeasure.ennrealToMeasure = μ
⊢ μ.withDensityᵥ (s.rnDeriv μ) = s

Tactic:
rw [absolutelyContinuous_ennreal_iff, (_ : μ.toENNRealVectorMeasure.ennrealToMeasure = μ),
    totalVariation_absolutelyContinuous_iff] at h

Premises used: MeasureTheory.SignedMeasure.absolutelyContinuous_ennreal_iff, MeasureTheory.SignedMeasure.totalVariation_absolutelyContinuous_iff
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
h₁ : ∀ (i : Set α) (hi : MeasurableSet i), (↑(μ.withDensityᵥ (s.rnDeriv μ)) : Set α → ℝ) i = (↑s : Set α → ℝ) i
⊢ μ.withDensityᵥ (s.rnDeriv μ) = s

Tactic:
ext1 i hi
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym
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)
h₃ : Integrable (ε := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal) (μ.restrict i)
⊢ (↑(μ.withDensityᵥ (s.rnDeriv μ)) : Set α → ℝ) 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]

Premises used: MeasureTheory.SignedMeasure.rnDeriv_def, MeasureTheory.integral_sub, MeasureTheory.withDensityᵥ_apply, And.right, And.left, MeasureTheory.SignedMeasure.integrable_rnDeriv, MeasureTheory.Measure.setIntegral_toReal_rnDeriv
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
rw : (↑s.toJordanDecomposition.toSignedMeasure : Set α → ℝ) i
| (↑s : Set α → ℝ) i

Tactic:
rw [← s.toSignedMeasure_toJordanDecomposition]

Premises used: MeasureTheory.SignedMeasure.toSignedMeasure_toJordanDecomposition
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym
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.toSignedMeasure : Set α → ℝ) i
⊢ s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i = (↑s : Set α → ℝ) i

Tactic:
conv_rhs => rw [← s.toSignedMeasure_toJordanDecomposition]

Premises used: MeasureTheory.SignedMeasure.toSignedMeasure_toJordanDecomposition
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym
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
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
h₆ h₇ :
  ENNReal.toReal ((s.toJordanDecomposition.posPart : (a : Set α) → ENNReal) i) -
      ENNReal.toReal ((s.toJordanDecomposition.negPart : (a : Set α) → ENNReal) i) =
    ENNReal.toReal ((s.toJordanDecomposition.posPart : (a : Set α) → ENNReal) i) -
      ENNReal.toReal ((s.toJordanDecomposition.negPart : (a : Set α) → ENNReal) i)
⊢ s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i =
    (↑s.toJordanDecomposition.toSignedMeasure : Set α → ℝ) i

Tactic:
rw [JordanDecomposition.toSignedMeasure, VectorMeasure.sub_apply,
        toSignedMeasure_apply_measurable hi, toSignedMeasure_apply_measurable hi, measureReal_def,
        measureReal_def]

Premises used: MeasureTheory.JordanDecomposition.toSignedMeasure, MeasureTheory.Measure.toSignedMeasure_apply_measurable, MeasureTheory.measureReal_def, MeasureTheory.VectorMeasure.sub_apply
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal) (μ.restrict i)

Tactic:
Integrable.integrableOn ?_

Premises used: MeasureTheory.IntegrableOn, MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
h₁ : Integrable (ε := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal) μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal) (μ.restrict i)

Tactic:
refine Integrable.integrableOn ?_

Premises used: MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal) μ

Tactic:
⟨?_, hasFiniteIntegral_toReal_of_lintegral_ne_top ?_⟩

Premises used: MeasureTheory.hasFiniteIntegral_toReal_of_lintegral_ne_top, MeasureTheory.Integrable, And.intro
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
h₁ : AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal) μ
h₂ : ∫⁻ (x : α), s.toJordanDecomposition.posPart.rnDeriv μ x ∂μ ≠ ⊤
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal) μ

Tactic:
refine ⟨?_, hasFiniteIntegral_toReal_of_lintegral_ne_top ?_⟩
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ Measurable (β := ℝ) fun (x : α) ↦ (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal) μ

Tactic:
apply Measurable.aestronglyMeasurable (by fun_prop)

Premises used: Measurable.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ ∫⁻ (x : α), s.toJordanDecomposition.posPart.rnDeriv μ x ∂μ ≠ ⊤

Tactic:
(lintegral_rnDeriv_lt_top _ _).ne

Premises used: MeasureTheory.Measure.lintegral_rnDeriv_lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ ∫⁻ (x : α), s.toJordanDecomposition.posPart.rnDeriv μ x ∂μ ≠ ⊤

Tactic:
exact (lintegral_rnDeriv_lt_top _ _).ne

Premises used: MeasureTheory.Measure.lintegral_rnDeriv_lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal) (μ.restrict i)

Tactic:
Integrable.integrableOn ?_

Premises used: MeasureTheory.IntegrableOn, MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
h₁ : Integrable (ε := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal) μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal) (μ.restrict i)

Tactic:
refine Integrable.integrableOn ?_

Premises used: MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal) μ

Tactic:
⟨?_, hasFiniteIntegral_toReal_of_lintegral_ne_top ?_⟩

Premises used: MeasureTheory.hasFiniteIntegral_toReal_of_lintegral_ne_top, MeasureTheory.Integrable, And.intro
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
h₁ : AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal) μ
h₂ : ∫⁻ (x : α), s.toJordanDecomposition.negPart.rnDeriv μ x ∂μ ≠ ⊤
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal) μ

Tactic:
refine ⟨?_, hasFiniteIntegral_toReal_of_lintegral_ne_top ?_⟩
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ Measurable (β := ℝ) fun (x : α) ↦ (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal) μ

Tactic:
apply Measurable.aestronglyMeasurable (by fun_prop)

Premises used: Measurable.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ ∫⁻ (x : α), s.toJordanDecomposition.negPart.rnDeriv μ x ∂μ ≠ ⊤

Tactic:
(lintegral_rnDeriv_lt_top _ _).ne

Premises used: MeasureTheory.Measure.lintegral_rnDeriv_lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ ∫⁻ (x : α), s.toJordanDecomposition.negPart.rnDeriv μ x ∂μ ≠ ⊤

Tactic:
exact (lintegral_rnDeriv_lt_top _ _).ne

Premises used: MeasureTheory.Measure.lintegral_rnDeriv_lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : SigmaFinite μ
h : s.totalVariation ≪ μ.toENNRealVectorMeasure.ennrealToMeasure
⊢ μ.toENNRealVectorMeasure.ennrealToMeasure = μ

Tactic:
equivMeasure.right_inv μ

Premises used: MeasureTheory.VectorMeasure.ennrealToMeasure, Equiv.right_inv, MeasureTheory.Measure.ofMeasurable, MeasureTheory.VectorMeasure.equivMeasure
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : SigmaFinite μ
h : s.totalVariation ≪ μ.toENNRealVectorMeasure.ennrealToMeasure
⊢ μ.toENNRealVectorMeasure.ennrealToMeasure = μ

Tactic:
exact equivMeasure.right_inv μ

Premises used: Equiv.right_inv, MeasureTheory.VectorMeasure.equivMeasure
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : SigmaFinite μ
⊢ s ≪ᵥ μ.toENNRealVectorMeasure ↔ μ.withDensityᵥ (s.rnDeriv μ) = s

Tactic:
⟨withDensityᵥ_rnDeriv_eq s μ, fun h => h ▸ withDensityᵥ_absolutelyContinuous _ _⟩

Premises used: MeasureTheory.SignedMeasure.withDensityᵥ_rnDeriv_eq, Eq.rec, MeasureTheory.SignedMeasure.rnDeriv, MeasureTheory.Measure.withDensityᵥ_absolutelyContinuous, Iff.intro
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ ν : Measure α
inst_2 : μ.HaveLebesgueDecomposition ν
inst_3 : SigmaFinite μ
f : α → E
hμν : μ ≪ ν
hf : Integrable f μ
rw : Eq (α := VectorMeasure α E) ((ν.withDensity (μ.rnDeriv ν)).withDensityᵥ f) (μ.withDensityᵥ f)
rw₁ rw₂ : Eq (α := VectorMeasure α E) (μ.withDensityᵥ f) (μ.withDensityᵥ f)
⊢ Eq (α := VectorMeasure α E) (ν.withDensityᵥ fun (x : α) ↦ (μ.rnDeriv ν x).toReal • f x) (μ.withDensityᵥ f)

Tactic:
rw [withDensityᵥ_smul_eq_withDensityᵥ_withDensity' (measurable_rnDeriv μ ν).aemeasurable
    (rnDeriv_lt_top μ ν) ((integrable_rnDeriv_smul_iff hμν).mpr hf), withDensity_rnDeriv_eq μ ν hμν]

Premises used: Iff.mpr, Measurable.aemeasurable, MeasureTheory.Measure.rnDeriv_lt_top, MeasureTheory.withDensityᵥ_smul_eq_withDensityᵥ_withDensity', MeasureTheory.integrable_rnDeriv_smul_iff, MeasureTheory.Measure.measurable_rnDeriv, MeasureTheory.Measure.withDensity_rnDeriv_eq
-- Module: Mathlib.MeasureTheory.VectorMeasure.Integral
Goal:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
⊢ (↑(μ.transpose B) : Set X → E →L[ℝ] G) = cbmApplyMeasure μ B

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.VectorMeasure.Integral
Goal:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
s : Set X
x : E
⊢ Eq.{u_5 + 1} (α := G) ((cbmApplyMeasure μ B s : (a : E) → G) x : G)
    ((((B : (a : E) → F →L[ℝ] G) x : F →L[ℝ] G) : (a : F) → G) ((↑μ : Set X → F) s) : G)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.VectorMeasure.Integral
Goal:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
s t : Set X
hs : MeasurableSet s
ht : MeasurableSet t
hdisj : Disjoint s t
h :
  ∀ (x : E),
    Eq.{u_5 + 1} (α := G) ((cbmApplyMeasure μ B (s ∪ t) : (a : E) → G) x : G)
      ((cbmApplyMeasure μ B s + cbmApplyMeasure μ B t : (a : E) → G) x : G)
⊢ cbmApplyMeasure μ B (s ∪ t) = cbmApplyMeasure μ B s + cbmApplyMeasure μ B t

Tactic:
ext x