-- Mathlib/Topology/MetricSpace/Cauchy.lean
theorem cauchySeq_iff_le_tendsto_0 {s : ℕ → α} :
    CauchySeq s ↔
      ∃ b : ℕ → ℝ,
        (∀ n, 0 ≤ b n) ∧
          (∀ n m N : ℕ, N ≤ n → N ≤ m → dist (s n) (s m) ≤ b N) ∧ Tendsto b atTop (𝓝 0) :=
  ⟨fun hs => by
    /- `s` is a Cauchy sequence. The sequence `b` will be constructed by taking
      the supremum of the distances between `s n` and `s m` for `n m ≥ N`.
      First, we prove that all these distances are bounded, as otherwise the Sup
      would not make sense. -/
    let S N := (fun p : ℕ × ℕ => dist (s p.1) (s p.2)) '' { p | p.1 ≥ N ∧ p.2 ≥ N }
    have hS : ∀ N, ∃ x, ∀ y ∈ S N, y ≤ x

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
S : ℕ → Set ℝ := fun N => (fun p => dist (s p.1) (s p.2)) '' {p | p.1 ≥ N ∧ p.2 ≥ N}
hS : ∀ (N : ℕ), ∃ x, ∀ y ∈ S N, y ≤ x
ub : ∀ (m n N : ℕ), N ≤ m → N ≤ n → dist (s m) (s n) ≤ sSup (S N)
S0m : ∀ (n : ℕ), 0 ∈ S n
S0 : ∀ (n : ℕ), 0 ≤ sSup (S n)
ε : ℝ
ε0 : ε > 0
N : ℕ
hN : ∀ m ≥ N, ∀ n ≥ N, dist (s m) (s n) < ε / 2
n : ℕ
hn : n ≥ N
⊢ sSup (S n) < ε

Tactic:
refine lt_of_le_of_lt (csSup_le ⟨_, S0m _⟩ ?_) (half_lt_self ε0)

Result:
α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
S : ℕ → Set ℝ := fun N => (fun p => dist (s p.1) (s p.2)) '' {p | p.1 ≥ N ∧ p.2 ≥ N}
hS : ∀ (N : ℕ), ∃ x, ∀ y ∈ S N, y ≤ x
ub : ∀ (m n N : ℕ), N ≤ m → N ≤ n → dist (s m) (s n) ≤ sSup (S N)
S0m : ∀ (n : ℕ), 0 ∈ S n
S0 : ∀ (n : ℕ), 0 ≤ sSup (S n)
ε : ℝ
ε0 : ε > 0
N : ℕ
hN : ∀ m ≥ N, ∀ n ≥ N, dist (s m) (s n) < ε / 2
n : ℕ
hn : n ≥ N
⊢ ∀ b ∈ S n, b ≤ ε / 2

Proof state:
case intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
S : ℕ → Set ℝ := fun N => (fun p => dist (s p.1) (s p.2)) '' {p | p.1 ≥ N ∧ p.2 ≥ N}
R : ℝ
hR : ∀ (m n : ℕ), dist (s m) (s n) < R
⊢ ∀ (N : ℕ), ∃ x, ∀ y ∈ S N, y ≤ x

Tactic:
refine fun N => ⟨R, ?_⟩

Result:
case intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
S : ℕ → Set ℝ := fun N => (fun p => dist (s p.1) (s p.2)) '' {p | p.1 ≥ N ∧ p.2 ≥ N}
R : ℝ
hR : ∀ (m n : ℕ), dist (s m) (s n) < R
N : ℕ
⊢ ∀ y ∈ S N, y ≤ R

Proof state:
case intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
S : ℕ → Set ℝ := fun N => (fun p => dist (s p.1) (s p.2)) '' {p | p.1 ≥ N ∧ p.2 ≥ N}
R : ℝ
hR : ∀ (m n : ℕ), dist (s m) (s n) < R
N : ℕ
⊢ ∀ y ∈ S N, y ≤ R

