mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → 0 j ≤ s j) ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → s j ≤ 0 j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → 0 j_1 ≤ s j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → s j_1 ≤ 0 j_1
⊢ s (i ∆ j) = 0 ∧ s (iᶜ ∆ jᶜ) = 0

pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → 0 j ≤ s j) ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → s j ≤ 0 j
hj' : 0 ≤[j] s ∧ ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → s j_1 ≤ 0 j_1
⊢ MeasurableSet j

pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : 0 ≤[i] s ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → s j ≤ 0 j
hj' : 0 ≤[j] s ∧ ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → s j_1 ≤ 0 j_1
⊢ MeasurableSet i

pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : 0 ≤[i] s ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → s j ≤ 0 j
hj' : 0 ≤[j] s ∧ s ≤[jᶜ] 0
⊢ MeasurableSet jᶜ

pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : 0 ≤[i] s ∧ s ≤[iᶜ] 0
hj' : 0 ≤[j] s ∧ s ≤[jᶜ] 0
⊢ MeasurableSet iᶜ

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → 0 j ≤ s j) ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → s j ≤ 0 j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → 0 j_1 ≤ s j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → s j_1 ≤ 0 j_1
⊢ s (i ∆ j) = 0 ∧ s (iᶜ ∆ jᶜ) = 0

α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → 0 j ≤ s j) ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → s j ≤ 0 j
hj' : 0 ≤[j] s ∧ ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → s j_1 ≤ 0 j_1
⊢ MeasurableSet j

α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : 0 ≤[i] s ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → s j ≤ 0 j
hj' : 0 ≤[j] s ∧ ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → s j_1 ≤ 0 j_1
⊢ MeasurableSet i

α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : 0 ≤[i] s ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → s j ≤ 0 j
hj' : 0 ≤[j] s ∧ s ≤[jᶜ] 0
⊢ MeasurableSet jᶜ

α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : 0 ≤[i] s ∧ s ≤[iᶜ] 0
hj' : 0 ≤[j] s ∧ s ≤[jᶜ] 0
⊢ MeasurableSet iᶜ
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case h₁
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
h : ε < ∞
hμ : ¬μ = 0
hε' : 0 < ε.toReal / 3
hdivp : 0 ≤ 1 / p.toReal
hpow : 0 < measureUnivNNReal μ ^ (1 / p.toReal)
δ₁ : ℝ
hδ₁ : 0 < δ₁
heLpNorm₁ :
  ∀ (i : ℕ) (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
δ₂ : ℝ
hδ₂ : 0 < δ₂
heLpNorm₂ :
  ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
t : Set α
htm : MeasurableSet t
ht₁ : μ t ≤ ENNReal.ofReal (min δ₁ δ₂)
N n : ℕ
hN : ∀ x ∈ tᶜ, dist (g x) (f n x) < ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))
hn : n ≥ N
hnf : eLpNorm (t.indicator (f n)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
hng : eLpNorm (t.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
this✝ : 0 ≤ ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))
this :
  eLpNorm (tᶜ.indicator (f n - g)) p μ ≤
    ENNReal.ofReal (ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))) * μ tᶜ ^ (1 / p.toReal)
⊢ μ tᶜ ≤ μ univ

Tactic:
]

Goal state after:
case h₁
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
h : ε < ∞
hμ : ¬μ = 0
hε' : 0 < ε.toReal / 3
hdivp : 0 ≤ 1 / p.toReal
hpow : 0 < measureUnivNNReal μ ^ (1 / p.toReal)
δ₁ : ℝ
hδ₁ : 0 < δ₁
heLpNorm₁ :
  ∀ (i : ℕ) (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
δ₂ : ℝ
hδ₂ : 0 < δ₂
heLpNorm₂ :
  ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
t : Set α
htm : MeasurableSet t
ht₁ : μ t ≤ ENNReal.ofReal (min δ₁ δ₂)
N n : ℕ
hN : ∀ x ∈ tᶜ, dist (g x) (f n x) < ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))
hn : n ≥ N
hnf : eLpNorm (t.indicator (f n)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
hng : eLpNorm (t.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
this✝ : 0 ≤ ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))
this :
  eLpNorm (tᶜ.indicator (f n - g)) p μ ≤
    ENNReal.ofReal (ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))) * μ tᶜ ^ (1 / p.toReal)
