-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
lemma tendsto_measure_biUnion_Ici_zero_of_pairwise_disjoint
    {X : Type*} [MeasurableSpace X] {μ : Measure X} [IsFiniteMeasure μ]
    {Es : ℕ → Set X} (Es_mble : ∀ i, NullMeasurableSet (Es i) μ)
    (Es_disj : Pairwise fun n m ↦ Disjoint (Es n) (Es m)) :
    Tendsto (μ ∘ fun n ↦ ⋃ i ≥ n, Es i) atTop (𝓝 0)

Proof state:
X : Type u_5
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun n m => Disjoint (Es n) (Es m)
decr : Antitone fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i
nothing : ⋂ n, ⋃ i, ⋃ (_ : i ≥ n), Es i = ∅
n : ℕ
⊢ NullMeasurableSet (⋃ i, ⋃ (_ : i ≥ n), Es i) μ

Tactic:
measurability

Result:
no goals

Proof state:
case intro.intro.intro.intro
X : Type u_5
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun n m => Disjoint (Es n) (Es m)
decr : Antitone fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i
x : X
hx : ∀ (i : ℕ), ∃ i_1 ≥ i, x ∈ Es i_1
j : ℕ
left✝ : j ≥ 0
x_in_Es_j : x ∈ Es j
k : ℕ
k_gt_j : k ≥ j + 1
x_in_Es_k : x ∈ Es k
⊢ x ∈ ∅

Tactic:
have oops := (Es_disj (Nat.ne_of_lt k_gt_j)).ne_of_mem x_in_Es_j x_in_Es_k

Result:
case intro.intro.intro.intro
X : Type u_5
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun n m => Disjoint (Es n) (Es m)
decr : Antitone fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i
x : X
hx : ∀ (i : ℕ), ∃ i_1 ≥ i, x ∈ Es i_1
j : ℕ
left✝ : j ≥ 0
x_in_Es_j : x ∈ Es j
k : ℕ
k_gt_j : k ≥ j + 1
x_in_Es_k : x ∈ Es k
oops : x ≠ x
⊢ x ∈ ∅

Proof state:
X : Type u_5
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun n m => Disjoint (Es n) (Es m)
decr : Antitone fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i
x : X
hx : ∀ (i : ℕ), ∃ i_1 ≥ i, x ∈ Es i_1
⊢ x ∈ ∅

Tactic:
obtain ⟨j, _, x_in_Es_j⟩ := hx 0

Result:
case intro.intro
X : Type u_5
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun n m => Disjoint (Es n) (Es m)
decr : Antitone fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i
x : X
hx : ∀ (i : ℕ), ∃ i_1 ≥ i, x ∈ Es i_1
j : ℕ
left✝ : j ≥ 0
x_in_Es_j : x ∈ Es j
⊢ x ∈ ∅

Proof state:
X : Type u_5
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun n m => Disjoint (Es n) (Es m)
decr : Antitone fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i
⊢ Tendsto (⇑μ ∘ fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i) atTop (𝓝 0)

Tactic:
have nothing : ⋂ n, ⋃ i ≥ n, Es i = ∅ := by
  apply subset_antisymm _ (empty_subset _)
  intro x hx
  simp only [mem_iInter, mem_iUnion, exists_prop] at hx
  obtain ⟨j, _, x_in_Es_j⟩ := hx 0
  obtain ⟨k, k_gt_j, x_in_Es_k⟩ := hx (j+1)
  have oops := (Es_disj (Nat.ne_of_lt k_gt_j)).ne_of_mem x_in_Es_j x_in_Es_k
  contradiction

Result:
X : Type u_5
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun n m => Disjoint (Es n) (Es m)
decr : Antitone fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i
nothing : ⋂ n, ⋃ i, ⋃ (_ : i ≥ n), Es i = ∅
⊢ Tendsto (⇑μ ∘ fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i) atTop (𝓝 0)

