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

Goal state before:
pp: 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 ⟂ₘ μ
⊢ { 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 := ⋯ }.posPart =
    (t.toJordanDecomposition.posPart, fun x ↦ ENNReal.ofReal (f x)).1 +
      μ.withDensity (t.toJordanDecomposition.posPart, fun x ↦ ENNReal.ofReal (f x)).2

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Goal state before:
pp: case neg
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
hf : MemLp f p μ
hp : 1 ≤ p
hg : ¬MemLp g p μ
⊢ 0 ≤ lpNorm f p μ + 0

Tactic:
]

Goal state after:
case neg
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
hf : MemLp f p μ
hp : 1 ≤ p
hg : ¬MemLp g p μ
⊢ 0 ≤ lpNorm f p μ + 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: 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 ⟂ₘ μ
⊢ { 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 := ⋯ }.negPart =
    (t.toJordanDecomposition.negPart, fun x ↦ ENNReal.ofReal (-f x)).1 +
      μ.withDensity (t.toJordanDecomposition.negPart, fun x ↦ ENNReal.ofReal (-f x)).2

Tactic:
]

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

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t
hfi : ¬Integrable f μ
⊢ s.HaveLebesgueDecomposition μ

Tactic:
]

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t
hfi : ¬Integrable f μ
⊢ s.HaveLebesgueDecomposition μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
ι : Type u_3
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, MemLp (f i) p μ
hp : 1 ≤ p
⊢ (eLpNorm (∑ i ∈ s, f i) p μ).toReal ≤ (∑ a ∈ s, eLpNorm (f a) p μ).toReal

Tactic:
]

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
ι : Type u_3
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, MemLp (f i) p μ
hp : 1 ≤ p
⊢ (eLpNorm (∑ i ∈ s, f i) p μ).toReal ≤ (∑ a ∈ s, eLpNorm (f a) p μ).toReal
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t
hfi : ¬Integrable f μ
⊢ s = t

Tactic:
]

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t
hfi : ¬Integrable f μ
⊢ s = t
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
ι : Type u_3
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, MemLp (f i) p μ
hp : 1 ≤ p
⊢ (∑ i ∈ s, eLpNorm (f i) p μ).toReal ≤ (∑ a ∈ s, eLpNorm (f a) p μ).toReal

pp: case hb
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
ι : Type u_3
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, MemLp (f i) p μ
hp : 1 ≤ p
⊢ ∑ i ∈ s, eLpNorm (f i) p μ ≠ ∞

Tactic:
]

Goal state after:
case hb
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
ι : Type u_3
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, MemLp (f i) p μ
hp : 1 ≤ p
⊢ ∑ i ∈ s, eLpNorm (f i) p μ ≠ ∞
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Goal state before:
pp: case inr
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : Module ℚ≥0 E
inst✝ : NormedSpace ℝ E
ι : Type u_3
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, MemLp (f i) p μ
hp : 1 ≤ p
hs : s.Nonempty
⊢ lpNorm (∑ i ∈ s, f i) p μ ≤ ∑ i ∈ s, (fun i ↦ lpNorm (f i) p μ) i

Tactic:
]

Goal state after:
case inr
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : Module ℚ≥0 E
inst✝ : NormedSpace ℝ E
ι : Type u_3
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, MemLp (f i) p μ
hp : 1 ≤ p
hs : s.Nonempty
⊢ lpNorm (∑ i ∈ s, f i) p μ ≤ ∑ i ∈ s, (fun i ↦ lpNorm (f i) p μ) i
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : 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
⊢ t = s.singularPart μ

Tactic:
]

Goal state after:
α : 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
⊢ t = s.singularPart μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
g : α → ℝ
hg : MemLp g p μ
h : ∀ (x : α), ‖f x‖ ≤ g x
hf : AEStronglyMeasurable f μ
⊢ (eLpNorm f p μ).toReal ≤ (eLpNorm g p μ).toReal

Tactic:
]

Goal state after:
case pos
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
g : α → ℝ
hg : MemLp g p μ
h : ∀ (x : α), ‖f x‖ ≤ g x
hf : AEStronglyMeasurable f μ
⊢ (eLpNorm f p μ).toReal ≤ (eLpNorm g p μ).toReal
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Goal state before:
pp: case neg
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
c : ℝ≥0
hc : c ≠ 0
hf : ¬AEStronglyMeasurable f μ
⊢ 0 = c ^ p.toReal⁻¹ • 0

Tactic:
]