⊢ μ tᶜ ≤ μ univ
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : α → E
h : f =ᵐ[μ] g
hf : ¬Integrable f μ
hg : ¬Integrable g μ
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ✝ : Measure α
s : SignedMeasure α
μ : Measure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ s.toJordanDecomposition.negPart.HaveLebesgueDecomposition μ

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ✝ : Measure α
s : SignedMeasure α
μ : Measure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ s.toJordanDecomposition.negPart.HaveLebesgueDecomposition μ
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ✝ : Measure α
s : SignedMeasure α
μ : Measure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ s.toJordanDecomposition.posPart.HaveLebesgueDecomposition μ

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ✝ : Measure α
s : SignedMeasure α
μ : Measure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ s.toJordanDecomposition.posPart.HaveLebesgueDecomposition μ
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ✝ : Measure α
s : SignedMeasure α
μ : Measure α
inst✝ : s.HaveLebesgueDecomposition μ
r : ℝ≥0
⊢ (r • s.toJordanDecomposition.posPart).HaveLebesgueDecomposition μ

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ✝ : Measure α
s : SignedMeasure α
μ : Measure α
inst✝ : s.HaveLebesgueDecomposition μ
r : ℝ≥0
⊢ (r • s.toJordanDecomposition.posPart).HaveLebesgueDecomposition μ
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ✝ : Measure α
s : SignedMeasure α
μ : Measure α
inst✝ : s.HaveLebesgueDecomposition μ
r : ℝ≥0
⊢ (r • s.toJordanDecomposition.negPart).HaveLebesgueDecomposition μ

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ✝ : Measure α
s : SignedMeasure α
μ : Measure α
inst✝ : s.HaveLebesgueDecomposition μ
r : ℝ≥0
⊢ (r • s.toJordanDecomposition.negPart).HaveLebesgueDecomposition μ
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ✝ : Measure α
s : SignedMeasure α
μ : Measure α
inst✝ : s.HaveLebesgueDecomposition μ
r : ℝ
hr : r < 0
⊢ ((-r).toNNReal • s.toJordanDecomposition.negPart).HaveLebesgueDecomposition μ

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ✝ : Measure α
s : SignedMeasure α
μ : Measure α
inst✝ : s.HaveLebesgueDecomposition μ
r : ℝ
hr : r < 0
⊢ ((-r).toNNReal • s.toJordanDecomposition.negPart).HaveLebesgueDecomposition μ
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ✝ : Measure α
s : SignedMeasure α
μ : Measure α
inst✝ : s.HaveLebesgueDecomposition μ
r : ℝ
hr : r < 0
⊢ ((-r).toNNReal • s.toJordanDecomposition.posPart).HaveLebesgueDecomposition μ

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ✝ : Measure α
s : SignedMeasure α
μ : Measure α
inst✝ : s.HaveLebesgueDecomposition μ
r : ℝ
hr : r < 0
⊢ ((-r).toNNReal • s.toJordanDecomposition.posPart).HaveLebesgueDecomposition μ
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hfi : Integrable (fun x ↦ (f x).toReal) μ
this : IsFiniteMeasure (μ.withDensity f)
i : Set α
hi : MeasurableSet i
⊢ (∫⁻ (a : α) in i, f a ∂μ).toReal = (∫⁻ (a : α) in i, f a ∂μ).toReal

pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hfi : Integrable (fun x ↦ (f x).toReal) μ
this : IsFiniteMeasure (μ.withDensity f)
i : Set α
hi : MeasurableSet i
⊢ ∀ᵐ (x : α) ∂μ.restrict i, f x < ∞

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hfi : Integrable (fun x ↦ (f x).toReal) μ
this : IsFiniteMeasure (μ.withDensity f)
i : Set α
hi : MeasurableSet i
⊢ ∀ᵐ (x : α) ∂μ.restrict i, f x < ∞
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ (s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
    { posPart := s.toJordanDecomposition.posPart.singularPart μ,
            negPart := s.toJordanDecomposition.negPart.singularPart μ, posPart_finite := ⋯, negPart_finite := ⋯,
            mutuallySingular := ⋯ }.posPart.toSignedMeasure -
      { posPart := s.toJordanDecomposition.posPart.singularPart μ,
            negPart := s.toJordanDecomposition.negPart.singularPart μ, posPart_finite := ⋯, negPart_finite := ⋯,
            mutuallySingular := ⋯ }.negPart.toSignedMeasure

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
this :
  (s.singularPart μ).toJordanDecomposition =
    { posPart := s.toJordanDecomposition.posPart.singularPart μ,
      negPart := s.toJordanDecomposition.negPart.singularPart μ, posPart_finite := ⋯, negPart_finite := ⋯,
      mutuallySingular := ⋯ }
⊢ { posPart := s.toJordanDecomposition.posPart.singularPart μ,
          negPart := s.toJordanDecomposition.negPart.singularPart μ, posPart_finite := ⋯, negPart_finite := ⋯,
          mutuallySingular := ⋯ }.posPart +
      { posPart := s.toJordanDecomposition.posPart.singularPart μ,
          negPart := s.toJordanDecomposition.negPart.singularPart μ, posPart_finite := ⋯, negPart_finite := ⋯,
          mutuallySingular := ⋯ }.negPart =
    s.toJordanDecomposition.posPart.singularPart μ + s.toJordanDecomposition.negPart.singularPart μ

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ s.toJordanDecomposition.posPart.singularPart μ + s.toJordanDecomposition.negPart.singularPart μ ⟂ₘ μ

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ s.toJordanDecomposition.posPart.singularPart μ + s.toJordanDecomposition.negPart.singularPart μ ⟂ₘ μ
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ Measurable fun x ↦
    (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal - (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ Measurable fun x ↦
    (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal - (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : Integrable f μ
this✝ : IsFiniteMeasure (μ.withDensity fun x ↦ ENNReal.ofReal (f x))
this : IsFiniteMeasure (μ.withDensity fun x ↦ ENNReal.ofReal ((-f) x))
i : Set α
hi : MeasurableSet i
⊢ (∫⁻ (a : α) in i, ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α) in i, ENNReal.ofReal (-f a) ∂μ).toReal =
    (∫⁻ (a : α) in i, ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α) in i, ENNReal.ofReal (-f a) ∂μ).toReal

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ
hf : Integrable f μ
i : Set α
hi : MeasurableSet i
⊢ ∫ (x : α) in i, f x ∂μ = ∫ (x : α) in i, f x ∂μ

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case left
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → 0 j ≤ s j) ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → s j ≤ 0 j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → 0 j_1 ≤ s j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → s j_1 ≤ 0 j_1
⊢ 0 = 0

pp: case left.h
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → 0 j ≤ s j) ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → s j ≤ 0 j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → 0 j_1 ≤ s j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → s j_1 ≤ 0 j_1
⊢ Disjoint (jᶜ ∩ i) (iᶜ ∩ j)

pp: case left.hA
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → 0 j ≤ s j) ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → s j ≤ 0 j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → 0 j_1 ≤ s j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → s j_1 ≤ 0 j_1
⊢ MeasurableSet (jᶜ ∩ i)

pp: case left.hB
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → 0 j ≤ s j) ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → s j ≤ 0 j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → 0 j_1 ≤ s j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → s j_1 ≤ 0 j_1
⊢ MeasurableSet (iᶜ ∩ j)

Tactic:
]

Goal state after:
case left.h
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → 0 j ≤ s j) ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → s j ≤ 0 j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → 0 j_1 ≤ s j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → s j_1 ≤ 0 j_1
⊢ Disjoint (jᶜ ∩ i) (iᶜ ∩ j)

case left.hA
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → 0 j ≤ s j) ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → s j ≤ 0 j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → 0 j_1 ≤ s j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → s j_1 ≤ 0 j_1
⊢ MeasurableSet (jᶜ ∩ i)

