case intro
α : Type u
β : Type v
X : Type ?u.226298
ι : Type ?u.226301
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : ℕ → α
hu : CauchySeq u
N : ℕ
hN : ∀ (n : ℕ), n ≥ N → dist (u n) (u N) < 1
⊢ ∃ R, R > 0 ∧ ∀ (m n : ℕ), dist (u m) (u n) < R
α : Type u
β : Type v
X : Type ?u.226298
ι : Type ?u.226301
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : ℕ → α
hu : CauchySeq u
⊢ ∃ R, R > 0 ∧ ∀ (m n : ℕ), dist (u m) (u n) < R
rcases Metric.cauchySeq_iff'.1 hu 1 zero_lt_one with ⟨N, hN⟩
case intro
α : Type u
β : Type v
X : Type ?u.226298
ι : Type ?u.226301
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : ℕ → α
hu : CauchySeq u
N : ℕ
hN : ∀ (n : ℕ), n ≥ N → dist (u n) (u N) < 1
this : ∃ R, R > 0 ∧ ∀ (n : ℕ), dist (u n) (u N) < R
⊢ ∃ R, R > 0 ∧ ∀ (m n : ℕ), dist (u m) (u n) < R

case this
α : Type u
β : Type v
X : Type ?u.226298
ι : Type ?u.226301
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : ℕ → α
hu : CauchySeq u
N : ℕ
hN : ∀ (n : ℕ), n ≥ N → dist (u n) (u N) < 1
⊢ ∃ R, R > 0 ∧ ∀ (n : ℕ), dist (u n) (u N) < R
case intro
α : Type u
β : Type v
X : Type ?u.226298
ι : Type ?u.226301
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : ℕ → α
hu : CauchySeq u
N : ℕ
hN : ∀ (n : ℕ), n ≥ N → dist (u n) (u N) < 1
⊢ ∃ R, R > 0 ∧ ∀ (m n : ℕ), dist (u m) (u n) < R
suffices : ∃ R > 0, ∀ n, dist (u n) (u N) < R
case this
α : Type u
β : Type v
X : Type ?u.226298
ι : Type ?u.226301
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : ℕ → α
hu : CauchySeq u
N : ℕ
hN : ∀ (n : ℕ), n ≥ N → dist (u n) (u N) < 1
R : ℝ≥0 := Finset.sup (Finset.range N) fun n => nndist (u n) (u N)
⊢ ∃ R, R > 0 ∧ ∀ (n : ℕ), dist (u n) (u N) < R
case this
α : Type u
β : Type v
X : Type ?u.226298
ι : Type ?u.226301
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : ℕ → α
hu : CauchySeq u
N : ℕ
hN : ∀ (n : ℕ), n ≥ N → dist (u n) (u N) < 1
⊢ ∃ R, R > 0 ∧ ∀ (n : ℕ), dist (u n) (u N) < R
let R := Finset.sup (Finset.range N) fun n => nndist (u n) (u N)
case this
α : Type u
β : Type v
X : Type ?u.226298
ι : Type ?u.226301
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : ℕ → α
hu : CauchySeq u
N : ℕ
hN : ∀ (n : ℕ), n ≥ N → dist (u n) (u N) < 1
R : ℝ≥0 := Finset.sup (Finset.range N) fun n => nndist (u n) (u N)
n : ℕ
⊢ dist (u n) (u N) < ↑R + 1
case this
α : Type u
β : Type v
X : Type ?u.226298
ι : Type ?u.226301
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : ℕ → α
hu : CauchySeq u
N : ℕ
hN : ∀ (n : ℕ), n ≥ N → dist (u n) (u N) < 1
R : ℝ≥0 := Finset.sup (Finset.range N) fun n => nndist (u n) (u N)
⊢ ∃ R, R > 0 ∧ ∀ (n : ℕ), dist (u n) (u N) < R
refine' ⟨↑R + 1, add_pos_of_nonneg_of_pos R.2 zero_lt_one, fun n => _⟩
case this.inl
α : Type u
β : Type v
X : Type ?u.226298
ι : Type ?u.226301
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : ℕ → α
hu : CauchySeq u
N : ℕ
hN : ∀ (n : ℕ), n ≥ N → dist (u n) (u N) < 1
R : ℝ≥0 := Finset.sup (Finset.range N) fun n => nndist (u n) (u N)
n : ℕ
h : N ≤ n
⊢ dist (u n) (u N) < ↑R + 1