Tactic:
rintro _ ⟨⟨m, n⟩, _, rfl⟩

Result:
case intro.intro.intro.mk.intro
α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
S : ℕ → Set ℝ := fun N => (fun p => dist (s p.1) (s p.2)) '' {p | p.1 ≥ N ∧ p.2 ≥ N}
R : ℝ
hR : ∀ (m n : ℕ), dist (s m) (s n) < R
N m n : ℕ
left✝ : (m, n) ∈ {p | p.1 ≥ N ∧ p.2 ≥ N}
⊢ (fun p => dist (s p.1) (s p.2)) (m, n) ≤ R

Proof state:
case intro.mk.intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
S : ℕ → Set ℝ := fun N => (fun p => dist (s p.1) (s p.2)) '' {p | p.1 ≥ N ∧ p.2 ≥ N}
hS : ∀ (N : ℕ), ∃ x, ∀ y ∈ S N, y ≤ x
ub : ∀ (m n N : ℕ), N ≤ m → N ≤ n → dist (s m) (s n) ≤ sSup (S N)
S0m : ∀ (n : ℕ), 0 ∈ S n
S0 : ∀ (n : ℕ), 0 ≤ sSup (S n)
ε : ℝ
ε0 : ε > 0
N : ℕ
hN : ∀ m ≥ N, ∀ n ≥ N, dist (s m) (s n) < ε / 2
n : ℕ
hn : n ≥ N
m' n' : ℕ
hm' : (m', n').1 ≥ n
hn' : (m', n').2 ≥ n
⊢ (fun p => dist (s p.1) (s p.2)) (m', n') ≤ ε / 2

Tactic:
exact le_of_lt (hN _ (le_trans hn hm') _ (le_trans hn hn'))

Result:
no goals

Proof state:
case intro.intro.intro.mk.intro
α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
S : ℕ → Set ℝ := fun N => (fun p => dist (s p.1) (s p.2)) '' {p | p.1 ≥ N ∧ p.2 ≥ N}
R : ℝ
hR : ∀ (m n : ℕ), dist (s m) (s n) < R
N m n : ℕ
left✝ : (m, n) ∈ {p | p.1 ≥ N ∧ p.2 ≥ N}
⊢ (fun p => dist (s p.1) (s p.2)) (m, n) ≤ R

Tactic:
exact le_of_lt (hR m n)

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
S : ℕ → Set ℝ := fun N => (fun p => dist (s p.1) (s p.2)) '' {p | p.1 ≥ N ∧ p.2 ≥ N}
hS : ∀ (N : ℕ), ∃ x, ∀ y ∈ S N, y ≤ x
ub : ∀ (m n N : ℕ), N ≤ m → N ≤ n → dist (s m) (s n) ≤ sSup (S N)
S0m : ∀ (n : ℕ), 0 ∈ S n
⊢ ∃ b, (∀ (n : ℕ), 0 ≤ b n) ∧ (∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (s n) (s m) ≤ b N) ∧ Tendsto b atTop (𝓝 0)

Tactic:
have S0 := fun n => le_csSup (hS n) (S0m n)

Result:
α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
S : ℕ → Set ℝ := fun N => (fun p => dist (s p.1) (s p.2)) '' {p | p.1 ≥ N ∧ p.2 ≥ N}
hS : ∀ (N : ℕ), ∃ x, ∀ y ∈ S N, y ≤ x
ub : ∀ (m n N : ℕ), N ≤ m → N ≤ n → dist (s m) (s n) ≤ sSup (S N)
S0m : ∀ (n : ℕ), 0 ∈ S n
S0 : ∀ (n : ℕ), 0 ≤ sSup (S n)
⊢ ∃ b, (∀ (n : ℕ), 0 ≤ b n) ∧ (∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (s n) (s m) ≤ b N) ∧ Tendsto b atTop (𝓝 0)