-- Mathlib/Topology/Algebra/InfiniteSum/Nonarchimedean.lean
theorem cauchySeq_prod_of_tendsto_cofinite_one {f : α → G} (hf : Tendsto f cofinite (𝓝 1)) :
    CauchySeq (fun s ↦ ∏ i ∈ s, f i)

Proof state:
case intro
α : Type u_1
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformGroup G
inst✝ : NonarchimedeanGroup G
f : α → G
hf : Tendsto f cofinite (𝓝 1)
U : Set G
hU : U ∈ 𝓝 1
V : OpenSubgroup G
hV : ↑V ⊆ U
⊢ ∃ s, ∀ (t : Finset α), Disjoint t s → ∏ b ∈ t, f b ∈ U

Tactic:
use (tendsto_def.mp hf V V.mem_nhds_one).toFinset

Result:
case h
α : Type u_1
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformGroup G
inst✝ : NonarchimedeanGroup G
f : α → G
hf : Tendsto f cofinite (𝓝 1)
U : Set G
hU : U ∈ 𝓝 1
V : OpenSubgroup G
hV : ↑V ⊆ U
⊢ ∀ (t : Finset α), Disjoint t (Set.Finite.toFinset ⋯) → ∏ b ∈ t, f b ∈ U

Proof state:
case h.a
α : Type u_1
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformGroup G
inst✝ : NonarchimedeanGroup G
f : α → G
hf : Tendsto f cofinite (𝓝 1)
U : Set G
hU : U ∈ 𝓝 1
V : OpenSubgroup G
hV : ↑V ⊆ U
t : Finset α
ht : Disjoint t (Set.Finite.toFinset ⋯)
⊢ ∏ b ∈ t, f b ∈ ↑V

Tactic:
apply Subgroup.prod_mem

Result:
case h.a.h
α : Type u_1
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformGroup G
inst✝ : NonarchimedeanGroup G
f : α → G
hf : Tendsto f cofinite (𝓝 1)
U : Set G
hU : U ∈ 𝓝 1
V : OpenSubgroup G
hV : ↑V ⊆ U
t : Finset α
ht : Disjoint t (Set.Finite.toFinset ⋯)
⊢ ∀ c ∈ t, f c ∈ ↑V

Proof state:
α : Type u_1
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformGroup G
inst✝ : NonarchimedeanGroup G
f : α → G
hf : Tendsto f cofinite (𝓝 1)
U : Set G
hU : U ∈ 𝓝 1
⊢ ∃ s, ∀ (t : Finset α), Disjoint t s → ∏ b ∈ t, f b ∈ U

Tactic:
rcases is_nonarchimedean U hU with ⟨V, hV⟩

Result:
case intro
α : Type u_1
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformGroup G
inst✝ : NonarchimedeanGroup G
f : α → G
hf : Tendsto f cofinite (𝓝 1)
U : Set G
hU : U ∈ 𝓝 1
V : OpenSubgroup G
hV : ↑V ⊆ U
⊢ ∃ s, ∀ (t : Finset α), Disjoint t s → ∏ b ∈ t, f b ∈ U

Proof state:
α : Type u_1
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformGroup G
inst✝ : NonarchimedeanGroup G
f : α → G
hf : Tendsto f cofinite (𝓝 1)
⊢ CauchySeq fun s => ∏ i ∈ s, f i

Tactic:
apply cauchySeq_finset_iff_prod_vanishing.mpr

Result:
α : Type u_1
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformGroup G
inst✝ : NonarchimedeanGroup G
f : α → G
hf : Tendsto f cofinite (𝓝 1)
⊢ ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset α), Disjoint t s → ∏ b ∈ t, f b ∈ e

Proof state:
case h.a.h
α : Type u_1
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformGroup G
inst✝ : NonarchimedeanGroup G
f : α → G
hf : Tendsto f cofinite (𝓝 1)
U : Set G
hU : U ∈ 𝓝 1
V : OpenSubgroup G
hV : ↑V ⊆ U
t : Finset α
ht : Disjoint t (Set.Finite.toFinset ⋯)
⊢ ∀ c ∈ t, f c ∈ ↑V

Tactic:
intro i hi

Result:
case h.a.h
α : Type u_1
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformGroup G
inst✝ : NonarchimedeanGroup G
f : α → G
hf : Tendsto f cofinite (𝓝 1)
U : Set G
hU : U ∈ 𝓝 1
V : OpenSubgroup G
hV : ↑V ⊆ U
t : Finset α
ht : Disjoint t (Set.Finite.toFinset ⋯)
i : α
hi : i ∈ t
⊢ f i ∈ ↑V

Proof state:
case h.a.h
α : Type u_1
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformGroup G
inst✝ : NonarchimedeanGroup G
f : α → G
hf : Tendsto f cofinite (𝓝 1)
U : Set G
hU : U ∈ 𝓝 1
V : OpenSubgroup G
hV : ↑V ⊆ U
t : Finset α
ht : Disjoint t (Set.Finite.toFinset ⋯)
i : α
hi : i ∈ t
⊢ f i ∈ ↑V

Tactic:
simpa using Finset.disjoint_left.mp ht hi

Result:
no goals

Proof state:
case h
α : Type u_1
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformGroup G
inst✝ : NonarchimedeanGroup G
f : α → G
hf : Tendsto f cofinite (𝓝 1)
U : Set G
hU : U ∈ 𝓝 1
V : OpenSubgroup G
hV : ↑V ⊆ U
⊢ ∀ (t : Finset α), Disjoint t (Set.Finite.toFinset ⋯) → ∏ b ∈ t, f b ∈ U

Tactic:
intro t ht

Result:
case h
α : Type u_1
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformGroup G
inst✝ : NonarchimedeanGroup G
f : α → G
hf : Tendsto f cofinite (𝓝 1)
U : Set G
hU : U ∈ 𝓝 1
V : OpenSubgroup G
hV : ↑V ⊆ U
t : Finset α
ht : Disjoint t (Set.Finite.toFinset ⋯)
⊢ ∏ b ∈ t, f b ∈ U

Proof state:
case h
α : Type u_1
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformGroup G
inst✝ : NonarchimedeanGroup G
f : α → G
hf : Tendsto f cofinite (𝓝 1)
U : Set G
hU : U ∈ 𝓝 1
V : OpenSubgroup G
hV : ↑V ⊆ U
t : Finset α
ht : Disjoint t (Set.Finite.toFinset ⋯)
⊢ ∏ b ∈ t, f b ∈ U

Tactic:
apply hV

Result:
case h.a
α : Type u_1
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformGroup G
inst✝ : NonarchimedeanGroup G
f : α → G
hf : Tendsto f cofinite (𝓝 1)
U : Set G
hU : U ∈ 𝓝 1
V : OpenSubgroup G
hV : ↑V ⊆ U
t : Finset α
ht : Disjoint t (Set.Finite.toFinset ⋯)
⊢ ∏ b ∈ t, f b ∈ ↑V

Proof state:
α : Type u_1
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformGroup G
inst✝ : NonarchimedeanGroup G
f : α → G
hf : Tendsto f cofinite (𝓝 1)
⊢ ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset α), Disjoint t s → ∏ b ∈ t, f b ∈ e

Tactic:
intro U hU

Result:
α : Type u_1
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformGroup G
inst✝ : NonarchimedeanGroup G
f : α → G
hf : Tendsto f cofinite (𝓝 1)
U : Set G
hU : U ∈ 𝓝 1
⊢ ∃ s, ∀ (t : Finset α), Disjoint t s → ∏ b ∈ t, f b ∈ U