awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
ε : ℝ
hε : ε > 0
u : Set (α × α) := {a : α × α | dist a.1 a.2 < ε}
hu : u ∈ 𝓤 α
h : ∀ᶠ (m : β × β) in atTop, ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u
⊢ ∀ᶠ (x : β × β) in atTop, ∀ x_1 ∈ s, dist (F x.1 x_1) (F x.2 x_1) < ε

Tactic:
exact h.mono fun n h x hx => h x hx

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
h : ∀ ε > 0, ∃ (N : β), ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
mpr :
  ∀ (ε : ℝ) (hε : ε > 0) (hab : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ u),
    ∀ᶠ (m : β × β) in SProd.sprod (α := Filter β) (β := Filter β) atTop atTop, ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u
⊢ ∀ᶠ (m : β × β) in SProd.sprod (α := Filter β) (β := Filter β) atTop atTop, ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u

Tactic:
rcases Metric.mem_uniformity_dist.mp hu with ⟨ε, hε, hab⟩

Premises used: Metric.mem_uniformity_dist, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
h : ∀ ε > 0, ∃ (N : β), ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ
hε : ε > 0
hab : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ u
mpr :
  ∀ (N : β) (hN : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε),
    ∀ᶠ (m : β × β) in SProd.sprod (α := Filter β) (β := Filter β) atTop atTop, ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u
⊢ ∀ᶠ (m : β × β) in SProd.sprod (α := Filter β) (β := Filter β) atTop atTop, ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u

Tactic:
rcases h ε hε with ⟨N, hN⟩
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
h : ∀ ε > 0, ∃ (N : β), ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ
hε : ε > 0
hab : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ u
N : β
hN : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
mpr : ∃ (a : β × β), ∀ b ≥ a, ∀ x ∈ s, (F b.1 x, F b.2 x) ∈ u
⊢ ∀ᶠ (m : β × β) in SProd.sprod (α := Filter β) (β := Filter β) atTop atTop, ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u

Tactic:
rw [prod_atTop_atTop_eq, eventually_atTop]

Premises used: Filter.prod_atTop_atTop_eq, Filter.eventually_atTop
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
h : ∀ ε > 0, ∃ (N : β), ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ
hε : ε > 0
hab : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ u
N : β
hN : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
h₁ : ∀ b ≥ (N, N), ∀ x ∈ s, (F b.1 x, F b.2 x) ∈ u
⊢ ∃ (a : β × β), ∀ b ≥ a, ∀ x ∈ s, (F b.1 x, F b.2 x) ∈ u

Tactic:
use (N, N)

Premises used: Prod.mk
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
h : ∀ ε > 0, ∃ (N : β), ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ
hε : ε > 0
hab : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ u
N : β
hN : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
b : β × β
hb : b ≥ (N, N)
x : γ
hx : x ∈ s
⊢ (N, N).1 ≤ b.1

Tactic:
rcases hb with ⟨hbl, hbr⟩
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
h : ∀ ε > 0, ∃ (N : β), ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ
hε : ε > 0
hab : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ u
N : β
hN : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
b : β × β
hb : b ≥ (N, N)
x : γ
hx : x ∈ s
hbl : (N, N).1 ≤ b.1
⊢ (N, N).2 ≤ b.2

Tactic:
rcases hb with ⟨hbl, hbr⟩
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
h : ∀ ε > 0, ∃ (N : β), ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ
hε : ε > 0
hab : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ u
N : β
hN : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
b : β × β
x : γ
hx : x ∈ s
hbl : (N, N).1 ≤ b.1
hbr : (N, N).2 ≤ b.2
⊢ (F b.1 x, F b.2 x) ∈ u

Tactic:
hab (hN b.fst hbl.ge b.snd hbr.ge x hx)

Premises used: LE.le.ge, Prod.fst, Prod.snd
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
h : ∀ ε > 0, ∃ (N : β), ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ
hε : ε > 0
hab : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ u
N : β
hN : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
b : β × β
x : γ
hx : x ∈ s
hbl : (N, N).1 ≤ b.1
hbr : (N, N).2 ≤ b.2
⊢ (F b.1 x, F b.2 x) ∈ u

Tactic:
exact hab (hN b.fst hbl.ge b.snd hbr.ge x hx)

Premises used: LE.le.ge, Prod.fst, Prod.snd
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
s : β → α
b : β → ℝ
h : ∀ (n m : β), n ≤ m → dist (s n) (s m) ≤ b n
h₀ : Tendsto b atTop (𝓝 0)
⊢ CauchySeq s

