case intro.intro.intro
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
hf₁ : ∀ (n : ℕ), f n ∈ measureOfNegatives s
⊢ ∃ i, MeasurableSet i ∧ restrict 0 i ≤ restrict s i ∧ restrict s (iᶜ) ≤ restrict 0 (iᶜ)
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
⊢ ∃ i, MeasurableSet i ∧ restrict 0 i ≤ restrict s i ∧ restrict s (iᶜ) ≤ restrict 0 (iᶜ)
obtain ⟨f, _, hf₂, hf₁⟩ :=
  exists_seq_tendsto_sInf ⟨0, @zero_mem_measureOfNegatives _ _ s⟩ bddBelow_measureOfNegatives
case intro.intro.intro
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
⊢ ∃ i, MeasurableSet i ∧ restrict 0 i ≤ restrict s i ∧ restrict s (iᶜ) ≤ restrict 0 (iᶜ)
case intro.intro.intro
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
hf₁ : ∀ (n : ℕ), f n ∈ measureOfNegatives s
⊢ ∃ i, MeasurableSet i ∧ restrict 0 i ≤ restrict s i ∧ restrict s (iᶜ) ≤ restrict 0 (iᶜ)
choose B hB using hf₁
case intro.intro.intro
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
⊢ ∃ i, MeasurableSet i ∧ restrict 0 i ≤ restrict s i ∧ restrict s (iᶜ) ≤ restrict 0 (iᶜ)
case intro.intro.intro
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
⊢ ∃ i, MeasurableSet i ∧ restrict 0 i ≤ restrict s i ∧ restrict s (iᶜ) ≤ restrict 0 (iᶜ)
have hB₁ : ∀ n, MeasurableSet (B n) := fun n => (hB n).1.1
case intro.intro.intro
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
⊢ ∃ i, MeasurableSet i ∧ restrict 0 i ≤ restrict s i ∧ restrict s (iᶜ) ≤ restrict 0 (iᶜ)
case intro.intro.intro
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
⊢ ∃ i, MeasurableSet i ∧ restrict 0 i ≤ restrict s i ∧ restrict s (iᶜ) ≤ restrict 0 (iᶜ)
have hB₂ : ∀ n, s ≤[B n] 0 := fun n => (hB n).1.2
case intro.intro.intro
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
⊢ ∃ i, MeasurableSet i ∧ restrict 0 i ≤ restrict s i ∧ restrict s (iᶜ) ≤ restrict 0 (iᶜ)
case intro.intro.intro
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
⊢ ∃ i, MeasurableSet i ∧ restrict 0 i ≤ restrict s i ∧ restrict s (iᶜ) ≤ restrict 0 (iᶜ)
set A := ⋃ n, B n with hA
case intro.intro.intro
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
⊢ ∃ i, MeasurableSet i ∧ restrict 0 i ≤ restrict s i ∧ restrict s (iᶜ) ≤ restrict 0 (iᶜ)
case intro.intro.intro
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
⊢ ∃ i, MeasurableSet i ∧ restrict 0 i ≤ restrict s i ∧ restrict s (iᶜ) ≤ restrict 0 (iᶜ)
have hA₁ : MeasurableSet A := MeasurableSet.iUnion hB₁
case intro.intro.intro
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : restrict s A ≤ restrict 0 A
⊢ ∃ i, MeasurableSet i ∧ restrict 0 i ≤ restrict s i ∧ restrict s (iᶜ) ≤ restrict 0 (iᶜ)
case intro.intro.intro
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
⊢ ∃ i, MeasurableSet i ∧ restrict 0 i ≤ restrict s i ∧ restrict s (iᶜ) ≤ restrict 0 (iᶜ)
have hA₂ : s ≤[A] 0 := restrict_le_restrict_iUnion _ _ hB₁ hB₂
case intro.intro.intro
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : restrict s A ≤ restrict 0 A
hA₃ : ↑s A = sInf (measureOfNegatives s)
⊢ restrict 0 (Aᶜ) ≤ restrict s (Aᶜ)
case intro.intro.intro
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : restrict s A ≤ restrict 0 A
hA₃ : ↑s A = sInf (measureOfNegatives s)
⊢ ∃ i, MeasurableSet i ∧ restrict 0 i ≤ restrict s i ∧ restrict s (iᶜ) ≤ restrict 0 (iᶜ)
refine' ⟨Aᶜ, hA₁.compl, _, (compl_compl A).symm ▸ hA₂⟩
case intro.intro.intro
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : restrict s A ≤ restrict 0 A
hA₃ : ↑s A = sInf (measureOfNegatives s)
⊢ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ Aᶜ → ↑0 j ≤ ↑s j
case intro.intro.intro
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : restrict s A ≤ restrict 0 A
hA₃ : ↑s A = sInf (measureOfNegatives s)
⊢ restrict 0 (Aᶜ) ≤ restrict s (Aᶜ)
rw [restrict_le_restrict_iff _ _ hA₁.compl]
case intro.intro.intro
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : restrict s A ≤ restrict 0 A
hA₃ : ↑s A = sInf (measureOfNegatives s)
C : Set α
a✝ : MeasurableSet C
hC₁ : C ⊆ Aᶜ
⊢ ↑0 C ≤ ↑s C
case intro.intro.intro
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : restrict s A ≤ restrict 0 A
hA₃ : ↑s A = sInf (measureOfNegatives s)
⊢ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ Aᶜ → ↑0 j ≤ ↑s j
intro C _ hC₁
case intro.intro.intro
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : restrict s A ≤ restrict 0 A
hA₃ : ↑s A = sInf (measureOfNegatives s)
C : Set α
a✝ : MeasurableSet C
hC₁ : C ⊆ Aᶜ
hC₂ : ↑s C < ↑0 C
⊢ False
case intro.intro.intro
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : restrict s A ≤ restrict 0 A
hA₃ : ↑s A = sInf (measureOfNegatives s)
C : Set α
a✝ : MeasurableSet C
hC₁ : C ⊆ Aᶜ
⊢ ↑0 C ≤ ↑s C
by_contra' hC₂
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : restrict s A ≤ restrict 0 A
hA₃ : ↑s A = sInf (measureOfNegatives s)
C : Set α
a✝ : MeasurableSet C
hC₁ : C ⊆ Aᶜ
hC₂ : ↑s C < ↑0 C
D : Set α
hD₁ : MeasurableSet D
hD : D ⊆ C
hD₂ : restrict s D ≤ restrict 0 D
hD₃ : ↑s D < 0
⊢ False
case intro.intro.intro
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : restrict s A ≤ restrict 0 A
hA₃ : ↑s A = sInf (measureOfNegatives s)
C : Set α
a✝ : MeasurableSet C
hC₁ : C ⊆ Aᶜ
hC₂ : ↑s C < ↑0 C
⊢ False
rcases exists_subset_restrict_nonpos hC₂ with ⟨D, hD₁, hD, hD₂, hD₃⟩
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : restrict s A ≤ restrict 0 A
hA₃ : ↑s A = sInf (measureOfNegatives s)
C : Set α
a✝ : MeasurableSet C
hC₁ : C ⊆ Aᶜ
hC₂ : ↑s C < ↑0 C
D : Set α
hD₁ : MeasurableSet D
hD : D ⊆ C
hD₂ : restrict s D ≤ restrict 0 D
hD₃ : ↑s D < 0
this : ↑s (A ∪ D) < sInf (measureOfNegatives s)
⊢ False
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : restrict s A ≤ restrict 0 A
hA₃ : ↑s A = sInf (measureOfNegatives s)
C : Set α
a✝ : MeasurableSet C
hC₁ : C ⊆ Aᶜ
hC₂ : ↑s C < ↑0 C
D : Set α
hD₁ : MeasurableSet D
hD : D ⊆ C
hD₂ : restrict s D ≤ restrict 0 D
hD₃ : ↑s D < 0
⊢ False
have : s (A ∪ D) < sInf s.measureOfNegatives := by
  rw [← hA₃,
    of_union (Set.disjoint_of_subset_right (Set.Subset.trans hD hC₁) disjoint_compl_right) hA₁
      hD₁]
  linarith
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : restrict s A ≤ restrict 0 A
hA₃ : ↑s A = sInf (measureOfNegatives s)
C : Set α
a✝ : MeasurableSet C
hC₁ : C ⊆ Aᶜ
hC₂ : ↑s C < ↑0 C
D : Set α
hD₁ : MeasurableSet D
hD : D ⊆ C
hD₂ : restrict s D ≤ restrict 0 D
hD₃ : ↑s D < 0
this : ↑s (A ∪ D) < sInf (measureOfNegatives s)
⊢ sInf (measureOfNegatives s) ≤ ↑s (A ∪ D)
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : restrict s A ≤ restrict 0 A
hA₃ : ↑s A = sInf (measureOfNegatives s)
C : Set α
a✝ : MeasurableSet C
hC₁ : C ⊆ Aᶜ
hC₂ : ↑s C < ↑0 C
D : Set α
hD₁ : MeasurableSet D
hD : D ⊆ C
hD₂ : restrict s D ≤ restrict 0 D
hD₃ : ↑s D < 0
this : ↑s (A ∪ D) < sInf (measureOfNegatives s)
⊢ False
refine' not_le.2 this _
case intro.intro.intro.intro.intro.intro.intro.refine'_1
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : restrict s A ≤ restrict 0 A
hA₃ : ↑s A = sInf (measureOfNegatives s)
C : Set α
a✝ : MeasurableSet C
hC₁ : C ⊆ Aᶜ
hC₂ : ↑s C < ↑0 C
D : Set α
hD₁ : MeasurableSet D
hD : D ⊆ C
hD₂ : restrict s D ≤ restrict 0 D
hD₃ : ↑s D < 0
this : ↑s (A ∪ D) < sInf (measureOfNegatives s)
⊢ MeasurableSet (A ∪ D)

