-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem exists_measure_iInter_lt {α ι : Type*} {_ : MeasurableSpace α} {μ : Measure α}
    [SemilatticeSup ι] [Countable ι] {f : ι → Set α}
    (hm : ∀ i, NullMeasurableSet (f i) μ) {ε : ℝ≥0∞} (hε : 0 < ε) (hfin : ∃ i, μ (f i) ≠ ∞)
    (hfem : ⋂ n, f n = ∅) : ∃ m, μ (⋂ n ≤ m, f n) < ε

Proof state:
α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
ε : ℝ≥0∞
hε : 0 < ε
hfin : ∃ i, μ (f i) ≠ ⊤
hfem : ⋂ n, f n = ∅
⊢ ∃ m, μ (⋂ n, ⋂ (_ : n ≤ m), f n) < ε

Tactic:
let F m := μ (⋂ n ≤ m, f n)

Result:
α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
ε : ℝ≥0∞
hε : 0 < ε
hfin : ∃ i, μ (f i) ≠ ⊤
hfem : ⋂ n, f n = ∅
F : ι → ℝ≥0∞ := fun m => μ (⋂ n, ⋂ (_ : n ≤ m), f n)
⊢ ∃ m, μ (⋂ n, ⋂ (_ : n ≤ m), f n) < ε

Proof state:
α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
ε : ℝ≥0∞
hε : 0 < ε
hfin : ∃ i, μ (f i) ≠ ⊤
hfem : ⋂ n, f n = ∅
F : ι → ℝ≥0∞ := fun m => μ (⋂ n, ⋂ (_ : n ≤ m), f n)
hFAnti : Antitone F
⊢ μ (⋂ n, f n) = 0

Tactic:
simp only [hfem, measure_empty]

Result:
no goals

Proof state:
α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
ε : ℝ≥0∞
hε : 0 < ε
hfin : ∃ i, μ (f i) ≠ ⊤
hfem : ⋂ n, f n = ∅
F : ι → ℝ≥0∞ := fun m => μ (⋂ n, ⋂ (_ : n ≤ m), f n)
hFAnti : Antitone F
hzero : μ (⋂ n, f n) = 0
⊢ Tendsto F atTop (𝓝 0)

Tactic:
rw [← hzero]

Result:
α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
ε : ℝ≥0∞
hε : 0 < ε
hfin : ∃ i, μ (f i) ≠ ⊤
hfem : ⋂ n, f n = ∅
F : ι → ℝ≥0∞ := fun m => μ (⋂ n, ⋂ (_ : n ≤ m), f n)
hFAnti : Antitone F
hzero : μ (⋂ n, f n) = 0
⊢ Tendsto F atTop (𝓝 (μ (⋂ n, f n)))

Proof state:
α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
ε : ℝ≥0∞
hε : 0 < ε
hfin : ∃ i, μ (f i) ≠ ⊤
hfem : ⋂ n, f n = ∅
F : ι → ℝ≥0∞ := fun m => μ (⋂ n, ⋂ (_ : n ≤ m), f n)
hFAnti : Antitone F
hzero : μ (⋂ n, f n) = 0
⊢ Tendsto F atTop (𝓝 (μ (⋂ n, f n)))

Tactic:
exact tendsto_measure_iInter_le hm hfin

Result:
no goals

Proof state:
α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
ε : ℝ≥0∞
hε : 0 < ε
hfin : ∃ i, μ (f i) ≠ ⊤
hfem : ⋂ n, f n = ∅
F : ι → ℝ≥0∞ := fun m => μ (⋂ n, ⋂ (_ : n ≤ m), f n)
hFAnti : Antitone F
this : Tendsto F atTop (𝓝 0)
⊢ ∃ m, μ (⋂ n, ⋂ (_ : n ≤ m), f n) < ε

Tactic:
rw [@ENNReal.tendsto_atTop_zero_iff_lt_of_antitone
     _ (nonempty_of_exists hfin) _ _ hFAnti] at this

