-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem EMetric.cauchySeq_iff_le_tendsto_0 [Nonempty β] [SemilatticeSup β] {s : β → α} :
    CauchySeq s ↔ ∃ b : β → ℝ≥0∞, (∀ n m N : β, N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N) ∧
      Tendsto b atTop (𝓝 0) := EMetric.cauchySeq_iff.trans <| by
  constructor
  · intro hs
    /- `s` is Cauchy sequence. Let `b n` be the diameter of the set `s '' Set.Ici n`. -/
    refine ⟨fun N => EMetric.diam (s '' Ici N), fun n m N hn hm => ?_, ?_⟩
    -- Prove that it bounds the distances of points in the Cauchy sequence
    · exact EMetric.edist_le_diam_of_mem (mem_image_of_mem _ hn) (mem_image_of_mem _ hm)
    -- Prove that it tends to `0`, by using the Cauchy property of `s`
    · refine ENNReal.tendsto_nhds_zero.2 fun ε ε0 => ?_
      rcases hs ε ε0 with ⟨N, hN⟩
      refine (eventually_ge_atTop N).mono fun n hn => EMetric.diam_le ?_
      rintro _ ⟨k, hk, rfl⟩ _ ⟨l, hl, rfl⟩
      exact (hN _ (hn.trans hk) _ (hn.trans hl)).le
  · rintro ⟨b, ⟨b_bound, b_lim⟩⟩ ε εpos
    have : ∀ᶠ n in atTop, b n < ε := b_lim.eventually (gt_mem_nhds εpos)
    rcases this.exists with ⟨N, hN⟩
    refine ⟨N, fun m hm n hn => ?_⟩
    calc edist (s m) (s n) ≤ b N := b_bound m n N hm hn
    _ < ε := hN

Proof state:
case mpr.intro.intro
α : Type u_1
β : Type u_2
inst✝² : PseudoEMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
s : β → α
b : β → ℝ≥0∞
b_bound : ∀ (n m N : β), N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
ε : ℝ≥0∞
εpos : ε > 0
this : ∀ᶠ (n : β) in atTop, b n < ε
⊢ ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε

Tactic:
rcases this.exists with ⟨N, hN⟩

Result:
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : PseudoEMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
s : β → α
b : β → ℝ≥0∞
b_bound : ∀ (n m N : β), N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
ε : ℝ≥0∞
εpos : ε > 0
this : ∀ᶠ (n : β) in atTop, b n < ε
N : β
hN : b N < ε
⊢ ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε

Proof state:
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : PseudoEMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
s : β → α
b : β → ℝ≥0∞
b_bound : ∀ (n m N : β), N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
ε : ℝ≥0∞
εpos : ε > 0
this : ∀ᶠ (n : β) in atTop, b n < ε
N : β
hN : b N < ε
m : β
hm : N ≤ m
n : β
hn : N ≤ n
⊢ edist (s m) (s n) < ε

Tactic:
calc edist (s m) (s n) ≤ b N := b_bound m n N hm hn
_ < ε := hN

Result:
no goals

Proof state:
case mp.refine_1
α : Type u_1
β : Type u_2
inst✝² : PseudoEMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
s : β → α
hs : ∀ ε > 0, ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
n m N : β
hn : N ≤ n
hm : N ≤ m
⊢ edist (s n) (s m) ≤ (fun N => diam (s '' Ici N)) N

Tactic:
exact EMetric.edist_le_diam_of_mem (mem_image_of_mem _ hn) (mem_image_of_mem _ hm)

Result:
no goals

Proof state:
case mp.refine_2.intro
α : Type u_1
β : Type u_2
inst✝² : PseudoEMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
s : β → α
hs : ∀ ε > 0, ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
ε : ℝ≥0∞
ε0 : ε > 0
N : β
hN : ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
⊢ ∀ᶠ (x : β) in atTop, diam (s '' Ici x) ≤ ε

Tactic:
refine (eventually_ge_atTop N).mono fun n hn => EMetric.diam_le ?_

Result:
case mp.refine_2.intro
α : Type u_1
β : Type u_2
inst✝² : PseudoEMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
s : β → α
hs : ∀ ε > 0, ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
ε : ℝ≥0∞
ε0 : ε > 0
N : β
hN : ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
n : β
hn : N ≤ n
⊢ ∀ x ∈ s '' Ici n, ∀ y ∈ s '' Ici n, edist x y ≤ ε

Proof state:
case mp.refine_2.intro
α : Type u_1
β : Type u_2
inst✝² : PseudoEMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
s : β → α
hs : ∀ ε > 0, ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
ε : ℝ≥0∞
ε0 : ε > 0
N : β
hN : ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
n : β
hn : N ≤ n
⊢ ∀ x ∈ s '' Ici n, ∀ y ∈ s '' Ici n, edist x y ≤ ε

Tactic:
rintro _ ⟨k, hk, rfl⟩ _ ⟨l, hl, rfl⟩

Result:
case mp.refine_2.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : PseudoEMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
s : β → α
hs : ∀ ε > 0, ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
ε : ℝ≥0∞
ε0 : ε > 0
N : β
hN : ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
n : β
hn : N ≤ n
k : β
hk : k ∈ Ici n
l : β
hl : l ∈ Ici n
⊢ edist (s k) (s l) ≤ ε