Tactic:
Metric.cauchySeq_iff'.2 fun ε ε0 => (h₀.eventually (gt_mem_nhds ε0)).exists.imp fun N hN n hn =>
    calc dist (s n) (s N) = dist (s N) (s n) := dist_comm _ _
    _ ≤ b N := h _ _ hn
    _ < ε := hN

Premises used: Iff.mpr, gt_mem_nhds, Trans.trans, dist_comm, Exists.imp, Filter.Eventually.exists, Filter.Tendsto.eventually, Metric.cauchySeq_iff'
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
s : β → α
b : β → ℝ
h : ∀ (n m N : β), N ≤ n → N ≤ m → dist (s n) (s m) ≤ b N
h₀ : Tendsto b atTop (𝓝 0)
⊢ CauchySeq s

Tactic:
cauchySeq_of_le_tendsto_0' b (fun _n _m hnm => h _ _ _ le_rfl hnm) h₀

Premises used: le_rfl, cauchySeq_of_le_tendsto_0'
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
inst : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
rcases : ∀ (N : ℕ) (hN : ∀ n ≥ N, dist (u n) (u N) < 1), ∃ R > 0, ∀ (m n : ℕ), dist (u m) (u n) < R
⊢ ∃ R > 0, ∀ (m n : ℕ), dist (u m) (u n) < R

Tactic:
rcases Metric.cauchySeq_iff'.1 hu 1 zero_lt_one with ⟨N, hN⟩

Premises used: zero_lt_one, Iff.mp, OfNat.ofNat, Metric.cauchySeq_iff'
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
inst : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
N : ℕ
hN : ∀ n ≥ N, dist (u n) (u N) < 1
rsuffices : ∀ (R : ℝ) (R0 : R > 0) (H : ∀ (n : ℕ), dist (u n) (u N) < R), ∃ R > 0, ∀ (m n : ℕ), dist (u m) (u n) < R
rsuffices₁ : ∃ R > 0, ∀ (n : ℕ), dist (u n) (u N) < R
⊢ ∃ R > 0, ∀ (m n : ℕ), dist (u m) (u n) < R

Tactic:
rsuffices ⟨R, R0, H⟩ : ∃ R > 0, ∀ n, dist (u n) (u N) < R
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
inst : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
N : ℕ
hN : ∀ n ≥ N, dist (u n) (u N) < 1
R : ℝ
R0 : R > 0
H : ∀ (n : ℕ), dist (u n) (u N) < R
⊢ ∃ R > 0, ∀ (m n : ℕ), dist (u m) (u n) < R

Tactic:
⟨_, add_pos R0 R0, fun m n =>
      lt_of_le_of_lt (dist_triangle_right _ _ _) (add_lt_add (H m) (H n))⟩

Premises used: lt_of_le_of_lt, add_pos, dist_triangle_right, add_lt_add, And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
inst : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
N : ℕ
hN : ∀ n ≥ N, dist (u n) (u N) < 1
R : ℝ
R0 : R > 0
H : ∀ (n : ℕ), dist (u n) (u N) < R
⊢ ∃ R > 0, ∀ (m n : ℕ), dist (u m) (u n) < R

Tactic:
exact ⟨_, add_pos R0 R0, fun m n =>
      lt_of_le_of_lt (dist_triangle_right _ _ _) (add_lt_add (H m) (H n))⟩
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
inst : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
N : ℕ
hN : ∀ n ≥ N, dist (u n) (u N) < 1
R : NNReal := (Finset.range N).sup fun (n : ℕ) ↦ nndist (u n) (u N)
⊢ ∃ R > 0, ∀ (n : ℕ), dist (u n) (u N) < R

Tactic:
⟨↑R + 1, add_pos_of_nonneg_of_pos R.2 zero_lt_one, fun n => ?_⟩

Premises used: zero_lt_one, add_pos_of_nonneg_of_pos, HAdd.hAdd, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
inst : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
N : ℕ
hN : ∀ n ≥ N, dist (u n) (u N) < 1
R : NNReal := (Finset.range N).sup fun (n : ℕ) ↦ nndist (u n) (u N)
refine : ∀ (n : ℕ), dist (u n) (u N) < (↑R : ℝ) + 1
⊢ ∃ R > 0, ∀ (n : ℕ), dist (u n) (u N) < R

