-- Mathlib/Topology/Algebra/InfiniteSum/Nonarchimedean.lean
/-- Let `G` be a nonarchimedean abelian group, and let `f : ℕ → G` be a function
such that the quotients `f (n + 1) / f n` tend to one. Then the function is a Cauchy sequence. -/
@[to_additive "Let `G` be a nonarchimedean additive abelian group, and let `f : ℕ → G` be a
function such that the differences `f (n + 1) - f n` tend to zero.
Then the function is a Cauchy sequence."]
lemma cauchySeq_of_tendsto_div_nhds_one {f : ℕ → G}
    (hf : Tendsto (fun n ↦ f (n + 1) / f n) atTop (𝓝 1)) :
    CauchySeq f

Proof state:
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformGroup G
inst✝ : NonarchimedeanGroup G
f : ℕ → G
hf : Tendsto (fun n => f (n + 1) / f n) atTop (𝓝 1)
⊢ ∀ s ∈ 𝓝 1, ∃ a, ∀ b ≥ a, f b.2 / f b.1 ∈ s

Tactic:
intro s hs

Result:
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformGroup G
inst✝ : NonarchimedeanGroup G
f : ℕ → G
hf : Tendsto (fun n => f (n + 1) / f n) atTop (𝓝 1)
s : Set G
hs : s ∈ 𝓝 1
⊢ ∃ a, ∀ b ≥ a, f b.2 / f b.1 ∈ s

Proof state:
case intro.intro
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformGroup G
inst✝ : NonarchimedeanGroup G
f : ℕ → G
hf : Tendsto (fun n => f (n + 1) / f n) atTop (𝓝 1)
s : Set G
hs : s ∈ 𝓝 1
t : OpenSubgroup G
ht : ↑t ⊆ s
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → f (b + 1) / f b ∈ t
⊢ ∀ b ≥ (N, N), f b.2 / f b.1 ∈ s

Tactic:
rintro ⟨M, M'⟩ ⟨(hMN : N ≤ M), (hMN' : N ≤ M')⟩

Result:
case intro.intro.mk.intro
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformGroup G
inst✝ : NonarchimedeanGroup G
f : ℕ → G
hf : Tendsto (fun n => f (n + 1) / f n) atTop (𝓝 1)
s : Set G
hs : s ∈ 𝓝 1
t : OpenSubgroup G
ht : ↑t ⊆ s
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → f (b + 1) / f b ∈ t
M M' : ℕ
hMN : N ≤ M
hMN' : N ≤ M'
⊢ f (M, M').2 / f (M, M').1 ∈ s

Proof state:
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformGroup G
inst✝ : NonarchimedeanGroup G
f : ℕ → G
hf : Tendsto (fun n => f (n + 1) / f n) atTop (𝓝 1)
s : Set G
hs : s ∈ 𝓝 1
t : OpenSubgroup G
ht : ↑t ⊆ s
⊢ ∃ N, ∀ (b : ℕ), N ≤ b → f (b + 1) / f b ∈ t

Tactic:
simpa using tendsto_def.mp hf t t.mem_nhds_one

Result:
no goals

Proof state:
case intro.intro.mk.intro.a
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformGroup G
inst✝ : NonarchimedeanGroup G
f : ℕ → G
hf : Tendsto (fun n => f (n + 1) / f n) atTop (𝓝 1)
s : Set G
hs : s ∈ 𝓝 1
t : OpenSubgroup G
ht : ↑t ⊆ s
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → f (b + 1) / f b ∈ t
M M' : ℕ
hMN : N ≤ M
hMN' : N ≤ M'
⊢ f (M, M').2 / f (M, M').1 ∈ ↑t

Tactic:
wlog h : M ≤ M' generalizing M M'

Result:
case intro.intro.mk.intro.a.inr
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformGroup G
inst✝ : NonarchimedeanGroup G
f : ℕ → G
hf : Tendsto (fun n => f (n + 1) / f n) atTop (𝓝 1)
s : Set G
hs : s ∈ 𝓝 1
t : OpenSubgroup G
ht : ↑t ⊆ s
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → f (b + 1) / f b ∈ t
M M' : ℕ
hMN : N ≤ M
hMN' : N ≤ M'
this : ∀ (M M' : ℕ), N ≤ M → N ≤ M' → M ≤ M' → f (M, M').2 / f (M, M').1 ∈ ↑t
h : ¬M ≤ M'
⊢ f (M, M').2 / f (M, M').1 ∈ ↑t

G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformGroup G
inst✝ : NonarchimedeanGroup G
f : ℕ → G
hf : Tendsto (fun n => f (n + 1) / f n) atTop (𝓝 1)
s : Set G
hs : s ∈ 𝓝 1
t : OpenSubgroup G
ht : ↑t ⊆ s
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → f (b + 1) / f b ∈ t
M M' : ℕ
hMN : N ≤ M
hMN' : N ≤ M'
h : M ≤ M'
⊢ f (M, M').2 / f (M, M').1 ∈ ↑t

Proof state:
case intro.succ
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformGroup G
inst✝ : NonarchimedeanGroup G
f : ℕ → G
hf : Tendsto (fun n => f (n + 1) / f n) atTop (𝓝 1)
s : Set G
hs : s ∈ 𝓝 1
t : OpenSubgroup G
ht : ↑t ⊆ s
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → f (b + 1) / f b ∈ t
M : ℕ
hMN : N ≤ M
k : ℕ
ih : f (M, M + k).2 / f (M, M + k).1 ∈ ↑t
⊢ f (M, M + (k + 1)).2 / f (M, M + (k + 1)).1 ∈ ↑t

Tactic:
simpa using t.mul_mem (hN _ (by omega : N ≤ M + k)) ih

Result:
no goals

Proof state:
case intro
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformGroup G
inst✝ : NonarchimedeanGroup G
f : ℕ → G
hf : Tendsto (fun n => f (n + 1) / f n) atTop (𝓝 1)
s : Set G
hs : s ∈ 𝓝 1
t : OpenSubgroup G
ht : ↑t ⊆ s
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → f (b + 1) / f b ∈ t
M : ℕ
hMN : N ≤ M
k : ℕ
⊢ f (M, M + k).2 / f (M, M + k).1 ∈ ↑t

Tactic:
induction k with
| zero => simpa using one_mem t
| succ k ih => simpa using t.mul_mem (hN _ (by omega : N ≤ M + k)) ih

Result:
no goals