Result:
α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
ε : ℝ≥0∞
hε : 0 < ε
hfin : ∃ i, μ (f i) ≠ ⊤
hfem : ⋂ n, f n = ∅
F : ι → ℝ≥0∞ := fun m => μ (⋂ n, ⋂ (_ : n ≤ m), f n)
hFAnti : Antitone F
this : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, F n < ε
⊢ ∃ m, μ (⋂ n, ⋂ (_ : n ≤ m), f n) < ε

Proof state:
α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
ε : ℝ≥0∞
hε : 0 < ε
hfin : ∃ i, μ (f i) ≠ ⊤
hfem : ⋂ n, f n = ∅
F : ι → ℝ≥0∞ := fun m => μ (⋂ n, ⋂ (_ : n ≤ m), f n)
hFAnti : Antitone F
⊢ Tendsto F atTop (𝓝 0)

Tactic:
have hzero : μ (⋂ n, f n) = 0 := by
  simp only [hfem, measure_empty]

Result:
α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
ε : ℝ≥0∞
hε : 0 < ε
hfin : ∃ i, μ (f i) ≠ ⊤
hfem : ⋂ n, f n = ∅
F : ι → ℝ≥0∞ := fun m => μ (⋂ n, ⋂ (_ : n ≤ m), f n)
hFAnti : Antitone F
hzero : μ (⋂ n, f n) = 0
⊢ Tendsto F atTop (𝓝 0)

Proof state:
α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
ε : ℝ≥0∞
hε : 0 < ε
hfin : ∃ i, μ (f i) ≠ ⊤
hfem : ⋂ n, f n = ∅
F : ι → ℝ≥0∞ := fun m => μ (⋂ n, ⋂ (_ : n ≤ m), f n)
⊢ ∃ m, μ (⋂ n, ⋂ (_ : n ≤ m), f n) < ε

Tactic:
have hFAnti : Antitone F :=
    fun i j hij => measure_mono (biInter_subset_biInter_left fun k hki => le_trans hki hij)

Result:
α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
ε : ℝ≥0∞
hε : 0 < ε
hfin : ∃ i, μ (f i) ≠ ⊤
hfem : ⋂ n, f n = ∅
F : ι → ℝ≥0∞ := fun m => μ (⋂ n, ⋂ (_ : n ≤ m), f n)
hFAnti : Antitone F
⊢ ∃ m, μ (⋂ n, ⋂ (_ : n ≤ m), f n) < ε

Proof state:
α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
ε : ℝ≥0∞
hε : 0 < ε
hfin : ∃ i, μ (f i) ≠ ⊤
hfem : ⋂ n, f n = ∅
F : ι → ℝ≥0∞ := fun m => μ (⋂ n, ⋂ (_ : n ≤ m), f n)
hFAnti : Antitone F
this : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, F n < ε
⊢ ∃ m, μ (⋂ n, ⋂ (_ : n ≤ m), f n) < ε

Tactic:
exact this ε hε

Result:
no goals

Proof state:
α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
ε : ℝ≥0∞
hε : 0 < ε
hfin : ∃ i, μ (f i) ≠ ⊤
hfem : ⋂ n, f n = ∅
F : ι → ℝ≥0∞ := fun m => μ (⋂ n, ⋂ (_ : n ≤ m), f n)
hFAnti : Antitone F
⊢ ∃ m, μ (⋂ n, ⋂ (_ : n ≤ m), f n) < ε

Tactic:
suffices Filter.Tendsto F Filter.atTop (𝓝 0) by
  rw [@ENNReal.tendsto_atTop_zero_iff_lt_of_antitone
       _ (nonempty_of_exists hfin) _ _ hFAnti] at this
  exact this ε hε

Result:
α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
ε : ℝ≥0∞
hε : 0 < ε
hfin : ∃ i, μ (f i) ≠ ⊤
hfem : ⋂ n, f n = ∅
F : ι → ℝ≥0∞ := fun m => μ (⋂ n, ⋂ (_ : n ≤ m), f n)
hFAnti : Antitone F
⊢ Tendsto F atTop (𝓝 0)