Tactic:
refine ⟨↑R + 1, add_pos_of_nonneg_of_pos R.2 zero_lt_one, fun n => ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
inst : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
N : ℕ
hN : ∀ n ≥ N, dist (u n) (u N) < 1
R : NNReal := (Finset.range N).sup fun (n : ℕ) ↦ nndist (u n) (u N)
n : ℕ
inl : ∀ (h : N ≤ n), dist (u n) (u N) < (↑R : ℝ) + 1
inr : ∀ (h : n < N), dist (u n) (u N) < (↑R : ℝ) + 1
⊢ dist (u n) (u N) < (↑R : ℝ) + 1

Tactic:
rcases le_or_gt N n with h | h

Premises used: le_or_gt
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
inst : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
N : ℕ
hN : ∀ n ≥ N, dist (u n) (u N) < 1
R : NNReal := (Finset.range N).sup fun (n : ℕ) ↦ nndist (u n) (u N)
n : ℕ
h : N ≤ n
⊢ dist (u n) (u N) < (↑R : ℝ) + 1

Tactic:
lt_of_lt_of_le (hN _ h) (le_add_of_nonneg_left R.2)

Premises used: lt_of_lt_of_le, le_add_of_nonneg_left, Subtype.property
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
inst : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
N : ℕ
hN : ∀ n ≥ N, dist (u n) (u N) < 1
R : NNReal := (Finset.range N).sup fun (n : ℕ) ↦ nndist (u n) (u N)
n : ℕ
h : N ≤ n
⊢ dist (u n) (u N) < (↑R : ℝ) + 1

Tactic:
exact lt_of_lt_of_le (hN _ h) (le_add_of_nonneg_left R.2)

Premises used: lt_of_lt_of_le, le_add_of_nonneg_left, Subtype.property
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
inst : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
N : ℕ
hN : ∀ n ≥ N, dist (u n) (u N) < 1
R : NNReal := (Finset.range N).sup fun (n : ℕ) ↦ nndist (u n) (u N)
n : ℕ
h : n < N
⊢ nndist (u n) (u N) ≤ R

Tactic:
have : _ ≤ R := Finset.le_sup (Finset.mem_range.2 h)
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
inst : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
N : ℕ
hN : ∀ n ≥ N, dist (u n) (u N) < 1
R : NNReal := (Finset.range N).sup fun (n : ℕ) ↦ nndist (u n) (u N)
n : ℕ
h : n < N
this : nndist (u n) (u N) ≤ R
⊢ dist (u n) (u N) < (↑R : ℝ) + 1

Tactic:
lt_of_le_of_lt this (lt_add_of_pos_right _ zero_lt_one)

Premises used: lt_of_le_of_lt, lt_add_of_pos_right, zero_lt_one
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
inst : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
N : ℕ
hN : ∀ n ≥ N, dist (u n) (u N) < 1
R : NNReal := (Finset.range N).sup fun (n : ℕ) ↦ nndist (u n) (u N)
n : ℕ
h : n < N
this : nndist (u n) (u N) ≤ R
⊢ dist (u n) (u N) < (↑R : ℝ) + 1

Tactic:
exact lt_of_le_of_lt this (lt_add_of_pos_right _ zero_lt_one)

Premises used: lt_of_le_of_lt, lt_add_of_pos_right, zero_lt_one
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
inst : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
S : (N : ℕ) → Set ℝ := fun (N : ℕ) ↦ (fun (p : ℕ × ℕ) ↦ dist (s p.1) (s p.2)) '' {p : ℕ × ℕ | p.1 ≥ N ∧ p.2 ≥ N}
rcases : ∀ (R : ℝ) (hR : ∀ (m n : ℕ), dist (s m) (s n) < R) (N : ℕ), ∃ (x : ℝ), ∀ y ∈ S N, y ≤ x
⊢ ∀ (N : ℕ), ∃ (x : ℝ), ∀ y ∈ S N, y ≤ x

Tactic:
rcases cauchySeq_bdd hs with ⟨R, -, hR⟩

Premises used: cauchySeq_bdd
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
inst : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
S : (N : ℕ) → 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:
fun N => ⟨R, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
inst : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
S : (N : ℕ) → 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
refine : ∀ (N : ℕ), ∀ y ∈ S N, y ≤ R
⊢ ∀ (N : ℕ), ∃ (x : ℝ), ∀ y ∈ S N, y ≤ x

Tactic:
refine fun N => ⟨R, ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
inst : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
S : (N : ℕ) → 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 : Membership.mem (γ := Set (ℕ × ℕ)) {p : ℕ × ℕ | p.1 ≥ N ∧ p.2 ≥ N} (m, n)
⊢ (fun (p : ℕ × ℕ) ↦ dist (s p.1) (s p.2)) (m, n) ≤ R

Tactic:
le_of_lt (hR m n)

