-- Mathlib/MeasureTheory/OuterMeasure/Basic.lean
theorem iUnion_nat_of_monotone_of_tsum_ne_top (m : OuterMeasure α) {s : ℕ → Set α}
    (h_mono : ∀ n, s n ⊆ s (n + 1)) (h0 : (∑' k, m (s (k + 1) \ s k)) ≠ ∞) :
    m (⋃ n, s n) = ⨆ n, m (s n)

Proof state:
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤
n : ℕ
h' : Monotone s
⊢ ∀ (i : ℕ), s i ⊆ s n ∪ ⋃ i, s (i + n + 1) \ s (i + n)

Tactic:
intro i x hx

Result:
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤
n : ℕ
h' : Monotone s
i : ℕ
x : α
hx : x ∈ s i
⊢ x ∈ s n ∪ ⋃ i, s (i + n + 1) \ s (i + n)

Proof state:
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤
n : ℕ
h' : Monotone s
x : α
this : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ m < j, x ∉ s m
hnj : n < j
⊢ j - (n + 1) + n + 1 = j

Tactic:
omega

Result:
no goals

Proof state:
case mk.intro.inr
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤
n : ℕ
h' : Monotone s
x : α
this : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ m < j, x ∉ s m
hnj : n < j
⊢ x ∈ s n ∪ ⋃ i, s (i + n + 1) \ s (i + n)

Tactic:
have : j - (n + 1) + n + 1 = j := by omega

Result:
case mk.intro.inr
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤
n : ℕ
h' : Monotone s
x : α
this✝ : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ m < j, x ∉ s m
hnj : n < j
this : j - (n + 1) + n + 1 = j
⊢ x ∈ s n ∪ ⋃ i, s (i + n + 1) \ s (i + n)

Proof state:
case mk.intro.inr.refine_1
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤
n : ℕ
h' : Monotone s
x : α
this✝ : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ m < j, x ∉ s m
hnj : n < j
this : j - (n + 1) + n + 1 = j
⊢ x ∈ s (j - (n + 1) + n + 1)

Tactic:
rwa [this]

Result:
no goals

Proof state:
case mk.intro
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤
n : ℕ
h' : Monotone s
x : α
this : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ m < j, x ∉ s m
⊢ x ∈ s n ∪ ⋃ i, s (i + n + 1) \ s (i + n)

Tactic:
rcases le_or_lt j n with hjn | hnj

Result:
case mk.intro.inl
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤
n : ℕ
h' : Monotone s
x : α
this : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ m < j, x ∉ s m
hjn : j ≤ n
⊢ x ∈ s n ∪ ⋃ i, s (i + n + 1) \ s (i + n)

case mk.intro.inr
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤
n : ℕ
h' : Monotone s
x : α
this : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ m < j, x ∉ s m
hnj : n < j
⊢ x ∈ s n ∪ ⋃ i, s (i + n + 1) \ s (i + n)

Proof state:
case mk.intro.inl
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤
n : ℕ
h' : Monotone s
x : α
this : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ m < j, x ∉ s m
hjn : j ≤ n
⊢ x ∈ s n ∪ ⋃ i, s (i + n + 1) \ s (i + n)

Tactic:
exact Or.inl (h' hjn hj)

Result:
no goals

Proof state:
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤
n : ℕ
⊢ m ((⋃ n, s n) \ s n) ≤ ∑' (k : ℕ), m (s (k + n + 1) \ s (k + n))

Tactic:
refine (m.mono ?_).trans (measure_iUnion_le _)

Result:
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤
n : ℕ
⊢ (⋃ n, s n) \ s n ⊆ ⋃ i, s (i + n + 1) \ s (i + n)

Proof state:
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤
n : ℕ
h' : Monotone s
i : ℕ
x : α
hx : x ∈ s i
this : ∃ i, x ∈ s i
⊢ x ∈ s n ∪ ⋃ i, s (i + n + 1) \ s (i + n)

Tactic:
rcases Nat.findX this with ⟨j, hj, hlt⟩

Result:
case mk.intro
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤
n : ℕ
h' : Monotone s
i : ℕ
x : α
hx : x ∈ s i
this : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ m < j, x ∉ s m
⊢ x ∈ s n ∪ ⋃ i, s (i + n + 1) \ s (i + n)

Proof state:
case mk.intro
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤
n : ℕ
h' : Monotone s
i : ℕ
x : α
hx : x ∈ s i
this : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ m < j, x ∉ s m
⊢ x ∈ s n ∪ ⋃ i, s (i + n + 1) \ s (i + n)

Tactic:
clear hx i

Result:
case mk.intro
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤
n : ℕ
h' : Monotone s
x : α
this : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ m < j, x ∉ s m
⊢ x ∈ s n ∪ ⋃ i, s (i + n + 1) \ s (i + n)

Proof state:
case mk.intro.inr.refine_2
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤
n : ℕ
h' : Monotone s
x : α
this✝ : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ m < j, x ∉ s m
hnj : n < j
this : j - (n + 1) + n + 1 = j
⊢ j - (n + 1) + n < j

Tactic:
rw [← Nat.succ_le_iff, Nat.succ_eq_add_one, this]

Result:
no goals

Proof state:
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤
n : ℕ
h' : Monotone s
i : ℕ
x : α
hx : x ∈ s i
⊢ ∃ i, x ∈ s i

Tactic:
exists i

Result:
no goals

Proof state:
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤
⊢ m (⋃ n, s n) = ⨆ n, m (s n)

Tactic:
refine measure_iUnion_of_tendsto_zero m atTop ?_

Result:
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤
⊢ Tendsto (fun k => m ((⋃ n, s n) \ s k)) atTop (𝓝 0)

Proof state:
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤
n : ℕ
⊢ (⋃ n, s n) \ s n ⊆ ⋃ i, s (i + n + 1) \ s (i + n)

Tactic:
have h' : Monotone s := @monotone_nat_of_le_succ (Set α) _ _ h_mono

Result:
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤
n : ℕ
h' : Monotone s
⊢ (⋃ n, s n) \ s n ⊆ ⋃ i, s (i + n + 1) \ s (i + n)

Proof state:
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤
⊢ Tendsto (fun k => m ((⋃ n, s n) \ s k)) atTop (𝓝 0)

Tactic:
refine tendsto_nhds_bot_mono' (ENNReal.tendsto_sum_nat_add _ h0) fun n => ?_

Result:
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤
n : ℕ
⊢ m ((⋃ n, s n) \ s n) ≤ ∑' (k : ℕ), m (s (k + n + 1) \ s (k + n))

Proof state:
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤
n : ℕ
h' : Monotone s
⊢ (⋃ n, s n) \ s n ⊆ ⋃ i, s (i + n + 1) \ s (i + n)

Tactic:
simp only [diff_subset_iff, iUnion_subset_iff]

Result:
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤
n : ℕ
h' : Monotone s
⊢ ∀ (i : ℕ), s i ⊆ s n ∪ ⋃ i, s (i + n + 1) \ s (i + n)

Proof state:
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤
n : ℕ
h' : Monotone s
i : ℕ
x : α
hx : x ∈ s i
⊢ x ∈ s n ∪ ⋃ i, s (i + n + 1) \ s (i + n)

Tactic:
have : ∃i, x ∈ s i := by exists i

Result:
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤
n : ℕ
h' : Monotone s
i : ℕ
x : α
hx : x ∈ s i
this : ∃ i, x ∈ s i
⊢ x ∈ s n ∪ ⋃ i, s (i + n + 1) \ s (i + n)