case left.hB
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → 0 j ≤ s j) ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → s j ≤ 0 j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → 0 j_1 ≤ s j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → s j_1 ≤ 0 j_1
⊢ MeasurableSet (iᶜ ∩ j)
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hfi : Integrable f μ
j : Set α
hj₁ : MeasurableSet j
hj₂ : μ j = 0
⊢ ((μ.withDensityᵥ f).trim hm) j = 0

Tactic:
]

Goal state after:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hfi : Integrable f μ
j : Set α
hj₁ : MeasurableSet j
hj₂ : μ j = 0
⊢ ((μ.withDensityᵥ f).trim hm) j = 0
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
h : ε < ∞
hμ : ¬μ = 0
hε' : 0 < ε.toReal / 3
hdivp : 0 ≤ 1 / p.toReal
hpow : 0 < measureUnivNNReal μ ^ (1 / p.toReal)
δ₁ : ℝ
hδ₁ : 0 < δ₁
heLpNorm₁ :
  ∀ (i : ℕ) (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
δ₂ : ℝ
hδ₂ : 0 < δ₂
heLpNorm₂ :
  ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
t : Set α
htm : MeasurableSet t
ht₁ : μ t ≤ ENNReal.ofReal (min δ₁ δ₂)
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ∀ x ∈ tᶜ, dist (g x) (f b x) < ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))
n : ℕ
hn : n ≥ N
hnf : eLpNorm (t.indicator (f n)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
hng : eLpNorm (t.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
hlt : eLpNorm (tᶜ.indicator (f n - g)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
⊢ ε / ENNReal.ofReal 3 = ε / 3

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
h : ε < ∞
hμ : ¬μ = 0
hε' : 0 < ε.toReal / 3
hdivp : 0 ≤ 1 / p.toReal
hpow : 0 < measureUnivNNReal μ ^ (1 / p.toReal)
δ₁ : ℝ
hδ₁ : 0 < δ₁
heLpNorm₁ :
  ∀ (i : ℕ) (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
δ₂ : ℝ
hδ₂ : 0 < δ₂
heLpNorm₂ :
  ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
t : Set α
htm : MeasurableSet t
ht₁ : μ t ≤ ENNReal.ofReal (min δ₁ δ₂)
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ∀ x ∈ tᶜ, dist (g x) (f b x) < ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))
n : ℕ
hn : n ≥ N
hnf : eLpNorm (t.indicator (f n)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
hng : eLpNorm (t.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
hlt : eLpNorm (tᶜ.indicator (f n - g)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
⊢ ε / ENNReal.ofReal 3 = ε / 3
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hfi : Integrable f μ
j : Set α
hj₁ : MeasurableSet j
hj₂ : μ j = 0
⊢ ∫ (x : α) in j, f x ∂μ = 0

Tactic:
]

Goal state after:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hfi : Integrable f μ
j : Set α
hj₁ : MeasurableSet j
hj₂ : μ j = 0
⊢ ∫ (x : α) in j, f x ∂μ = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
⊢ μ.withDensityᵥ (s.rnDeriv μ) = s

pp: α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : s.totalVariation ≪ μ.toENNRealVectorMeasure.ennrealToMeasure
⊢ μ.toENNRealVectorMeasure.ennrealToMeasure = μ

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
⊢ μ.withDensityᵥ (s.rnDeriv μ) = s

α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : s.totalVariation ≪ μ.toENNRealVectorMeasure.ennrealToMeasure
⊢ μ.toENNRealVectorMeasure.ennrealToMeasure = μ
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym

Goal state before:
pp: α : 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 i

pp: case hf
α : 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)

pp: case hg
α : 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:
]

Goal state after:
α : 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 i

case hf
α : 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)

case hg
α : 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)
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym

Goal state before:
pp: α : 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 i).toReal - (s.toJordanDecomposition.negPart i).toReal =
    (s.toJordanDecomposition.posPart i).toReal - (s.toJordanDecomposition.negPart i).toReal

Tactic:
]

Goal state after: