Theorem: cauchySeq_of_le_geometric_two' (LeanInRome/S5_Topology/S02_Metric_Spaces.lean)

State before:
X : Type u_1
inst✝ : MetricSpace X
a b c : X
r : ℝ
u : ℕ → X
hu : ∀ (n : ℕ), dist (u n) (u (n + 1)) ≤ (1 / 2) ^ n
⊢ CauchySeq u
Tactic:
rw [Metric.cauchySeq_iff']
State after:
X : Type u_1
inst✝ : MetricSpace X
a b c : X
r : ℝ
u : ℕ → X
hu : ∀ (n : ℕ), dist (u n) (u (n + 1)) ≤ (1 / 2) ^ n
⊢ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) (u N) < ε

State before:
X : Type u_1
inst✝ : MetricSpace X
a b c : X
r : ℝ
u : ℕ → X
hu : ∀ (n : ℕ), dist (u n) (u (n + 1)) ≤ (1 / 2) ^ n
⊢ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) (u N) < ε
Tactic:
intro ε ε_pos
State after:
X : Type u_1
inst✝ : MetricSpace X
a b c : X
r : ℝ
u : ℕ → X
hu : ∀ (n : ℕ), dist (u n) (u (n + 1)) ≤ (1 / 2) ^ n
ε : ℝ
ε_pos : ε > 0
⊢ ∃ N, ∀ n ≥ N, dist (u n) (u N) < ε

State before:
X : Type u_1
inst✝ : MetricSpace X
a b c : X
r : ℝ
u : ℕ → X
hu : ∀ (n : ℕ), dist (u n) (u (n + 1)) ≤ (1 / 2) ^ n
ε : ℝ
ε_pos : ε > 0
⊢ ∃ N, ∀ n ≥ N, dist (u n) (u N) < ε
Tactic:
obtain ⟨N, hN⟩ : ∃ N : ℕ, 1 / 2 ^ N * 2 < ε := by sorry
State after:
case intro
X : Type u_1
inst✝ : MetricSpace X
a b c : X
r : ℝ
u : ℕ → X
hu : ∀ (n : ℕ), dist (u n) (u (n + 1)) ≤ (1 / 2) ^ n
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : 1 / 2 ^ N * 2 < ε
⊢ ∃ N, ∀ n ≥ N, dist (u n) (u N) < ε

State before:
case intro
X : Type u_1
inst✝ : MetricSpace X
a b c : X
r : ℝ
u : ℕ → X
hu : ∀ (n : ℕ), dist (u n) (u (n + 1)) ≤ (1 / 2) ^ n
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : 1 / 2 ^ N * 2 < ε
⊢ ∃ N, ∀ n ≥ N, dist (u n) (u N) < ε
Tactic:
use N
State after:
case h
X : Type u_1
inst✝ : MetricSpace X
a b c : X
r : ℝ
u : ℕ → X
hu : ∀ (n : ℕ), dist (u n) (u (n + 1)) ≤ (1 / 2) ^ n
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : 1 / 2 ^ N * 2 < ε
⊢ ∀ n ≥ N, dist (u n) (u N) < ε

State before:
case h
X : Type u_1
inst✝ : MetricSpace X
a b c : X
r : ℝ
u : ℕ → X
hu : ∀ (n : ℕ), dist (u n) (u (n + 1)) ≤ (1 / 2) ^ n
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : 1 / 2 ^ N * 2 < ε
⊢ ∀ n ≥ N, dist (u n) (u N) < ε
Tactic:
intro n hn
State after:
case h
X : Type u_1
inst✝ : MetricSpace X
a b c : X
r : ℝ
u : ℕ → X
hu : ∀ (n : ℕ), dist (u n) (u (n + 1)) ≤ (1 / 2) ^ n
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : 1 / 2 ^ N * 2 < ε
n : ℕ
hn : n ≥ N
⊢ dist (u n) (u N) < ε

State before:
case h
X : Type u_1
inst✝ : MetricSpace X
a b c : X
r : ℝ
u : ℕ → X
hu : ∀ (n : ℕ), dist (u n) (u (n + 1)) ≤ (1 / 2) ^ n
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : 1 / 2 ^ N * 2 < ε
n : ℕ
hn : n ≥ N
⊢ dist (u n) (u N) < ε
Tactic:
obtain ⟨k, rfl : n = N + k⟩ := le_iff_exists_add.mp hn
State after:
case h.intro
X : Type u_1
inst✝ : MetricSpace X
a b c : X
r : ℝ
u : ℕ → X
hu : ∀ (n : ℕ), dist (u n) (u (n + 1)) ≤ (1 / 2) ^ n
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : 1 / 2 ^ N * 2 < ε
k : ℕ
hn : N + k ≥ N
⊢ dist (u (N + k)) (u N) < ε

State before:
case h.intro
X : Type u_1
inst✝ : MetricSpace X
a b c : X
r : ℝ
u : ℕ → X
hu : ∀ (n : ℕ), dist (u n) (u (n + 1)) ≤ (1 / 2) ^ n
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : 1 / 2 ^ N * 2 < ε
k : ℕ
hn : N + k ≥ N
⊢ dist (u (N + k)) (u N) < ε
Tactic:
calc
  dist (u (N + k)) (u N) = dist (u (N + 0)) (u (N + k)) := sorry
  _ ≤ ∑ i in range k, dist (u (N + i)) (u (N + (i + 1))) := sorry
  _ ≤ ∑ i in range k, (1 / 2 : ℝ) ^ (N + i) := sorry
  _ = 1 / 2 ^ N * ∑ i in range k, (1 / 2 : ℝ) ^ i := sorry
  _ ≤ 1 / 2 ^ N * 2 := sorry
  _ < ε := sorry
State after:
no goals

State before:
X : Type u_1
inst✝ : MetricSpace X
a b c : X
r : ℝ
u : ℕ → X
hu : ∀ (n : ℕ), dist (u n) (u (n + 1)) ≤ (1 / 2) ^ n
ε : ℝ
ε_pos : ε > 0
⊢ ∃ N, 1 / 2 ^ N * 2 < ε
Tactic:
sorry
State after:
no goals