Proof state:
case intro.intro
X : Type u_5
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun n m => Disjoint (Es n) (Es m)
decr : Antitone fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i
x : X
hx : ∀ (i : ℕ), ∃ i_1 ≥ i, x ∈ Es i_1
j : ℕ
left✝ : j ≥ 0
x_in_Es_j : x ∈ Es j
⊢ x ∈ ∅

Tactic:
obtain ⟨k, k_gt_j, x_in_Es_k⟩ := hx (j+1)

Result:
case intro.intro.intro.intro
X : Type u_5
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun n m => Disjoint (Es n) (Es m)
decr : Antitone fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i
x : X
hx : ∀ (i : ℕ), ∃ i_1 ≥ i, x ∈ Es i_1
j : ℕ
left✝ : j ≥ 0
x_in_Es_j : x ∈ Es j
k : ℕ
k_gt_j : k ≥ j + 1
x_in_Es_k : x ∈ Es k
⊢ x ∈ ∅

Proof state:
X : Type u_5
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun n m => Disjoint (Es n) (Es m)
decr : Antitone fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i
nothing : ⋂ n, ⋃ i, ⋃ (_ : i ≥ n), Es i = ∅
key : Tendsto (⇑μ ∘ fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i) atTop (𝓝 0)
⊢ Tendsto (⇑μ ∘ fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i) atTop (𝓝 0)

Tactic:
convert key

Result:
no goals

Proof state:
X : Type u_5
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun n m => Disjoint (Es n) (Es m)
decr : Antitone fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i
nothing : ⋂ n, ⋃ i, ⋃ (_ : i ≥ n), Es i = ∅
key : Tendsto (⇑μ ∘ fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i) atTop (𝓝 (μ (⋂ n, ⋃ i, ⋃ (_ : i ≥ n), Es i)))
⊢ Tendsto (⇑μ ∘ fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i) atTop (𝓝 0)

Tactic:
simp only [nothing, measure_empty] at key

Result:
X : Type u_5
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun n m => Disjoint (Es n) (Es m)
decr : Antitone fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i
nothing : ⋂ n, ⋃ i, ⋃ (_ : i ≥ n), Es i = ∅
key : Tendsto (⇑μ ∘ fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i) atTop (𝓝 0)
⊢ Tendsto (⇑μ ∘ fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i) atTop (𝓝 0)

Proof state:
X : Type u_5
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun n m => Disjoint (Es n) (Es m)
decr : Antitone fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i
⊢ ⋂ n, ⋃ i, ⋃ (_ : i ≥ n), Es i ⊆ ∅

Tactic:
intro x hx

Result:
X : Type u_5
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun n m => Disjoint (Es n) (Es m)
decr : Antitone fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i
x : X
hx : x ∈ ⋂ n, ⋃ i, ⋃ (_ : i ≥ n), Es i
⊢ x ∈ ∅

Proof state:
case intro.intro.intro.intro
X : Type u_5
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun n m => Disjoint (Es n) (Es m)
decr : Antitone fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i
x : X
hx : ∀ (i : ℕ), ∃ i_1 ≥ i, x ∈ Es i_1
j : ℕ
left✝ : j ≥ 0
x_in_Es_j : x ∈ Es j
k : ℕ
k_gt_j : k ≥ j + 1
x_in_Es_k : x ∈ Es k
oops : x ≠ x
⊢ x ∈ ∅

Tactic:
contradiction

Result:
no goals

Proof state:
X : Type u_5
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun n m => Disjoint (Es n) (Es m)
⊢ Tendsto (⇑μ ∘ fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i) atTop (𝓝 0)

Tactic:
have decr : Antitone fun n ↦ ⋃ i ≥ n, Es i :=
  fun n m hnm ↦ biUnion_mono (fun _ hi ↦ le_trans hnm hi) (fun _ _ ↦ subset_rfl)

Result:
X : Type u_5
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun n m => Disjoint (Es n) (Es m)
decr : Antitone fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i
⊢ Tendsto (⇑μ ∘ fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i) atTop (𝓝 0)