Goal state after:
case neg
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
c : ℝ≥0
hc : c ≠ 0
hf : ¬AEStronglyMeasurable f μ
⊢ 0 = c ^ p.toReal⁻¹ • 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : 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
⊢ t.toJordanDecomposition.posPart.toSignedMeasure - t.toJordanDecomposition.negPart.toSignedMeasure =
    (s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure

Tactic:
]

Goal state after:
α : 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
⊢ t.toJordanDecomposition.posPart.toSignedMeasure - t.toJordanDecomposition.negPart.toSignedMeasure =
    (s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: case e_a
α : 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
hfpos : Measurable fun x ↦ ENNReal.ofReal (f x)
⊢ { 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 := ⋯ }.posPart =
    t.toJordanDecomposition.posPart + μ.withDensity fun x ↦ ENNReal.ofReal (f x)

Tactic:
]

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

Goal state before:
pp: case e_a
α : 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 fun x ↦ ENNReal.ofReal (-f x)
⊢ { 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 := ⋯ }.negPart =
    t.toJordanDecomposition.negPart + μ.withDensity fun x ↦ ENNReal.ofReal (-f x)

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Goal state before:
pp: case neg.inr.inl
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : p ≠ ∞
f : α → E
hf : ¬AEStronglyMeasurable f μ
hp₀ : p ≠ 0
⊢ lpNorm f p (0 • μ) = 0 • lpNorm f p μ

Tactic:
]

Goal state after:
case neg.inr.inl
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : p ≠ ∞
f : α → E
hf : ¬AEStronglyMeasurable f μ
hp₀ : p ≠ 0
⊢ lpNorm f p (0 • μ) = 0 • lpNorm f p μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Goal state before:
pp: case neg.inr.inr
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : p ≠ ∞
f : α → E
c : ℝ≥0
hf : ¬AEStronglyMeasurable f μ
hp₀ : p ≠ 0
hc : c ≠ 0
⊢ 0 = c ^ p.toReal⁻¹ • 0

Tactic:
]

Goal state after:
case neg.inr.inr
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : p ≠ ∞
f : α → E
c : ℝ≥0
hf : ¬AEStronglyMeasurable f μ
hp₀ : p ≠ 0
hc : c ≠ 0
⊢ 0 = c ^ p.toReal⁻¹ • 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t
hfi : ¬Integrable f μ
⊢ t = s.singularPart μ

Tactic:
]

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t
hfi : ¬Integrable f μ
⊢ t = s.singularPart μ
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t
hfi : ¬Integrable f μ
⊢ s = t

Tactic:
]

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t
hfi : ¬Integrable f μ
⊢ s = t
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
K : Type u_3
inst✝ : RCLike K
f : α → K
p : ℝ≥0∞
μ : Measure α
hf : AEStronglyMeasurable f μ
⊢ lpNorm (fun x ↦ ‖(starRingEnd (α → K)) f x‖) p μ = lpNorm (fun x ↦ ‖f x‖) p μ

pp: case pos.hf
α : Type u_1
m : MeasurableSpace α
K : Type u_3
inst✝ : RCLike K
f : α → K
p : ℝ≥0∞
μ : Measure α
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable ((starRingEnd (α → K)) f) μ

Tactic:
]

Goal state after:
case pos
α : Type u_1
m : MeasurableSpace α
K : Type u_3
inst✝ : RCLike K
f : α → K
p : ℝ≥0∞
μ : Measure α
hf : AEStronglyMeasurable f μ
⊢ lpNorm (fun x ↦ ‖(starRingEnd (α → K)) f x‖) p μ = lpNorm (fun x ↦ ‖f x‖) p μ

case pos.hf
α : Type u_1
m : MeasurableSpace α
K : Type u_3
inst✝ : RCLike K
f : α → K
p : ℝ≥0∞
μ : Measure α
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable ((starRingEnd (α → K)) f) μ
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
hfg : Tendsto (fun n ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
this : f = (fun x ↦ g) + fun n ↦ f n - g
⊢ UnifIntegrable ((fun x ↦ g) + fun n ↦ f n - g) p μ

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
hfg : Tendsto (fun n ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
this : f = (fun x ↦ g) + fun n ↦ f n - g
⊢ UnifIntegrable ((fun x ↦ g) + fun n ↦ f n - g) p μ
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
K : Type u_3
inst✝ : RCLike K
f : α → K
p : ℝ≥0∞
μ : Measure α
hf : ¬AEStronglyMeasurable f μ
⊢ 0 = 0

pp: α : Type u_1
m : MeasurableSpace α
K : Type u_3
inst✝ : RCLike K
f : α → K
p : ℝ≥0∞
μ : Measure α
hf : ¬AEStronglyMeasurable f μ
h : AEStronglyMeasurable ((starRingEnd (α → K)) f) μ
⊢ AEStronglyMeasurable f μ

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
K : Type u_3
inst✝ : RCLike K
f : α → K
p : ℝ≥0∞
μ : Measure α
hf : ¬AEStronglyMeasurable f μ
h : AEStronglyMeasurable ((starRingEnd (α → K)) f) μ
⊢ AEStronglyMeasurable f μ
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
⊢ ((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:
]

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

Goal state before:
pp: case inr
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
⊢ ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
    r •
      ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure)

Tactic:
]

Goal state after:
case inr
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
⊢ ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
    r •
      ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure)
Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed

Goal state before:
pp: case refine_2
Ω : Type u_1
inst✝⁴ : TopologicalSpace Ω
inst✝³ : MeasurableSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
fs : ι → Ω →ᵇ ℝ≥0
c : ℝ≥0
fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i) ω ≤ c
f : Ω → ℝ≥0
fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun i ↦ (fs i) ω) L (𝓝 (f ω))
⊢ ∀ᵐ (a : Ω) ∂μ, Tendsto (fun n ↦ ↑((fs n) a)) L (𝓝 ↑(f a))

Tactic:
· simpa only [Function.comp_apply, ENNReal.tendsto_coe] using fs_lim

Goal state after:
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : μ univ = 0
⊢ UnifIntegrable f p μ

Tactic:
Measure.measure_univ_eq_zero

Goal state after:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : μ = 0
⊢ UnifIntegrable f p μ
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : μ = 0
⊢ UnifIntegrable f p μ

Tactic:
]

Goal state after:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : μ = 0
⊢ UnifIntegrable f p μ
Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed

Goal state before:
pp: Ω : Type u_1
inst✝³ : TopologicalSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ℕ → Ω →ᵇ ℝ≥0
fs_bdd : ∀ (n : ℕ) (ω : Ω), (fs n) ω ≤ c
fs_lim : ∀ (x : Ω), Tendsto (fun i ↦ (fs i) x) atTop (𝓝 (E.indicator (fun x ↦ 1) x))
⊢ ∀ (ω : Ω), Tendsto (fun n ↦ (fs n) ω) atTop (𝓝 (E.indicator (fun x ↦ 1) ω))

Tactic:
]

Goal state after:
Ω : Type u_1
inst✝³ : TopologicalSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ℕ → Ω →ᵇ ℝ≥0
fs_bdd : ∀ (n : ℕ) (ω : Ω), (fs n) ω ≤ c
fs_lim : ∀ (x : Ω), Tendsto (fun i ↦ (fs i) x) atTop (𝓝 (E.indicator (fun x ↦ 1) x))
⊢ ∀ (ω : Ω), Tendsto (fun n ↦ (fs n) ω) atTop (𝓝 (E.indicator (fun x ↦ 1) ω))
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: case inr
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
⊢ r •
      ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure) =
    r •
      ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure)

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed

Goal state before:
pp: Ω : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
key : Tendsto (fun n ↦ ⇑(thickenedIndicator ⋯ F)) atTop (𝓝 (F.indicator fun x ↦ 1))
⊢ Tendsto (fun n ω ↦ (thickenedIndicator ⋯ F) ω) atTop (𝓝 (F.indicator fun x ↦ 1))

Tactic:
]

Goal state after:
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
key : Tendsto (fun n ↦ ⇑(thickenedIndicator ⋯ F)) atTop (𝓝 (F.indicator fun x ↦ 1))
⊢ Tendsto (fun n ω ↦ (thickenedIndicator ⋯ F) ω) atTop (𝓝 (F.indicator fun x ↦ 1))
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst✝¹ : s.HaveLebesgueDecomposition μ
inst✝ : t.HaveLebesgueDecomposition μ
⊢ s + t = s + t

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬μ univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ p.toReal)
hμs' : μ s = 0
⊢ 0 ≤ ENNReal.ofReal ε

Tactic:
]

Goal state after:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬μ univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ p.toReal)
hμs' : μ s = 0
⊢ 0 ≤ ENNReal.ofReal ε
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst✝¹ : s.HaveLebesgueDecomposition μ
inst✝ : t.HaveLebesgueDecomposition μ
⊢ s.singularPart μ + -t.singularPart μ = s.singularPart μ + -t.singularPart μ

Tactic:
]

Goal state after: