mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case neg.h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M ↦ {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable ({x | ↑M ≤ ↑‖f x‖₊}.indicator f) μ
hbound : HasFiniteIntegral (fun x ↦ ‖f x‖) μ
n : ℕ
x : α
hx : ¬↑n ≤ ‖f x‖
⊢ x ∉ {x | ↑n ≤ ‖f x‖₊}

Tactic:
assumption

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

Goal state before:
pp: case refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ.toSignedMeasure = ν.toSignedMeasure
i : Set α
hi : MeasurableSet i
this : μ.toSignedMeasure i = ν.toSignedMeasure i
⊢ μ i = ν i

Tactic:
toSignedMeasure_apply_measurable hi,

Goal state after:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ.toSignedMeasure = ν.toSignedMeasure
i : Set α
hi : MeasurableSet i
this : μ.real i = ν.toSignedMeasure i
⊢ μ i = ν i
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ.toSignedMeasure = ν.toSignedMeasure
i : Set α
hi : MeasurableSet i
this : μ.real i = ν.toSignedMeasure i
⊢ μ i = ν i

Tactic:
toSignedMeasure_apply_measurable hi,

Goal state after:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ.toSignedMeasure = ν.toSignedMeasure
i : Set α
hi : MeasurableSet i
this : μ.real i = ν.real i
⊢ μ i = ν i
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
i : Set α
hi : MeasurableSet i
⊢ (μ + ν).toSignedMeasure i = (μ.toSignedMeasure + ν.toSignedMeasure) i

Tactic:
toSignedMeasure_apply_measurable hi,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
i : Set α
hi : MeasurableSet i
⊢ (μ + ν).real i = (μ.toSignedMeasure + ν.toSignedMeasure) i
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
i : Set α
hi : MeasurableSet i
⊢ μ.real i + ν.real i = μ.toSignedMeasure i + ν.toSignedMeasure i

Tactic:
toSignedMeasure_apply_measurable hi,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
i : Set α
hi : MeasurableSet i
⊢ μ.real i + ν.real i = μ.real i + ν.toSignedMeasure i
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0
i : Set α
hi : MeasurableSet i
⊢ (r • μ).toSignedMeasure i = (r • μ.toSignedMeasure) i

Tactic:
toSignedMeasure_apply_measurable hi,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0
i : Set α
hi : MeasurableSet i
⊢ (r • μ).real i = (r • μ.toSignedMeasure) i
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0
i : Set α
hi : MeasurableSet i
⊢ (r • μ).real i = (r • μ.toSignedMeasure) i

Tactic:
_root_.smul_apply,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0
i : Set α
hi : MeasurableSet i
⊢ (r • μ).real i = r • μ.toSignedMeasure i
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0
i : Set α
hi : MeasurableSet i
⊢ (r • μ).real i = r • μ.toSignedMeasure i

Tactic:
toSignedMeasure_apply_measurable hi,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0
i : Set α
hi : MeasurableSet i
⊢ (r • μ).real i = r • μ.real i
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
i : Set α
hi : MeasurableSet i
⊢ μ.toSignedMeasure i - ν.toSignedMeasure i = μ.real i - ν.real i

Tactic:
toSignedMeasure_apply_measurable hi,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
i : Set α
hi : MeasurableSet i
⊢ μ.real i - ν.toSignedMeasure i = μ.real i - ν.real i
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : μ s ≤ ENNReal.ofReal ((ε / M) ^ p.toReal)
hp : ¬p = 0
haebdd : ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ M
⊢ μ (univ ∩ s) ^ p.toReal⁻¹ * ENNReal.ofReal M ≤ ENNReal.ofReal ε

Tactic:
Set.univ_inter,

Goal state after:
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : μ s ≤ ENNReal.ofReal ((ε / M) ^ p.toReal)
hp : ¬p = 0
haebdd : ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ M
⊢ μ s ^ p.toReal⁻¹ * ENNReal.ofReal M ≤ ENNReal.ofReal ε
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
x : α
h : x ∈ {x | ‖f x‖ < M}
⊢ ‖f x‖ < ?m.95

pp: case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
x : α
h : x ∉ {x | ‖f x‖ < M}
⊢ 0 < ?m.95

Tactic:
exacts [h, hMpos]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
r : ℝ≥0
i : Set α
hi : MeasurableSet i
⊢ (r • j).toSignedMeasure i = (r • j.toSignedMeasure) i

Tactic:
_root_.smul_apply,

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
r : ℝ≥0
i : Set α
hi : MeasurableSet i
⊢ (r • j).toSignedMeasure i = r • j.toSignedMeasure i
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: case hi
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → 0 j ≤ s j
hsv : 0 ≤[v] s
hs : s (u ∆ v) = 0
⊢ MeasurableSet v

Tactic:
assumption

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

Goal state before:
pp: case hi
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : 0 ≤[u] s
hsv : 0 ≤[v] s
hs : s (u ∆ v) = 0
⊢ MeasurableSet u

Tactic:
assumption

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

Goal state before:
pp: case posPart
α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.posPart = j₂.posPart
hj' : j₁.toSignedMeasure = j₂.toSignedMeasure
⊢ j₁.posPart = j₂.posPart

pp: case negPart
α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.posPart = j₂.posPart
hj' : j₁.toSignedMeasure = j₂.toSignedMeasure
⊢ j₁.negPart = j₂.negPart

Tactic:
· exact hj

Goal state after:
case negPart
α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.posPart = j₂.posPart
hj' : j₁.toSignedMeasure = j₂.toSignedMeasure
⊢ j₁.negPart = j₂.negPart
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁶ : AddCommMonoid M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
R : Type u_6
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
r : R
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
s : Set α
hs : w s = 0
⊢ (r • v) s = 0

Tactic:
_root_.smul_apply,

Goal state after:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁶ : AddCommMonoid M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
R : Type u_6
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
r : R
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
s : Set α
hs : w s = 0
⊢ r • v s = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : s i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
A : Set α := ⋯
hA : A = i \ ⋃ l, s.restrictNonposSeq i l
bdd : ℕ → ℕ := ⋯
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : s i = s A + ∑' (l : ℕ), s (s.restrictNonposSeq i l)
⊢ 0 ≤ ∑' (l : ℕ), s (s.restrictNonposSeq i l)

Tactic:
exact tsum_nonneg fun n => le_of_lt (measure_of_restrictNonposSeq h _ (hn n))

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : s.totalVariation ≪ μ.ennrealToMeasure
⊢ s ≪ᵥ μ

Tactic:
refine VectorMeasure.AbsolutelyContinuous.mk fun S hS₁ hS₂ => ?_

Goal state after:
case mpr
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : s.totalVariation ≪ μ.ennrealToMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : μ S = 0
⊢ s S = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
h₁ : ∀ (n : ℕ), MeasurableSet (i ∩ f n)
⊢ Pairwise (Disjoint on fun n ↦ i ∩ f n)

Tactic:
intro n m hnm

Goal state after:
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
h₁ : ∀ (n : ℕ), MeasurableSet (i ∩ f n)
n m : ℕ
hnm : n ≠ m
⊢ (Disjoint on fun n ↦ i ∩ f n) n m
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
𝕜 : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
hf : Integrable f μ
i : Set α
hi : MeasurableSet i
⊢ ∫ (x : α) in i, (r • f) x ∂μ = (r • μ.withDensityᵥ f) i

Tactic:
_root_.smul_apply,

Goal state after:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
𝕜 : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
hf : Integrable f μ
i : Set α
hi : MeasurableSet i
⊢ ∫ (x : α) in i, (r • f) x ∂μ = r • (μ.withDensityᵥ f) i
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
h₁ : ∀ (n : ℕ), MeasurableSet (i ∩ f n)
h₂ : Pairwise (Disjoint on fun n ↦ i ∩ f n)
h : ∀ (n : ℕ), 0 ≤ s (i ∩ f n)
⊢ Summable fun n ↦ NNReal.mk (s (i ∩ f n)) ⋯

Tactic:
· exact (NNReal.summable_mk h).2 (s.m_iUnion h₁ h₂).summable

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : Integrable f μ
hg : Integrable g μ
hfg : μ.withDensityᵥ f = μ.withDensityᵥ g
i : Set α
hi : MeasurableSet i
x✝ : μ i < ∞
⊢ ∫ (x : α) in i, f x ∂μ = ∫ (x : α) in i, g x ∂μ

Tactic:
rw [← withDensityᵥ_apply hf hi, hfg, withDensityᵥ_apply hg hi]

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 μ
r : ℝ≥0
⊢ (r • s).toJordanDecomposition.negPart.HaveLebesgueDecomposition μ

Tactic:
rw [toJordanDecomposition_smul, JordanDecomposition.smul_negPart]

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.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
⊢ ∫ (x : α) in i, (f x).toReal ∂μ = (μ.withDensity f).toSignedMeasure i

Tactic:
toSignedMeasure_apply_measurable hi,

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 : α) in i, (f x).toReal ∂μ = (μ.withDensity f).real i
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 =
    (μ.withDensity fun x ↦ ENNReal.ofReal (f x)).toSignedMeasure i -
      (μ.withDensity fun x ↦ ENNReal.ofReal (-f x)).toSignedMeasure i

Tactic:
toSignedMeasure_apply_measurable hi,

Goal state after:
α : 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 =
    (μ.withDensity fun x ↦ ENNReal.ofReal (f x)).real i -
      (μ.withDensity fun x ↦ ENNReal.ofReal (-f x)).toSignedMeasure i
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 =
    (μ.withDensity fun x ↦ ENNReal.ofReal (f x)).real i -
      (μ.withDensity fun x ↦ ENNReal.ofReal (-f x)).toSignedMeasure i

Tactic:
toSignedMeasure_apply_measurable hi,

Goal state after:
α : 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 =
    (μ.withDensity fun x ↦ ENNReal.ofReal (f x)).real i - (μ.withDensity fun x ↦ ENNReal.ofReal (-f x)).real 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.real i - s.toJordanDecomposition.negPart.real i =
    s.toJordanDecomposition.posPart.toSignedMeasure i - s.toJordanDecomposition.negPart.toSignedMeasure i

Tactic:
toSignedMeasure_apply_measurable hi,

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.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.toSignedMeasure 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.real i - s.toJordanDecomposition.negPart.real i =
    s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.toSignedMeasure i

Tactic:
toSignedMeasure_apply_measurable hi,

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.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real 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 ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
this✝ : IsFiniteMeasure (μ.withDensity fun x ↦ ENNReal.ofReal (f x))
this : IsFiniteMeasure (μ.withDensity fun x ↦ ENNReal.ofReal ((-f) x))
i : Set α
hi : MeasurableSet i
⊢ (t + μ.withDensityᵥ f) i =
    (t.toJordanDecomposition.posPart + μ.withDensity fun x ↦ ENNReal.ofReal (f x)).toSignedMeasure i -
      (t.toJordanDecomposition.negPart + μ.withDensity fun x ↦ ENNReal.ofReal (-f x)).toSignedMeasure i

Tactic:
toSignedMeasure_apply_measurable hi,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
this✝ : IsFiniteMeasure (μ.withDensity fun x ↦ ENNReal.ofReal (f x))
this : IsFiniteMeasure (μ.withDensity fun x ↦ ENNReal.ofReal ((-f) x))
i : Set α
hi : MeasurableSet i
⊢ (t + μ.withDensityᵥ f) i =
    (t.toJordanDecomposition.posPart + μ.withDensity fun x ↦ ENNReal.ofReal (f x)).real i -
      (t.toJordanDecomposition.negPart + μ.withDensity fun x ↦ ENNReal.ofReal (-f x)).toSignedMeasure 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 ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
this✝ : IsFiniteMeasure (μ.withDensity fun x ↦ ENNReal.ofReal (f x))
this : IsFiniteMeasure (μ.withDensity fun x ↦ ENNReal.ofReal ((-f) x))
i : Set α
hi : MeasurableSet i
⊢ (t + μ.withDensityᵥ f) i =
    (t.toJordanDecomposition.posPart + μ.withDensity fun x ↦ ENNReal.ofReal (f x)).real i -
      (t.toJordanDecomposition.negPart + μ.withDensity fun x ↦ ENNReal.ofReal (-f x)).toSignedMeasure i

Tactic:
toSignedMeasure_apply_measurable hi,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
this✝ : IsFiniteMeasure (μ.withDensity fun x ↦ ENNReal.ofReal (f x))
this : IsFiniteMeasure (μ.withDensity fun x ↦ ENNReal.ofReal ((-f) x))
i : Set α
hi : MeasurableSet i
⊢ (t + μ.withDensityᵥ f) i =
    (t.toJordanDecomposition.posPart + μ.withDensity fun x ↦ ENNReal.ofReal (f x)).real i -
      (t.toJordanDecomposition.negPart + μ.withDensity fun x ↦ ENNReal.ofReal (-f x)).real i
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Goal state before:
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:
simpa using fun i hi ↦ (hf i hi).2.ne

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

Goal state before:
pp: α : 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
this : ∀ᵐ (x : α) ∂μ.restrict s, ‖{x | ‖f i x‖₊ < C}.indicator (f i) x‖ ≤ ↑C
⊢ ENNReal.ofReal ↑C * μ (univ ∩ s) ^ p.toReal⁻¹ ≤ ↑C * μ s ^ (1 / p.toReal)

Tactic:
Set.univ_inter,

Goal state after:
α : 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
this : ∀ᵐ (x : α) ∂μ.restrict s, ‖{x | ‖f i x‖₊ < C}.indicator (f i) x‖ ≤ ↑C
⊢ ENNReal.ofReal ↑C * μ s ^ p.toReal⁻¹ ≤ ↑C * μ s ^ (1 / p.toReal)
Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed

Goal state before:
pp: Ω : Type u_1
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : TopologicalSpace Ω
inst✝³ : HasOuterApproxClosed Ω
inst✝² : BorelSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ∀ (f : Ω →ᵇ ℝ), ∫ (x : Ω), f x ∂μ = ∫ (x : Ω), f x ∂ν
f : Ω →ᵇ ℝ≥0
⊢ (∫⁻ (x : Ω), ↑(f x) ∂μ).toReal = (∫⁻ (x : Ω), ↑(f x) ∂ν).toReal

Tactic:
toReal_lintegral_coe_eq_integral f μ,

Goal state after:
Ω : Type u_1
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : TopologicalSpace Ω
inst✝³ : HasOuterApproxClosed Ω
inst✝² : BorelSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ∀ (f : Ω →ᵇ ℝ), ∫ (x : Ω), f x ∂μ = ∫ (x : Ω), f x ∂ν
f : Ω →ᵇ ℝ≥0
⊢ ∫ (x : Ω), ↑(f x) ∂μ = (∫⁻ (x : Ω), ↑(f x) ∂ν).toReal