case intro.intro.intro.intro.intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : restrict s A ≤ restrict 0 A
hA₃ : ↑s A = sInf (measureOfNegatives s)
C : Set α
a✝ : MeasurableSet C
hC₁ : C ⊆ Aᶜ
hC₂ : ↑s C < ↑0 C
D : Set α
hD₁ : MeasurableSet D
hD : D ⊆ C
hD₂ : restrict s D ≤ restrict 0 D
hD₃ : ↑s D < 0
this : ↑s (A ∪ D) < sInf (measureOfNegatives s)
⊢ restrict s (A ∪ D) ≤ restrict 0 (A ∪ D)
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : restrict s A ≤ restrict 0 A
hA₃ : ↑s A = sInf (measureOfNegatives s)
C : Set α
a✝ : MeasurableSet C
hC₁ : C ⊆ Aᶜ
hC₂ : ↑s C < ↑0 C
D : Set α
hD₁ : MeasurableSet D
hD : D ⊆ C
hD₂ : restrict s D ≤ restrict 0 D
hD₃ : ↑s D < 0
this : ↑s (A ∪ D) < sInf (measureOfNegatives s)
⊢ sInf (measureOfNegatives s) ≤ ↑s (A ∪ D)
refine' csInf_le bddBelow_measureOfNegatives ⟨A ∪ D, ⟨_, _⟩, rfl⟩
case a
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : restrict s A ≤ restrict 0 A
⊢ ↑s A ≤ sInf (measureOfNegatives s)