Premises used: le_of_lt
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
inst : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
S : (N : ℕ) → 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 : Membership.mem (γ := Set (ℕ × ℕ)) {p : ℕ × ℕ | p.1 ≥ N ∧ p.2 ≥ N} (m, n)
⊢ (fun (p : ℕ × ℕ) ↦ dist (s p.1) (s p.2)) (m, n) ≤ R

Tactic:
exact le_of_lt (hR m n)

Premises used: le_of_lt
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
inst : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
S : (N : ℕ) → Set ℝ := fun (N : ℕ) ↦ (fun (p : ℕ × ℕ) ↦ dist (s p.1) (s p.2)) '' {p : ℕ × ℕ | p.1 ≥ N ∧ p.2 ≥ N}
⊢ ∀ (N : ℕ), ∃ (x : ℝ), ∀ y ∈ S N, y ≤ x

Tactic:
have hS : ∀ N, ∃ x, ∀ y ∈ S N, y ≤ x := by
      rcases cauchySeq_bdd hs with ⟨R, -, hR⟩
      refine fun N => ⟨R, ?_⟩
      rintro _ ⟨⟨m, n⟩, _, rfl⟩
      exact le_of_lt (hR m n)
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
inst : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
S : (N : ℕ) → 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
⊢ ∀ (m n N : ℕ), N ≤ m → N ≤ n → dist (s m) (s n) ≤ sSup (S N)

Tactic:
have ub : ∀ m n N, N ≤ m → N ≤ n → dist (s m) (s n) ≤ sSup (S N) := fun m n N hm hn =>
      le_csSup (hS N) ⟨⟨_, _⟩, ⟨hm, hn⟩, rfl⟩
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
inst : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
S : (N : ℕ) → 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)
⊢ ∀ (n : ℕ), 0 ∈ S n

Tactic:
have S0m : ∀ n, (0 : ℝ) ∈ S n := fun n => ⟨⟨n, n⟩, ⟨le_rfl, le_rfl⟩, dist_self _⟩
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
inst : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
S : (N : ℕ) → 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
⊢ ∀ (n : ℕ), 0 ≤ sSup (S n)

Tactic:
have S0 := fun n => le_csSup (hS n) (S0m n)
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
inst : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
S : (N : ℕ) → 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)

Tactic:
⟨fun N => sSup (S N), S0, ub, Metric.tendsto_atTop.2 fun ε ε0 => ?_⟩

Premises used: Iff.mpr, Metric.tendsto_atTop, And.intro, Exists.intro, SupSet.sSup
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
inst : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
S : (N : ℕ) → 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)
refine : ∀ (ε : ℝ) (ε0 : ε > 0), ∃ (N : ℕ), ∀ n ≥ N, dist (sSup (S n)) 0 < ε
⊢ ∃ (b : ℕ → ℝ), (∀ (n : ℕ), 0 ≤ b n) ∧ (∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (s n) (s m) ≤ b N) ∧ Tendsto b atTop (𝓝 0)

Tactic:
refine ⟨fun N => sSup (S N), S0, ub, Metric.tendsto_atTop.2 fun ε ε0 => ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
inst : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
S : (N : ℕ) → 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 : ℕ), ∀ n ≥ N, dist (sSup (S n)) 0 < ε

Tactic:
(Metric.cauchySeq_iff.1 hs (ε / 2) (half_pos ε0)).imp fun N hN n hn => ?_

Premises used: Metric.cauchySeq_iff, half_pos, HDiv.hDiv, Exists.imp, Iff.mp, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
inst : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
S : (N : ℕ) → 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
refine : ∀ (N : ℕ) (hN : ∀ m ≥ N, ∀ n ≥ N, dist (s m) (s n) < ε / 2) (n : ℕ) (hn : n ≥ N), dist (sSup (S n)) 0 < ε
⊢ ∃ (N : ℕ), ∀ n ≥ N, dist (sSup (S n)) 0 < ε

Tactic:
refine (Metric.cauchySeq_iff.1 hs (ε / 2) (half_pos ε0)).imp fun N hN n hn => ?_

Premises used: Metric.cauchySeq_iff, half_pos, HDiv.hDiv, Exists.imp, Iff.mp, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
inst : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
S : (N : ℕ) → 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
rw : sSup (S n) < ε
⊢ dist (sSup (S n)) 0 < ε

Tactic:
rw [Real.dist_0_eq_abs, abs_of_nonneg (S0 n)]

Premises used: Real.dist_0_eq_abs, abs_of_nonneg
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
inst : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
S : (N : ℕ) → 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:
lt_of_le_of_lt (csSup_le ⟨_, S0m _⟩ ?_) (half_lt_self ε0)

