-- Mathlib/Topology/UniformSpace/Cauchy.lean
theorem cauchySeq_shift {u : ℕ → α} (k : ℕ) : CauchySeq (fun n ↦ u (n + k)) ↔ CauchySeq u

Proof state:
case h
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h✝ : ∀ V ∈ 𝓤 α, ∃ N, ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
V : Set (α × α)
mV : V ∈ 𝓤 α
N : ℕ
h : ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
⊢ ∀ k_1 ≥ N + k, ∀ l ≥ N + k, (u k_1, u l) ∈ V

Tactic:
intro a ha b hb

Result:
case h
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h✝ : ∀ V ∈ 𝓤 α, ∃ N, ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
V : Set (α × α)
mV : V ∈ 𝓤 α
N : ℕ
h : ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
a : ℕ
ha : a ≥ N + k
b : ℕ
hb : b ≥ N + k
⊢ (u a, u b) ∈ V

Proof state:
case mp
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h : CauchySeq fun n => u (n + k)
⊢ CauchySeq u

Tactic:
rw [cauchySeq_iff] at h ⊢

Result:
case mp
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h : ∀ V ∈ 𝓤 α, ∃ N, ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
⊢ ∀ V ∈ 𝓤 α, ∃ N, ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V

Proof state:
case mp
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h : ∀ V ∈ 𝓤 α, ∃ N, ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
V : Set (α × α)
mV : V ∈ 𝓤 α
⊢ ∃ N, ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V

Tactic:
obtain ⟨N, h⟩ := h V mV

Result:
case mp.intro
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h✝ : ∀ V ∈ 𝓤 α, ∃ N, ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
V : Set (α × α)
mV : V ∈ 𝓤 α
N : ℕ
h : ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
⊢ ∃ N, ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V

Proof state:
case mp
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h : ∀ V ∈ 𝓤 α, ∃ N, ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
⊢ ∀ V ∈ 𝓤 α, ∃ N, ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V

Tactic:
intro V mV

Result:
case mp
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h : ∀ V ∈ 𝓤 α, ∃ N, ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
V : Set (α × α)
mV : V ∈ 𝓤 α
⊢ ∃ N, ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V

Proof state:
case h
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h✝ : ∀ V ∈ 𝓤 α, ∃ N, ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
V : Set (α × α)
mV : V ∈ 𝓤 α
N : ℕ
h : ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
a : ℕ
ha : a ≥ N + k
b : ℕ
hb : b ≥ N + k
⊢ (u a, u b) ∈ V

Tactic:
convert h (a - k) (Nat.le_sub_of_add_le ha) (b - k) (Nat.le_sub_of_add_le hb) <;> omega

Result:
no goals

Proof state:
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
⊢ (CauchySeq fun n => u (n + k)) ↔ CauchySeq u

Tactic:
constructor <;> intro h

Result:
case mp
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h : CauchySeq fun n => u (n + k)
⊢ CauchySeq u

case mpr
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h : CauchySeq u
⊢ CauchySeq fun n => u (n + k)

Proof state:
case mp.intro
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h✝ : ∀ V ∈ 𝓤 α, ∃ N, ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
V : Set (α × α)
mV : V ∈ 𝓤 α
N : ℕ
h : ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
⊢ ∃ N, ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V

Tactic:
use N + k

Result:
case h
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h✝ : ∀ V ∈ 𝓤 α, ∃ N, ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
V : Set (α × α)
mV : V ∈ 𝓤 α
N : ℕ
h : ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
⊢ ∀ k_1 ≥ N + k, ∀ l ≥ N + k, (u k_1, u l) ∈ V

Proof state:
case mpr
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h : CauchySeq u
⊢ CauchySeq fun n => u (n + k)

Tactic:
exact h.comp_tendsto (tendsto_add_atTop_nat k)

Result:
no goals