case a
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : restrict s A ≤ restrict 0 A
⊢ sInf (measureOfNegatives s) ≤ ↑s A
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : restrict s A ≤ restrict 0 A
⊢ ↑s A = sInf (measureOfNegatives s)
apply le_antisymm
case a
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : restrict s A ≤ restrict 0 A
n : ℕ
⊢ (fun x => ↑s A) n ≤ f n
case a
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : restrict s A ≤ restrict 0 A
⊢ ↑s A ≤ sInf (measureOfNegatives s)
refine' le_of_tendsto_of_tendsto tendsto_const_nhds hf₂ (eventually_of_forall fun n => _)
case a
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : restrict s A ≤ restrict 0 A
n : ℕ
⊢ (fun x => ↑s ((⋃ (i : ℕ), B i) \ B n) + ↑s (B n)) n ≤ ↑s (B n)

α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : restrict s A ≤ restrict 0 A
n : ℕ
⊢ MeasurableSet ((⋃ (i : ℕ), B i) \ B n)
case a
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : restrict s A ≤ restrict 0 A
n : ℕ
⊢ (fun x => ↑s A) n ≤ f n
rw [← (hB n).2, hA, ← Set.diff_union_of_subset (Set.subset_iUnion _ n),
  of_union Set.disjoint_sdiff_left _ (hB₁ n)]
case a
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : restrict s A ≤ restrict 0 A
n : ℕ
⊢ ↑s ((⋃ (i : ℕ), B i) \ B n) ≤ 0
case a
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : restrict s A ≤ restrict 0 A
n : ℕ
⊢ (fun x => ↑s ((⋃ (i : ℕ), B i) \ B n) + ↑s (B n)) n ≤ ↑s (B n)
refine' add_le_of_nonpos_left _
case a
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : restrict s A ≤ restrict 0 A
n : ℕ
this : restrict s A ≤ restrict 0 A
⊢ ↑s ((⋃ (i : ℕ), B i) \ B n) ≤ 0
case a
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : restrict s A ≤ restrict 0 A
n : ℕ
⊢ ↑s ((⋃ (i : ℕ), B i) \ B n) ≤ 0
have : s ≤[A] 0 :=
  restrict_le_restrict_iUnion _ _ hB₁ fun m =>
    let ⟨_, h⟩ := (hB m).1
    h
