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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] -s
hw₁ : s w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
⊢ s v = 0

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] -s
hw₁ : s w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
⊢ s v = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : 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 : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ v → 0 j ≤ s j
hs : s (u ∆ v) = 0
⊢ s (u \ v) = 0 ∧ s (v \ u) = 0

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

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:
]

Goal state after:
α : 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 : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ v → 0 j ≤ s j
hs : s (u ∆ v) = 0
⊢ s (u \ v) = 0 ∧ s (v \ u) = 0

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

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
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : 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 : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ v → 0 j ≤ s j
hs : s (u \ v) + s (v \ u) = 0
a : 0 (u \ v) ≤ s (u \ v)
b : 0 (v \ u) ≤ s (v \ u)
⊢ s (u \ v) = 0 ∧ s (v \ u) = 0

Tactic:
]

Goal state after:
α : 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 : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ v → 0 j ≤ s j
hs : s (u \ v) + s (v \ u) = 0
a : 0 (u \ v) ≤ s (u \ v)
b : 0 (v \ u) ≤ s (v \ u)
⊢ s (u \ v) = 0 ∧ s (v \ u) = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : 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 : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ v → 0 j ≤ s j
hs : s (u \ v) + s (v \ u) = 0
a : 0 ≤ s (u \ v)
b : 0 ≤ s (v \ u)
⊢ s (u \ v) = 0 ∧ s (v \ u) = 0

Tactic:
]

Goal state after:
α : 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 : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ v → 0 j ≤ s j
hs : s (u \ v) + s (v \ u) = 0
a : 0 ≤ s (u \ v)
b : 0 ≤ s (v \ u)
⊢ s (u \ v) = 0 ∧ s (v \ u) = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

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

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : 0 ≤[u] -s
hsv : s ≤[v] 0
hs : s (u ∆ v) = 0
⊢ s (u \ v) = 0 ∧ s (v \ u) = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : 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
⊢ s (u \ v) = 0 ∧ s (v \ u) = 0

Tactic:
]

Goal state after:
α : 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
⊢ s (u \ v) = 0 ∧ s (v \ u) = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

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

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] s
hsv : 0 ≤[v] s
hs : s (u ∆ v) = 0
⊢ w ∩ u ∆ v ⊆ u ∆ v
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] s
hsv : 0 ≤[v] s
hs : s (u ∆ v) = 0
hwuv : s ((w ∩ u) ∆ (w ∩ v)) = 0
huv : s ((w ∩ u) \ (w ∩ v)) = 0
hvu : s ((w ∩ v) \ (w ∩ u)) = 0
⊢ s (w ∩ v) = s (w ∩ v)

Tactic:
]

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

Goal state before:
pp: case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : OrderClosedTopology M
v w : VectorMeasure α M
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (b : β), MeasurableSet (f b)
hf₂ : ∀ (b : β), v ≤[f b] w
val✝ : Encodable β
⊢ v ≤[⋃ i, ⋃ b ∈ Encodable.decode₂ β i, f b] w

Tactic:
]

Goal state after:
case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : OrderClosedTopology M
v w : VectorMeasure α M
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (b : β), MeasurableSet (f b)
hf₂ : ∀ (b : β), v ≤[f b] w
val✝ : Encodable β
⊢ v ≤[⋃ i, ⋃ b ∈ Encodable.decode₂ β i, f b] w
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

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

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] -s
hsv : s ≤[v] 0
hs : s (u ∆ v) = 0
⊢ s (w ∩ u) = s (w ∩ v)
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

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

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] -s
hsv : 0 ≤[v] -s
hs : s (u ∆ v) = 0
⊢ s (w ∩ u) = s (w ∩ v)
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

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