Premises used: half_lt_self, lt_of_le_of_lt, Exists.intro, csSup_le
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
inst : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
S : (N : ℕ) → 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
refine : ∀ b ∈ S n, b ≤ ε / 2
⊢ sSup (S n) < ε

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

Premises used: half_lt_self, lt_of_le_of_lt, Exists.intro, csSup_le
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
inst : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
S : (N : ℕ) → 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:
le_of_lt (hN _ (le_trans hn hm') _ (le_trans hn hn'))

Premises used: le_of_lt, le_trans
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
inst : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
S : (N : ℕ) → 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'))

Premises used: le_of_lt, le_trans
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
inst : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
b : ℕ → ℝ
hb : ∀ (n : ℕ), 0 < b n
rw :
  ∀ (hu : ∀ ε > 0, ∃ (N : ℕ), ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε) (b : ℕ → ℝ) (hb : ∀ (n : ℕ), 0 < b n),
    ∃ (f : ℕ → ℕ), StrictMono f ∧ ∀ (n m : ℕ), m ≥ f n → dist (u m) (u (f n)) < b n
⊢ ∃ (f : ℕ → ℕ), StrictMono f ∧ ∀ (n m : ℕ), m ≥ f n → dist (u m) (u (f n)) < b n

Tactic:
rw [cauchySeq_iff] at hu

Premises used: Metric.cauchySeq_iff
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
inst : PseudoMetricSpace α
u : ℕ → α
hu : ∀ ε > 0, ∃ (N : ℕ), ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε
b : ℕ → ℝ
hb : ∀ (n : ℕ), 0 < b n
k : ℕ
rw : ∃ (a : ℕ), ∀ b_1 ≥ a, ∀ m ≥ b_1, dist (u m) (u b_1) < b k
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ m ≥ n, dist (u m) (u n) < b k

Tactic:
rw [eventually_atTop]

Premises used: Filter.eventually_atTop
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
inst : PseudoMetricSpace α
u : ℕ → α
hu : ∀ ε > 0, ∃ (N : ℕ), ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε
b : ℕ → ℝ
hb : ∀ (n : ℕ), 0 < b n
k : ℕ
obtain :
  ∀ (N : ℕ) (hN : ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < b k), ∃ (a : ℕ), ∀ b_1 ≥ a, ∀ m ≥ b_1, dist (u m) (u b_1) < b k
⊢ ∃ (a : ℕ), ∀ b_1 ≥ a, ∀ m ≥ b_1, dist (u m) (u b_1) < b k

Tactic:
obtain ⟨N, hN⟩ := hu (b k) (hb k)
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
inst : PseudoMetricSpace α
u : ℕ → α
hu : ∀ ε > 0, ∃ (N : ℕ), ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε
b : ℕ → ℝ
hb : ∀ (n : ℕ), 0 < b n
k N : ℕ
hN : ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < b k
⊢ ∃ (a : ℕ), ∀ b_1 ≥ a, ∀ m ≥ b_1, dist (u m) (u b_1) < b k

Tactic:
⟨N, fun m hm r hr => hN r (hm.trans hr) m hm⟩

Premises used: Exists.intro, LE.le.trans
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
inst : PseudoMetricSpace α
u : ℕ → α
hu : ∀ ε > 0, ∃ (N : ℕ), ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε
b : ℕ → ℝ
hb : ∀ (n : ℕ), 0 < b n
k N : ℕ
hN : ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < b k
⊢ ∃ (a : ℕ), ∀ b_1 ≥ a, ∀ m ≥ b_1, dist (u m) (u b_1) < b k

Tactic:
exact ⟨N, fun m hm r hr => hN r (hm.trans hr) m hm⟩
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
inst : PseudoMetricSpace α
u : ℕ → α
hu : ∀ ε > 0, ∃ (N : ℕ), ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε
b : ℕ → ℝ
hb : ∀ (n : ℕ), 0 < b n
⊢ ∀ (k : ℕ), ∀ᶠ (n : ℕ) in atTop, ∀ m ≥ n, dist (u m) (u n) < b k

Tactic:
have hu' : ∀ k, ∀ᶠ (n : ℕ) in atTop, ∀ m ≥ n, dist (u m) (u n) < b k := by
    intro k
    rw [eventually_atTop]
    obtain ⟨N, hN⟩ := hu (b k) (hb k)
    exact ⟨N, fun m hm r hr => hN r (hm.trans hr) m hm⟩