-- Mathlib/MeasureTheory/Decomposition/SignedHahn.lean
theorem bddBelow_measureOfNegatives : BddBelow s.measureOfNegatives

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
⊢ False

Tactic:
have h' : ∀ n : ℕ, ∃ y : ℝ, y ∈ s.measureOfNegatives ∧ y < -n := fun n => h (-n)

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
h' : ∀ (n : ℕ), ∃ y ∈ s.measureOfNegatives, y < -↑n
⊢ False

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -↑n
⊢ ∀ (n : ℕ), ∃ B, MeasurableSet B ∧ s ≤[B] 0 ∧ ↑s B < -↑n

Tactic:
intro n

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -↑n
n : ℕ
⊢ ∃ B, MeasurableSet B ∧ s ≤[B] 0 ∧ ↑s B < -↑n

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
⊢ BddBelow s.measureOfNegatives

Tactic:
simp_rw [BddBelow, Set.Nonempty, mem_lowerBounds]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
⊢ ∃ x, ∀ x_1 ∈ s.measureOfNegatives, x ≤ x_1

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
⊢ ∃ x, ∀ x_1 ∈ s.measureOfNegatives, x ≤ x_1

Tactic:
by_contra! h

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
⊢ False

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -↑n
B : ℕ → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), s ≤[B n] 0
h_lt : ∀ (n : ℕ), ↑s (B n) < -↑n
A : Set α := ⋃ n, B n
hA : A = ⋃ n, B n
n : ℕ
⊢ ↑s A ≤ ↑s (B n)

Tactic:
rw [hA, ← Set.diff_union_of_subset (Set.subset_iUnion _ n),
  of_union Set.disjoint_sdiff_left _ (hmeas n)]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -↑n
B : ℕ → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), s ≤[B n] 0
h_lt : ∀ (n : ℕ), ↑s (B n) < -↑n
A : Set α := ⋃ n, B n
hA : A = ⋃ n, B n
n : ℕ
⊢ ↑s ((⋃ i, B i) \ B n) + ↑s (B n) ≤ ↑s (B n)

α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -↑n
B : ℕ → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), s ≤[B n] 0
h_lt : ∀ (n : ℕ), ↑s (B n) < -↑n
A : Set α := ⋃ n, B n
hA : A = ⋃ n, B n
n : ℕ
⊢ MeasurableSet ((⋃ i, B i) \ B n)

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -↑n
B : ℕ → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), s ≤[B n] 0
h_lt : ∀ (n : ℕ), ↑s (B n) < -↑n
⊢ False

Tactic:
set A := ⋃ n, B n with hA

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -↑n
B : ℕ → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), s ≤[B n] 0
h_lt : ∀ (n : ℕ), ↑s (B n) < -↑n
A : Set α := ⋃ n, B n
hA : A = ⋃ n, B n
⊢ False

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
h' : ∀ (n : ℕ), ∃ y ∈ s.measureOfNegatives, y < -↑n
⊢ False

Tactic:
choose f hf using h'

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -↑n
⊢ False

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -↑n
n : ℕ
⊢ ∃ B, MeasurableSet B ∧ s ≤[B] 0 ∧ ↑s B < -↑n

Tactic:
rcases hf n with ⟨⟨B, ⟨hB₁, hBr⟩, hB₂⟩, hlt⟩

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -↑n
n : ℕ
hlt : f n < -↑n
B : Set α
hB₂ : ↑s B = f n
hB₁ : MeasurableSet B
hBr : s ≤[B] 0
⊢ ∃ B, MeasurableSet B ∧ s ≤[B] 0 ∧ ↑s B < -↑n

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -↑n
B : ℕ → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), s ≤[B n] 0
h_lt : ∀ (n : ℕ), ↑s (B n) < -↑n
A : Set α := ⋃ n, B n
hA : A = ⋃ n, B n
n : ℕ
⊢ MeasurableSet ((⋃ i, B i) \ B n)

Tactic:
exact (MeasurableSet.iUnion hmeas).diff (hmeas n)

Result:
no goals