case a
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : restrict s A ≤ restrict 0 A
n : ℕ
this : restrict s A ≤ restrict 0 A
⊢ MeasurableSet (⋃ (i : ℕ), B i)
case a
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : restrict s A ≤ restrict 0 A
n : ℕ
this : restrict s A ≤ restrict 0 A
⊢ ↑s ((⋃ (i : ℕ), B i) \ B n) ≤ 0
refine'
  nonpos_of_restrict_le_zero _ (restrict_le_zero_subset _ _ (Set.diff_subset _ _) this)
no goals
case a
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : restrict s A ≤ restrict 0 A
n : ℕ
this : restrict s A ≤ restrict 0 A
⊢ MeasurableSet (⋃ (i : ℕ), B i)
exact MeasurableSet.iUnion hB₁
no goals
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : restrict s A ≤ restrict 0 A
n : ℕ
⊢ MeasurableSet ((⋃ (i : ℕ), B i) \ B n)
exact (MeasurableSet.iUnion hB₁).diff (hB₁ n)
no goals
case a
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : restrict s A ≤ restrict 0 A
⊢ sInf (measureOfNegatives s) ≤ ↑s A
exact csInf_le bddBelow_measureOfNegatives ⟨A, ⟨hA₁, hA₂⟩, rfl⟩
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : restrict s A ≤ restrict 0 A
hA₃ : ↑s A = sInf (measureOfNegatives s)
C : Set α
a✝ : MeasurableSet C
hC₁ : C ⊆ Aᶜ
hC₂ : ↑s C < ↑0 C
D : Set α
hD₁ : MeasurableSet D
hD : D ⊆ C
hD₂ : restrict s D ≤ restrict 0 D
hD₃ : ↑s D < 0
⊢ ↑s A + ↑s D < ↑s A
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : restrict s A ≤ restrict 0 A
hA₃ : ↑s A = sInf (measureOfNegatives s)
C : Set α
a✝ : MeasurableSet C
hC₁ : C ⊆ Aᶜ
hC₂ : ↑s C < ↑0 C
D : Set α
hD₁ : MeasurableSet D
hD : D ⊆ C
hD₂ : restrict s D ≤ restrict 0 D
hD₃ : ↑s D < 0
⊢ ↑s (A ∪ D) < sInf (measureOfNegatives s)
rw [← hA₃,
  of_union (Set.disjoint_of_subset_right (Set.Subset.trans hD hC₁) disjoint_compl_right) hA₁
    hD₁]
no goals
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : restrict s A ≤ restrict 0 A
hA₃ : ↑s A = sInf (measureOfNegatives s)
C : Set α
a✝ : MeasurableSet C
hC₁ : C ⊆ Aᶜ
hC₂ : ↑s C < ↑0 C
D : Set α
hD₁ : MeasurableSet D
hD : D ⊆ C
hD₂ : restrict s D ≤ restrict 0 D
hD₃ : ↑s D < 0
⊢ ↑s A + ↑s D < ↑s A
linarith
no goals
case intro.intro.intro.intro.intro.intro.intro.refine'_1
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : restrict s A ≤ restrict 0 A
hA₃ : ↑s A = sInf (measureOfNegatives s)
C : Set α
a✝ : MeasurableSet C
hC₁ : C ⊆ Aᶜ
hC₂ : ↑s C < ↑0 C
D : Set α
hD₁ : MeasurableSet D
hD : D ⊆ C
hD₂ : restrict s D ≤ restrict 0 D
hD₃ : ↑s D < 0
this : ↑s (A ∪ D) < sInf (measureOfNegatives s)
⊢ MeasurableSet (A ∪ D)
exact hA₁.union hD₁
no goals
case intro.intro.intro.intro.intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.111089
inst✝³ : MeasurableSpace α
M : Type ?u.111095
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s✝ : SignedMeasure α
i j : Set α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf (measureOfNegatives s)))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : restrict s A ≤ restrict 0 A
hA₃ : ↑s A = sInf (measureOfNegatives s)
C : Set α
a✝ : MeasurableSet C
hC₁ : C ⊆ Aᶜ
hC₂ : ↑s C < ↑0 C
D : Set α
hD₁ : MeasurableSet D
hD : D ⊆ C
hD₂ : restrict s D ≤ restrict 0 D
hD₃ : ↑s D < 0
this : ↑s (A ∪ D) < sInf (measureOfNegatives s)
⊢ restrict s (A ∪ D) ≤ restrict 0 (A ∪ D)
exact restrict_le_restrict_union _ _ hA₁ hA₂ hD₁ hD₂