Tactic:
]

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.toSignedMeasure = j₂.negPart.toSignedMeasure
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
hi₁ : MeasurableSet i
hi₂ : v ≤[i] w
hj₁ : MeasurableSet j
hj₂ : v ≤[j] w
⊢ v ≤[⋃ b, bif b then i else j] w

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
hi₁ : MeasurableSet i
hi₂ : v ≤[i] w
hj₁ : MeasurableSet j
hj₂ : v ≤[j] w
⊢ v ≤[⋃ b, bif b then i else j] w
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.toSignedMeasure = j₂.toSignedMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : j₁.toSignedMeasure ≤[S] 0
hS₃ : 0 ≤[Sᶜ] j₁.toSignedMeasure
hS₄ : j₁.posPart S = 0
hS₅ : j₁.negPart Sᶜ = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : j₁.toSignedMeasure ≤[T] 0
hT₃ : 0 ≤[Tᶜ] j₁.toSignedMeasure
hT₄ : j₂.posPart T = 0
hT₅ : j₂.negPart Tᶜ = 0
⊢ j₁ = j₂

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.toSignedMeasure = j₂.toSignedMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : j₁.toSignedMeasure ≤[S] 0
hS₃ : 0 ≤[Sᶜ] j₁.toSignedMeasure
hS₄ : j₁.posPart S = 0
hS₅ : j₁.negPart Sᶜ = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : j₁.toSignedMeasure ≤[T] 0
hT₃ : 0 ≤[Tᶜ] j₁.toSignedMeasure
hT₄ : j₂.posPart T = 0
hT₅ : j₂.negPart Tᶜ = 0
⊢ j₁ = j₂
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v : VectorMeasure α M
i : Set α
hi₂ : 0 ≤[i] v
hi₁ : ¬MeasurableSet i
⊢ 0 ≤ 0

Tactic:
]

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

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v : VectorMeasure α M
i : Set α
hi₂ : v ≤[i] 0
hi₁ : ¬MeasurableSet i
⊢ 0 ≤ 0

Tactic:
]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v : VectorMeasure α M
i : Set α
hi : ¬MeasurableSet i
⊢ 0 ≤ 0

Tactic:
]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : LinearOrder M
v : VectorMeasure α M
i : Set α
hi : ¬∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → v j ≤ 0 j
hi₁ : MeasurableSet i
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ 0 < v j

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : LinearOrder M
v : VectorMeasure α M
i : Set α
hi : ¬∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → v j ≤ 0 j
hi₁ : MeasurableSet i
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ 0 < v j
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : AddLeftMono M
inst✝ : ContinuousAdd M
x✝² x✝¹ x✝ : VectorMeasure α M
h : x✝¹ ≤ x✝
i : Set α
hi : MeasurableSet i
⊢ x✝² i + x✝ i ≤ x✝² i + x✝ i

Tactic:
]

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

Goal state before:
pp: α : 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 < ε
δ : ℝ
hδpos : 0 < δ
hδ : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ 2 * ENNReal.ofReal (ε / 2)
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
⊢ ENNReal.ofReal ε ≤ ENNReal.ofReal ε

pp: case ha₀
α : 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 < ε
δ : ℝ
hδpos : 0 < δ
hδ : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ 2 * ENNReal.ofReal (ε / 2)
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
⊢ 2 ≠ 0

pp: case ha
α : 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 < ε
δ : ℝ
hδpos : 0 < δ
hδ : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ 2 * ENNReal.ofReal (ε / 2)
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
⊢ 2 ≠ ∞

Tactic:
]

Goal state after:
case ha₀
α : 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 < ε
δ : ℝ
hδpos : 0 < δ
hδ : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ 2 * ENNReal.ofReal (ε / 2)
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
⊢ 2 ≠ 0