case this.inr
α : Type u
β : Type v
X : Type ?u.226298
ι : Type ?u.226301
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : ℕ → α
hu : CauchySeq u
N : ℕ
hN : ∀ (n : ℕ), n ≥ N → dist (u n) (u N) < 1
R : ℝ≥0 := Finset.sup (Finset.range N) fun n => nndist (u n) (u N)
n : ℕ
h : n < N
⊢ dist (u n) (u N) < ↑R + 1
case this
α : Type u
β : Type v
X : Type ?u.226298
ι : Type ?u.226301
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : ℕ → α
hu : CauchySeq u
N : ℕ
hN : ∀ (n : ℕ), n ≥ N → dist (u n) (u N) < 1
R : ℝ≥0 := Finset.sup (Finset.range N) fun n => nndist (u n) (u N)
n : ℕ
⊢ dist (u n) (u N) < ↑R + 1
cases' le_or_lt N n with h h
case intro.intro.intro
α : Type u
β : Type v
X : Type ?u.226298
ι : Type ?u.226301
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : ℕ → α
hu : CauchySeq u
N : ℕ
hN : ∀ (n : ℕ), n ≥ N → dist (u n) (u N) < 1
R : ℝ
R0 : R > 0
H : ∀ (n : ℕ), dist (u n) (u N) < R
⊢ ∃ R, R > 0 ∧ ∀ (m n : ℕ), dist (u m) (u n) < R
case intro
α : Type u
β : Type v
X : Type ?u.226298
ι : Type ?u.226301
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : ℕ → α
hu : CauchySeq u
N : ℕ
hN : ∀ (n : ℕ), n ≥ N → dist (u n) (u N) < 1
this : ∃ R, R > 0 ∧ ∀ (n : ℕ), dist (u n) (u N) < R
⊢ ∃ R, R > 0 ∧ ∀ (m n : ℕ), dist (u m) (u n) < R
rcases this with ⟨R, R0, H⟩
no goals
case intro.intro.intro
α : Type u
β : Type v
X : Type ?u.226298
ι : Type ?u.226301
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : ℕ → α
hu : CauchySeq u
N : ℕ
hN : ∀ (n : ℕ), n ≥ N → dist (u n) (u N) < 1
R : ℝ
R0 : R > 0
H : ∀ (n : ℕ), dist (u n) (u N) < R
⊢ ∃ R, R > 0 ∧ ∀ (m n : ℕ), dist (u m) (u n) < R
exact ⟨_, add_pos R0 R0, fun m n =>
  lt_of_le_of_lt (dist_triangle_right _ _ _) (add_lt_add (H m) (H n))⟩
no goals
case this.inl
α : Type u
β : Type v
X : Type ?u.226298
ι : Type ?u.226301
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : ℕ → α
hu : CauchySeq u
N : ℕ
hN : ∀ (n : ℕ), n ≥ N → dist (u n) (u N) < 1
R : ℝ≥0 := Finset.sup (Finset.range N) fun n => nndist (u n) (u N)
n : ℕ
h : N ≤ n
⊢ dist (u n) (u N) < ↑R + 1
exact lt_of_lt_of_le (hN _ h) (le_add_of_nonneg_left R.2)
case this.inr
α : Type u
β : Type v
X : Type ?u.226298
ι : Type ?u.226301
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : ℕ → α
hu : CauchySeq u
N : ℕ
hN : ∀ (n : ℕ), n ≥ N → dist (u n) (u N) < 1
R : ℝ≥0 := Finset.sup (Finset.range N) 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
case this.inr
α : Type u
β : Type v
X : Type ?u.226298
ι : Type ?u.226301
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : ℕ → α
hu : CauchySeq u
N : ℕ
hN : ∀ (n : ℕ), n ≥ N → dist (u n) (u N) < 1
R : ℝ≥0 := Finset.sup (Finset.range N) fun n => nndist (u n) (u N)
n : ℕ
h : n < N
⊢ dist (u n) (u N) < ↑R + 1
have : _ ≤ R := Finset.le_sup (Finset.mem_range.2 h)
no goals
case this.inr
α : Type u
β : Type v
X : Type ?u.226298
ι : Type ?u.226301
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : ℕ → α
hu : CauchySeq u
N : ℕ
hN : ∀ (n : ℕ), n ≥ N → dist (u n) (u N) < 1
R : ℝ≥0 := Finset.sup (Finset.range N) 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
exact lt_of_le_of_lt this (lt_add_of_pos_right _ zero_lt_one)