-- Mathlib/MeasureTheory/Decomposition/SignedHahn.lean
theorem exists_subset_restrict_nonpos' (hi₁ : MeasurableSet i) (hi₂ : s i < 0)
    (hn : ¬∀ n : ℕ, ¬s ≤[i \ ⋃ l < n, restrictNonposSeq s i l] 0) :
    ∃ j : Set α, MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ s j < 0

Proof state:
case neg.h
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
h : ¬s ≤[i] 0
hn : ∃ n, s ≤[i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l] 0
k : ℕ := Nat.find hn
hk₂ : s ≤[i \ ⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l] 0
hmeas : MeasurableSet (⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
a : ℕ
x : α
⊢ x ∈ ⋃ (_ : a < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i a → x ∈ i

Tactic:
simp only [and_imp, exists_prop, Set.mem_iUnion]

Result:
case neg.h
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
h : ¬s ≤[i] 0
hn : ∃ n, s ≤[i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l] 0
k : ℕ := Nat.find hn
hk₂ : s ≤[i \ ⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l] 0
hmeas : MeasurableSet (⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
a : ℕ
x : α
⊢ a < k → x ∈ MeasureTheory.SignedMeasure.restrictNonposSeq s i a → x ∈ i

Proof state:
case h.e'_4.h.e'_7.h
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
h✝ : ¬s ≤[i] 0
hn : ∃ n, s ≤[i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l] 0
k : ℕ := Nat.find hn
hk₂ : s ≤[i \ ⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l] 0
hmeas : MeasurableSet (⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ∀ l < k, 0 ≤ ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
l : ℕ
h : l < k
x : α
⊢ x ∈ MeasureTheory.SignedMeasure.restrictNonposSeq s i l → l < k

Tactic:
exact fun _ => h

Result:
no goals

Proof state:
case h.e'_4.h.e'_7
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
h✝ : ¬s ≤[i] 0
hn : ∃ n, s ≤[i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l] 0
k : ℕ := Nat.find hn
hk₂ : s ≤[i \ ⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l] 0
hmeas : MeasurableSet (⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ∀ l < k, 0 ≤ ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
l : ℕ
h : ¬l < k
⊢ ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l = ∅

Tactic:
ext

Result:
case h.e'_4.h.e'_7.h
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
h✝ : ¬s ≤[i] 0
hn : ∃ n, s ≤[i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l] 0
k : ℕ := Nat.find hn
hk₂ : s ≤[i \ ⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l] 0
hmeas : MeasurableSet (⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ∀ l < k, 0 ≤ ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
l : ℕ
h : ¬l < k
x✝ : α
⊢ x✝ ∈ ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l ↔ x✝ ∈ ∅

Proof state:
case neg.hd
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
h : ¬s ≤[i] 0
hn : ∃ n, s ≤[i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l] 0
k : ℕ := Nat.find hn
hk₂ : s ≤[i \ ⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l] 0
hmeas : MeasurableSet (⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
a b : ℕ
hab : a ≠ b
x✝¹ : a < k
x✝ : b < k
⊢ Disjoint (MeasureTheory.SignedMeasure.restrictNonposSeq s i a) (MeasureTheory.SignedMeasure.restrictNonposSeq s i b)

Tactic:
exact restrictNonposSeq_disjoint hab

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
h : ¬s ≤[i] 0
hn : ∃ n, s ≤[i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l] 0
k : ℕ := Nat.find hn
hk₂ : s ≤[i \ ⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l] 0
hmeas : MeasurableSet (⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
l : ℕ
hl : l < k
⊢ MeasurableSet (⋃ k, ⋃ (_ : k < l), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)

Tactic:
exact
  MeasurableSet.iUnion fun _ =>
    MeasurableSet.iUnion fun _ => restrictNonposSeq_measurableSet _

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
h : ¬s ≤[i] 0
hn : ∃ n, s ≤[i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l] 0
k : ℕ := Nat.find hn
hk₂ : s ≤[i \ ⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l] 0
hmeas : MeasurableSet (⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ∀ l < k, 0 ≤ ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
l : ℕ
⊢ 0 ≤ ↑s (⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)

Tactic:
by_cases h : l < k

Result:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
h✝ : ¬s ≤[i] 0
hn : ∃ n, s ≤[i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l] 0
k : ℕ := Nat.find hn
hk₂ : s ≤[i \ ⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l] 0
hmeas : MeasurableSet (⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ∀ l < k, 0 ≤ ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
l : ℕ
h : l < k
⊢ 0 ≤ ↑s (⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)

case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
h✝ : ¬s ≤[i] 0
hn : ∃ n, s ≤[i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l] 0
k : ℕ := Nat.find hn
hk₂ : s ≤[i \ ⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l] 0
hmeas : MeasurableSet (⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ∀ l < k, 0 ≤ ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
l : ℕ
h : ¬l < k
⊢ 0 ≤ ↑s (⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)

Proof state:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
h✝ : ¬s ≤[i] 0
hn : ∃ n, s ≤[i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l] 0
k : ℕ := Nat.find hn
hk₂ : s ≤[i \ ⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l] 0
hmeas : MeasurableSet (⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ∀ l < k, 0 ≤ ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
l : ℕ
h : l < k
⊢ 0 ≤ ↑s (⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)

Tactic:
convert h₁ _ h

Result:
case h.e'_4.h.e'_7
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
h✝ : ¬s ≤[i] 0
hn : ∃ n, s ≤[i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l] 0
k : ℕ := Nat.find hn
hk₂ : s ≤[i \ ⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l] 0
hmeas : MeasurableSet (⋃ l, ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ∀ l < k, 0 ≤ ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
l : ℕ
h : l < k
⊢ ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l =
    MeasureTheory.SignedMeasure.restrictNonposSeq s i l