case ha
α : 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 < ε
δ : ℝ
hδpos : 0 < δ
hδ : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ 2 * ENNReal.ofReal (ε / 2)
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
⊢ 2 ≠ ∞
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.toSignedMeasure = j₂.toSignedMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : j₁.toSignedMeasure ≤[S] 0
hS₃ : 0 ≤[Sᶜ] j₁.toSignedMeasure
hS₄ : j₁.posPart S = 0
hS₅ : j₁.negPart Sᶜ = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : j₁.toSignedMeasure ≤[T] 0
hT₃ : 0 ≤[Tᶜ] j₁.toSignedMeasure
hT₄ : j₂.posPart T = 0
hT₅ : j₂.negPart Tᶜ = 0
hST₁ : j₁.toSignedMeasure (symmDiff Sᶜ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
⊢ j₁.posPart.real i = j₁.posPart.real (i ∩ Sᶜ)

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.toSignedMeasure = j₂.toSignedMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : j₁.toSignedMeasure ≤[S] 0
hS₃ : 0 ≤[Sᶜ] j₁.toSignedMeasure
hS₄ : j₁.posPart S = 0
hS₅ : j₁.negPart Sᶜ = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : j₁.toSignedMeasure ≤[T] 0
hT₃ : 0 ≤[Tᶜ] j₁.toSignedMeasure
hT₄ : j₂.posPart T = 0
hT₅ : j₂.negPart Tᶜ = 0
hST₁ : j₁.toSignedMeasure (symmDiff Sᶜ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
⊢ j₁.posPart.real i = j₁.posPart.real (i ∩ Sᶜ)
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
M : Type u_6
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
s : Set α
hs : w s = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
N : Type u_6
inst✝² : AddCommGroup N
inst✝¹ : TopologicalSpace N
inst✝ : IsTopologicalAddGroup N
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
s : Set α
hs : -w s = 0
⊢ v s = 0

Tactic:
neg_eq_zero

Goal state after:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
N : Type u_6
inst✝² : AddCommGroup N
inst✝¹ : TopologicalSpace N
inst✝ : IsTopologicalAddGroup N
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
s : Set α
hs : w s = 0
⊢ v s = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
N : Type u_6
inst✝² : AddCommGroup N
inst✝¹ : TopologicalSpace N
inst✝ : IsTopologicalAddGroup N
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
s : Set α
hs : w s = 0
⊢ v s = 0

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
N : Type u_6
inst✝² : AddCommGroup N
inst✝¹ : TopologicalSpace N
inst✝ : IsTopologicalAddGroup N
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
s : Set α
hs : w s = 0
⊢ v s = 0
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
hℒp : MemLp f p μ
right✝ : eLpNorm f p μ < ∞
f' : α → β
hf' : StronglyMeasurable f'
heq : f =ᵐ[μ] f'
δ : ℝ
hδpos : 0 < δ
hδ : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f') p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
⊢ eLpNorm f p (μ.restrict s) = eLpNorm f' p (μ.restrict s)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
hℒp : MemLp f p μ
right✝ : eLpNorm f p μ < ∞
f' : α → β
hf' : StronglyMeasurable f'
heq : f =ᵐ[μ] f'
δ : ℝ
hδpos : 0 < δ
hδ : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f') p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
⊢ eLpNorm f p (μ.restrict s) = eLpNorm f' p (μ.restrict s)
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
inst✝ : ContinuousAdd M
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
hv₁ : v₁ ≪ᵥ w
hv₂ : v₂ ≪ᵥ w
s : Set α
hs : w s = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
M : Type u_6
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
hv₁ : v₁ ≪ᵥ w
hv₂ : v₂ ≪ᵥ w
s : Set α
hs : w s = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
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
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : AddCommMonoid N
inst✝¹ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
inst✝ : MeasureSpace β
h : v ≪ᵥ w
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
hws : w (f ⁻¹' s) = 0
⊢ v (f ⁻¹' s) = 0

Tactic:
]

Goal state after:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : AddCommMonoid N
inst✝¹ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
inst✝ : MeasureSpace β
h : v ≪ᵥ w
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
hws : w (f ⁻¹' s) = 0
⊢ v (f ⁻¹' 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 α := i \ ⋃ l, s.restrictNonposSeq i l
hA : A = i \ ⋃ l, s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun n ↦ s.findExistsOneDivLT (i \ ⋃ k, ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : s i = s A + ∑' (l : ℕ), s (s.restrictNonposSeq i l)
⊢ s A ≤ s A + ∑' (l : ℕ), s (s.restrictNonposSeq i l)

Tactic:
]

Goal state after:
α : 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 α := i \ ⋃ l, s.restrictNonposSeq i l
hA : A = i \ ⋃ l, s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun n ↦ s.findExistsOneDivLT (i \ ⋃ k, ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : s i = s A + ∑' (l : ℕ), s (s.restrictNonposSeq i l)
⊢ s A ≤ s A + ∑' (l : ℕ), s (s.restrictNonposSeq i l)
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : AddCommMonoid N
inst✝¹ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
inst✝ : MeasureSpace β
h : v ≪ᵥ w
f : α → β
hf : ¬Measurable f
s : Set β
a✝ : (w.map f) s = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case mp
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
μ : VectorMeasure α ℝ≥0∞
h : ∀ ⦃s : Set α⦄, μ.ennrealToMeasure s = 0 → v s = 0
s : Set α
hmeas : MeasurableSet s
hs : μ s = 0
⊢ μ s = μ s

Tactic:
]

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

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
μ : VectorMeasure α ℝ≥0∞
h : v ≪ᵥ μ
s : Set α
hs : μ s = 0
hmeas : MeasurableSet s
⊢ v s = 0

Tactic:
]

Goal state after:
case pos
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
μ : VectorMeasure α ℝ≥0∞
h : v ≪ᵥ μ
s : Set α
hs : μ s = 0
hmeas : MeasurableSet s
⊢ v s = 0