awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
α : Type u_3
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsUniformAddGroup α
inst_3 : CompleteSpace α
f : ℕ → α
hf : Summable f
⊢ Injective (β := ℕ) fun (b : ℕ) ↦ 2 * b + 1

Tactic:
(add_left_injective 1).comp (mul_right_injective₀ (two_ne_zero' ℕ))

Premises used: mul_right_injective₀, two_ne_zero', Function.Injective.comp, Nat, add_left_injective, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
α : Type u_3
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsUniformAddGroup α
inst_3 : CompleteSpace α
f : ℕ → α
hf : Summable f
⊢ Injective (β := ℕ) fun (b : ℕ) ↦ 2 * b + 1

Tactic:
exact (add_left_injective 1).comp (mul_right_injective₀ (two_ne_zero' ℕ))

Premises used: mul_right_injective₀, two_ne_zero', Function.Injective.comp, Nat, add_left_injective, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
f : ℕ → M
⊢ (Multipliable.{u_1, 0} (α := M) fun (x : ℕ+) ↦ f (↑x : ℕ)) ↔ Multipliable.{u_1, 0} (α := M) fun (x : ℕ) ↦ f (x + 1)

Tactic:
Equiv.pnatEquivNat.symm.multipliable_iff.symm

Premises used: PNat.val, Equiv.pnatEquivNat, Equiv.symm, Equiv.multipliable_iff, Iff.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
f : ℕ → G
rw : (Multipliable.{u_2, 0} (α := G) fun (x : ℕ) ↦ f (x + 1)) ↔ Multipliable f
rw₁ rw₂ : Multipliable f ↔ Multipliable f
⊢ (Multipliable.{u_2, 0} (α := G) fun (n : ℕ+) ↦ f (↑n : ℕ)) ↔ Multipliable f

Tactic:
rw [multipliable_pnat_iff_multipliable_succ, multipliable_nat_add_iff]

Premises used: multipliable_pnat_iff_multipliable_succ, multipliable_nat_add_iff
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
f : ℕ → M
⊢ Eq.{u_1 + 1} (α := M) (∏' (n : ℕ+), f (↑n : ℕ)) (∏' (n : ℕ), f (n + 1))

Tactic:
(Equiv.pnatEquivNat.symm.tprod_eq _).symm

Premises used: PNat.val, Equiv.tprod_eq, Equiv.pnatEquivNat, Equiv.symm, Eq.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : T2Space G
f : ℕ → G
hf : Multipliable f
⊢ f 0 * ∏' (n : ℕ+), f (↑n : ℕ) = ∏' (n : ℕ), f n

Tactic:
simpa [hf.tprod_eq_zero_mul] using tprod_pnat_eq_tprod_succ

Premises used: tprod_pnat_eq_tprod_succ, Multipliable.tprod_eq_zero_mul
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
inst_3 : CompleteSpace G
inst_4 : T2Space G
f : ℤ → G
hf2 : Multipliable f
⊢ Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (↑n : ℤ)

Tactic:
have h1 : Multipliable fun n : ℕ ↦ f n :=
    (multipliable_int_iff_multipliable_nat_and_neg.mp hf2).1
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
inst_3 : CompleteSpace G
inst_4 : T2Space G
f : ℤ → G
hf2 : Multipliable f
h1 : Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (↑n : ℤ)
⊢ Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (-(↑n : ℤ))

Tactic:
have h2 : Multipliable fun n : ℕ ↦ f (-n) :=
    (multipliable_int_iff_multipliable_nat_and_neg.mp hf2).2
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
inst_3 : CompleteSpace G
inst_4 : T2Space G
f : ℤ → G
hf2 : Multipliable f
h1 : Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (↑n : ℤ)
h2 : Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (-(↑n : ℤ))
rwa : Multipliable.{u_2, 0} (α := G) fun (x : ℕ) ↦ f (↑(x + 1) : ℤ)
rwa₁ rwa₂ rwa₃ rwa₄ : Multipliable.{u_2, 0} (α := G) fun (x : ℕ) ↦ f (↑x : ℤ)
⊢ Multipliable.{u_2, 0} (α := G) fun (n : ℕ+) ↦ f (↑(↑n : ℕ) : ℤ)

Tactic:
rwa [multipliable_pnat_iff_multipliable_succ (f := (f ·)),
      multipliable_nat_add_iff 1 (f := (f ·))]

Premises used: multipliable_pnat_iff_multipliable_succ, multipliable_nat_add_iff, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
inst_3 : CompleteSpace G
inst_4 : T2Space G
f : ℤ → G
hf2 : Multipliable f
h1 : Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (↑n : ℤ)
h2 : Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (-(↑n : ℤ))
⊢ Multipliable.{u_2, 0} (α := G) fun (n : ℕ+) ↦ f (↑(↑n : ℕ) : ℤ)

Tactic:
have h3 : Multipliable fun n : ℕ+ ↦ f n := by
    rwa [multipliable_pnat_iff_multipliable_succ (f := (f ·)),
      multipliable_nat_add_iff 1 (f := (f ·))]
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
inst_3 : CompleteSpace G
inst_4 : T2Space G
f : ℤ → G
hf2 : Multipliable f
h1 : Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (↑n : ℤ)
h2 : Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (-(↑n : ℤ))
h3 : Multipliable.{u_2, 0} (α := G) fun (n : ℕ+) ↦ f (↑(↑n : ℕ) : ℤ)
rwa : Multipliable.{u_2, 0} (α := G) fun (x : ℕ) ↦ f (-(↑(x + 1) : ℤ))
rwa₁ rwa₂ rwa₃ rwa₄ : Multipliable.{u_2, 0} (α := G) fun (x : ℕ) ↦ f (-(↑x : ℤ))
⊢ Multipliable.{u_2, 0} (α := G) fun (n : ℕ+) ↦ f (-(↑(↑n : ℕ) : ℤ))

Tactic:
rwa [multipliable_pnat_iff_multipliable_succ (f := (fun x ↦ f (-x))),
      multipliable_nat_add_iff 1 (f := (fun x ↦ f (-x)))]

Premises used: multipliable_pnat_iff_multipliable_succ, multipliable_nat_add_iff, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
inst_3 : CompleteSpace G
inst_4 : T2Space G
f : ℤ → G
hf2 : Multipliable f
h1 : Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (↑n : ℤ)
h2 : Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (-(↑n : ℤ))
h3 : Multipliable.{u_2, 0} (α := G) fun (n : ℕ+) ↦ f (↑(↑n : ℕ) : ℤ)
⊢ Multipliable.{u_2, 0} (α := G) fun (n : ℕ+) ↦ f (-(↑(↑n : ℕ) : ℤ))

Tactic:
have h4 : Multipliable fun n : ℕ+ ↦ f (-n) := by
    rwa [multipliable_pnat_iff_multipliable_succ (f := (fun x ↦ f (-x))),
      multipliable_nat_add_iff 1 (f := (fun x ↦ f (-x)))]
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
inst_3 : CompleteSpace G
inst_4 : T2Space G
f : ℤ → G
hf2 : Multipliable f
h1 : Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (↑n : ℤ)
h2 : Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (-(↑n : ℤ))
h3 : Multipliable.{u_2, 0} (α := G) fun (n : ℕ+) ↦ f (↑(↑n : ℕ) : ℤ)
h4 : Multipliable.{u_2, 0} (α := G) fun (n : ℕ+) ↦ f (-(↑(↑n : ℕ) : ℤ))
⊢ ∏' (n : ℕ), f (↑n : ℤ) * f (-(↑n : ℤ)) = (∏' (n : ℤ), f n) * f 0

Tactic:
have := tprod_nat_mul_neg hf2
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
inst_3 : CompleteSpace G
inst_4 : T2Space G
f : ℤ → G
hf2 : Multipliable f
h1 : Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (↑n : ℤ)
h2 : Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (-(↑n : ℤ))
h3 : Multipliable.{u_2, 0} (α := G) fun (n : ℕ+) ↦ f (↑(↑n : ℕ) : ℤ)
h4 : Multipliable.{u_2, 0} (α := G) fun (n : ℕ+) ↦ f (-(↑(↑n : ℕ) : ℤ))
this : ∏' (n : ℕ), f (↑n : ℤ) * f (-(↑n : ℤ)) = (∏' (n : ℤ), f n) * f 0
⊢ Multipliable.{u_2, 0} (α := G) fun (b : ℕ) ↦ f (↑b : ℤ) * f (-(↑b : ℤ))

Tactic:
simpa using h1.mul h2

Premises used: Multipliable.mul
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
inst_3 : CompleteSpace G
inst_4 : T2Space G
f : ℤ → G
hf2 : Multipliable f
h1 : Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (↑n : ℤ)
h2 : Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (-(↑n : ℤ))
h3 : Multipliable.{u_2, 0} (α := G) fun (n : ℕ+) ↦ f (↑(↑n : ℕ) : ℤ)
h4 : Multipliable.{u_2, 0} (α := G) fun (n : ℕ+) ↦ f (-(↑(↑n : ℕ) : ℤ))
this : ∏' (n : ℕ), f (↑n : ℤ) * f (-(↑n : ℤ)) = (∏' (n : ℤ), f n) * f 0
⊢ f 0 * ∏' (n : ℕ+), f (↑(↑n : ℕ) : ℤ) * f (-(↑(↑n : ℕ) : ℤ)) = ∏' (n : ℤ), f n

Tactic:
simp only [← tprod_zero_pnat_eq_tprod_nat (by simpa using h1.mul h2), Nat.cast_zero, neg_zero,
    mul_comm _ (f 0), mul_assoc, mul_right_inj] at this

Premises used: mul_assoc, tprod_zero_pnat_eq_tprod_nat, mul_right_inj, mul_comm, Nat.cast_zero, OfNat.ofNat, neg_zero
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
inst_3 : CompleteSpace G
inst_4 : T2Space G
f : ℤ → G
hf2 : Multipliable f
h1 : Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (↑n : ℤ)
h2 : Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (-(↑n : ℤ))
h3 : Multipliable.{u_2, 0} (α := G) fun (n : ℕ+) ↦ f (↑(↑n : ℕ) : ℤ)
h4 : Multipliable.{u_2, 0} (α := G) fun (n : ℕ+) ↦ f (-(↑(↑n : ℕ) : ℤ))
this : f 0 * ∏' (n : ℕ+), f (↑(↑n : ℕ) : ℤ) * f (-(↑(↑n : ℕ) : ℤ)) = ∏' (n : ℤ), f n
⊢ ∏' (n : ℤ), f n = (f 0 * ∏' (n : ℕ+), f (↑(↑n : ℕ) : ℤ)) * ∏' (n : ℕ+), f (-(↑(↑n : ℕ) : ℤ))

Tactic:
simp [← this, h3.tprod_mul h4, ← mul_assoc]

Premises used: mul_assoc, Multipliable.tprod_mul
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
inst_3 : CompleteSpace G
inst_4 : T2Space G
f : ℤ → G
hf : Function.Even f
hf2 : Multipliable f
⊢ ∏' (n : ℤ), f n = f 0 * HPow.hPow (α := G) (β := ℕ) (∏' (n : ℕ+), f (↑(↑n : ℕ) : ℤ)) 2

Tactic:
simpa only [sq, ← mul_assoc, hf _] using tprod_int_eq_zero_mul_tprod_pnat hf2

Premises used: mul_assoc, sq, tprod_int_eq_zero_mul_tprod_pnat
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
Goal:
α : Type u_1
G : Type u_2
inst : CommGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
inst_3 : NonarchimedeanGroup G
f : α → G
hf : Tendsto f cofinite (𝓝 1)
apply :
  ∀ (e : Set G),
    Membership.mem (γ := Filter G) (𝓝 1) e → ∃ (s : Finset α), ∀ (t : Finset α), Disjoint t s → ∏ b ∈ t, f b ∈ e
⊢ CauchySeq.{u_2, u_1} (α := G) fun (s : Finset α) ↦ ∏ i ∈ s, f i

Tactic:
apply cauchySeq_finset_iff_prod_vanishing.mpr

Premises used: Iff.mpr, cauchySeq_finset_iff_prod_vanishing
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
Goal:
α : Type u_1
G : Type u_2
inst : CommGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
inst_3 : NonarchimedeanGroup G
f : α → G
hf : Tendsto f cofinite (𝓝 1)
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
rcases :
  ∀ (V : OpenSubgroup G) (hV : (↑V : Set G) ⊆ U), ∃ (s : Finset α), ∀ (t : Finset α), Disjoint t s → ∏ b ∈ t, f b ∈ U
⊢ ∃ (s : Finset α), ∀ (t : Finset α), Disjoint t s → ∏ b ∈ t, f b ∈ U

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

Premises used: NonarchimedeanGroup.is_nonarchimedean
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
Goal:
α : Type u_1
G : Type u_2
inst : CommGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
inst_3 : NonarchimedeanGroup G
f : α → G
hf : Tendsto f cofinite (𝓝 1)
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
V : OpenSubgroup G
hV : (↑V : Set G) ⊆ U
h : ∀ (t : Finset α), Disjoint t (Set.Finite.toFinset (s := (f ⁻¹' (↑V : Set G))ᶜ) ⋯) → ∏ b ∈ t, f b ∈ U
⊢ ∃ (s : Finset α), ∀ (t : Finset α), Disjoint t s → ∏ b ∈ t, f b ∈ U

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

Premises used: Filter.tendsto_def, OpenSubgroup.mem_nhds_one, SetLike.coe, Set.Finite.toFinset, Iff.mp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
Goal:
α : Type u_1
G : Type u_2
inst : CommGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
inst_3 : NonarchimedeanGroup G
f : α → G
hf : Tendsto f cofinite (𝓝 1)
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
V : OpenSubgroup G
hV : (↑V : Set G) ⊆ U
t : Finset α
ht : Disjoint t (Set.Finite.toFinset (s := (f ⁻¹' (↑V : Set G))ᶜ) ⋯)
h : ∏ b ∈ t, f b ∈ (↑V : Set G)
⊢ ∏ b ∈ t, f b ∈ U

Tactic:
apply hV
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
Goal:
α : Type u_1
G : Type u_2
inst : CommGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
inst_3 : NonarchimedeanGroup G
f : α → G
hf : Tendsto f cofinite (𝓝 1)
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
V : OpenSubgroup G
hV : (↑V : Set G) ⊆ U
t : Finset α
ht : Disjoint t (Set.Finite.toFinset (s := (f ⁻¹' (↑V : Set G))ᶜ) ⋯)
h : ∀ c ∈ t, f c ∈ (↑V : Subgroup G)
⊢ ∏ b ∈ t, f b ∈ (↑V : Set G)

Tactic:
apply Subgroup.prod_mem

Premises used: Subgroup.prod_mem
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
Goal:
α : Type u_1
G : Type u_2
inst : CommGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
inst_3 : NonarchimedeanGroup G
f : α → G
hf : Tendsto f cofinite (𝓝 1)
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
V : OpenSubgroup G
hV : (↑V : Set G) ⊆ U
t : Finset α
ht : Disjoint t (Set.Finite.toFinset (s := (f ⁻¹' (↑V : Set G))ᶜ) ⋯)
i : α
hi : i ∈ t
⊢ f i ∈ (↑V : Subgroup G)

Tactic:
simpa using Finset.disjoint_left.mp ht hi

Premises used: Iff.mp, Finset.disjoint_left
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
inst_3 : NonarchimedeanGroup G
f : ℕ → G
hf : Tendsto.{0, u_2} (β := G) (fun (n : ℕ) ↦ f (n + 1) / f n) atTop (𝓝 1)
this : Tendsto.{0, u_2} (β := G) (fun (p : ℕ × ℕ) ↦ f p.2 / f p.1) atTop (𝓝 1)
⊢ CauchySeq f

Tactic:
simpa [CauchySeq,
      cauchy_map_iff, prod_atTop_atTop_eq, uniformity_eq_comap_nhds_one G, atTop_neBot]

Premises used: CauchySeq, cauchy_map_iff, Filter.atTop_neBot, Filter.prod_atTop_atTop_eq, uniformity_eq_comap_nhds_one
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
inst_3 : NonarchimedeanGroup G
f : ℕ → G
hf : Tendsto.{0, u_2} (β := G) (fun (n : ℕ) ↦ f (n + 1) / f n) atTop (𝓝 1)
suffices : Tendsto.{0, u_2} (β := G) (fun (p : ℕ × ℕ) ↦ f p.2 / f p.1) atTop (𝓝 1)
⊢ CauchySeq f

Tactic:
suffices Tendsto (fun p : ℕ × ℕ ↦ f p.2 / f p.1) atTop (𝓝 1) by simpa [CauchySeq,
      cauchy_map_iff, prod_atTop_atTop_eq, uniformity_eq_comap_nhds_one G, atTop_neBot]
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
inst_3 : NonarchimedeanGroup G
f : ℕ → G
hf : Tendsto.{0, u_2} (β := G) (fun (n : ℕ) ↦ f (n + 1) / f n) atTop (𝓝 1)
rw : ∀ (s : Set G), Membership.mem (γ := Filter G) (𝓝 1) s → ∃ (a : ℕ × ℕ), ∀ b ≥ a, f b.2 / f b.1 ∈ s
⊢ Tendsto.{0, u_2} (β := G) (fun (p : ℕ × ℕ) ↦ f p.2 / f p.1) atTop (𝓝 1)

Tactic:
rw [tendsto_atTop']

Premises used: Filter.tendsto_atTop'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
inst_3 : NonarchimedeanGroup G
f : ℕ → G
hf : Tendsto.{0, u_2} (β := G) (fun (n : ℕ) ↦ f (n + 1) / f n) atTop (𝓝 1)
s : Set G
hs : Membership.mem (γ := Filter G) (𝓝 1) s
obtain : ∀ (t : OpenSubgroup G) (ht : (↑t : Set G) ⊆ s), ∃ (a : ℕ × ℕ), ∀ b ≥ a, f b.2 / f b.1 ∈ s
⊢ ∃ (a : ℕ × ℕ), ∀ b ≥ a, f b.2 / f b.1 ∈ s

Tactic:
obtain ⟨t, ht⟩ := is_nonarchimedean s hs

Premises used: NonarchimedeanGroup.is_nonarchimedean
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
inst_3 : NonarchimedeanGroup G
f : ℕ → G
hf : Tendsto.{0, u_2} (β := G) (fun (n : ℕ) ↦ f (n + 1) / f n) atTop (𝓝 1)
s : Set G
hs : Membership.mem (γ := Filter G) (𝓝 1) s
t : OpenSubgroup G
ht : (↑t : Set G) ⊆ s
⊢ ∃ (N : ℕ), ∀ (b : ℕ), N ≤ b → f (b + 1) / f b ∈ t

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

Premises used: Filter.tendsto_def, OpenSubgroup.mem_nhds_one, SetLike.coe, Iff.mp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
inst_3 : NonarchimedeanGroup G
f : ℕ → G
hf : Tendsto.{0, u_2} (β := G) (fun (n : ℕ) ↦ f (n + 1) / f n) atTop (𝓝 1)
s : Set G
hs : Membership.mem (γ := Filter G) (𝓝 1) s
t : OpenSubgroup G
ht : (↑t : Set G) ⊆ s
obtain : ∀ (N : ℕ) (hN : ∀ (b : ℕ), N ≤ b → f (b + 1) / f b ∈ t), ∃ (a : ℕ × ℕ), ∀ b ≥ a, f b.2 / f b.1 ∈ s
⊢ ∃ (a : ℕ × ℕ), ∀ b ≥ a, f b.2 / f b.1 ∈ s

Tactic:
obtain ⟨N, hN⟩ : ∃ N : ℕ, ∀ b, N ≤ b → f (b + 1) / f b ∈ t := by
    simpa using tendsto_def.mp hf t t.mem_nhds_one
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
inst_3 : NonarchimedeanGroup G
f : ℕ → G
hf : Tendsto.{0, u_2} (β := G) (fun (n : ℕ) ↦ f (n + 1) / f n) atTop (𝓝 1)
s : Set G
hs : Membership.mem (γ := Filter G) (𝓝 1) s
t : OpenSubgroup G
ht : (↑t : Set G) ⊆ s
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → f (b + 1) / f b ∈ t
⊢ ∃ (a : ℕ × ℕ), ∀ b ≥ a, f b.2 / f b.1 ∈ s

Tactic:
⟨(N, N), ?_⟩

Premises used: Prod.mk, Exists.intro
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
inst_3 : NonarchimedeanGroup G
f : ℕ → G
hf : Tendsto.{0, u_2} (β := G) (fun (n : ℕ) ↦ f (n + 1) / f n) atTop (𝓝 1)
s : Set G
hs : Membership.mem (γ := Filter G) (𝓝 1) s
t : OpenSubgroup G
ht : (↑t : Set G) ⊆ s
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → f (b + 1) / f b ∈ t
refine : ∀ b ≥ (N, N), f b.2 / f b.1 ∈ s
⊢ ∃ (a : ℕ × ℕ), ∀ b ≥ a, f b.2 / f b.1 ∈ s

Tactic:
refine ⟨(N, N), ?_⟩
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
inst_3 : NonarchimedeanGroup G
f : ℕ → G
hf : Tendsto.{0, u_2} (β := G) (fun (n : ℕ) ↦ f (n + 1) / f n) atTop (𝓝 1)
s : Set G
hs : Membership.mem (γ := Filter G) (𝓝 1) s
t : OpenSubgroup G
ht : (↑t : Set G) ⊆ s
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → f (b + 1) / f b ∈ t
M M' : ℕ
hMN : N ≤ M
hMN' : N ≤ M'
a : f (M, M').2 / f (M, M').1 ∈ (↑t : Set G)
⊢ f (M, M').2 / f (M, M').1 ∈ s

Tactic:
apply ht
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
inst_3 : NonarchimedeanGroup G
f : ℕ → G
hf : Tendsto.{0, u_2} (β := G) (fun (n : ℕ) ↦ f (n + 1) / f n) atTop (𝓝 1)
s : Set G
hs : Membership.mem (γ := Filter G) (𝓝 1) s
t : OpenSubgroup G
ht : (↑t : Set G) ⊆ s
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → f (b + 1) / f b ∈ t
M M' : ℕ
hMN : N ≤ M
hMN' : N ≤ M'
a :
  ∀ (this : ∀ (M M' : ℕ) (hMN : N ≤ M) (hMN' : N ≤ M') (h : M ≤ M'), f (M, M').2 / f (M, M').1 ∈ (↑t : Set G))
    (h : ¬M ≤ M'), f (M, M').2 / f (M, M').1 ∈ (↑t : Set G)
wlog : ∀ (M M' : ℕ) (hMN : N ≤ M) (hMN' : N ≤ M') (h : M ≤ M'), f (M, M').2 / f (M, M').1 ∈ (↑t : Set G)
⊢ f (M, M').2 / f (M, M').1 ∈ (↑t : Set G)

Tactic:
wlog h : M ≤ M' generalizing M M'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
inst_3 : NonarchimedeanGroup G
f : ℕ → G
hf : Tendsto.{0, u_2} (β := G) (fun (n : ℕ) ↦ f (n + 1) / f n) atTop (𝓝 1)
s : Set G
hs : Membership.mem (γ := Filter G) (𝓝 1) s
t : OpenSubgroup G
ht : (↑t : Set G) ⊆ s
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → f (b + 1) / f b ∈ t
M M' : ℕ
hMN : N ≤ M
hMN' : N ≤ M'
this : ∀ (M M' : ℕ) (hMN : N ≤ M) (hMN' : N ≤ M') (h : M ≤ M'), f (M, M').2 / f (M, M').1 ∈ (↑t : Set G)
h : ¬M ≤ M'
⊢ f (M, M').2 / f (M, M').1 ∈ (↑t : Set G)

Tactic:
simpa [inv_div] using t.inv_mem <| this _ _ hMN' hMN (le_of_not_ge h)

Premises used: le_of_not_ge, Subgroup.inv_mem, inv_div, OpenSubgroup.toSubgroup
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
inst_3 : NonarchimedeanGroup G
f : ℕ → G
hf : Tendsto.{0, u_2} (β := G) (fun (n : ℕ) ↦ f (n + 1) / f n) atTop (𝓝 1)
s : Set G
hs : Membership.mem (γ := Filter G) (𝓝 1) s
t : OpenSubgroup G
ht : (↑t : Set G) ⊆ s
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → f (b + 1) / f b ∈ t
M M' : ℕ
hMN : N ≤ M
hMN' : N ≤ M'
h : M ≤ M'
obtain : ∀ (k : ℕ) (hMN' : N ≤ M + k) (h : M ≤ M + k), f (M, M + k).2 / f (M, M + k).1 ∈ (↑t : Set G)
⊢ f (M, M').2 / f (M, M').1 ∈ (↑t : Set G)

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h

Premises used: Nat.exists_eq_add_of_le, rfl
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
inst_3 : NonarchimedeanGroup G
f : ℕ → G
hf : Tendsto.{0, u_2} (β := G) (fun (n : ℕ) ↦ f (n + 1) / f n) atTop (𝓝 1)
s : Set G
hs : Membership.mem (γ := Filter G) (𝓝 1) s
t : OpenSubgroup G
ht : (↑t : Set G) ⊆ s
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → f (b + 1) / f b ∈ t
M : ℕ
hMN : N ≤ M
⊢ f (M, M + 0).2 / f (M, M + 0).1 ∈ (↑t : Set G)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
inst_3 : NonarchimedeanGroup G
f : ℕ → G
hf : Tendsto.{0, u_2} (β := G) (fun (n : ℕ) ↦ f (n + 1) / f n) atTop (𝓝 1)
s : Set G
hs : Membership.mem (γ := Filter G) (𝓝 1) s
t : OpenSubgroup G
ht : (↑t : Set G) ⊆ 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 : Set G)
⊢ N ≤ M + k

Tactic:
lia
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
inst_3 : NonarchimedeanGroup G
f : ℕ → G
hf : Tendsto.{0, u_2} (β := G) (fun (n : ℕ) ↦ f (n + 1) / f n) atTop (𝓝 1)
s : Set G
hs : Membership.mem (γ := Filter G) (𝓝 1) s
t : OpenSubgroup G
ht : (↑t : Set G) ⊆ 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 : Set G)
⊢ f (M, M + (k + 1)).2 / f (M, M + (k + 1)).1 ∈ (↑t : Set G)

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

Premises used: Subgroup.mul_mem, OpenSubgroup.toSubgroup
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
inst_3 : NonarchimedeanGroup G
f : ℕ → G
hf : Tendsto.{0, u_2} (β := G) (fun (n : ℕ) ↦ f (n + 1) / f n) atTop (𝓝 1)
s : Set G
hs : Membership.mem (γ := Filter G) (𝓝 1) s
t : OpenSubgroup G
ht : (↑t : Set G) ⊆ s
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → f (b + 1) / f b ∈ t
M : ℕ
hMN : N ≤ M
k : ℕ
zero : f (M, M + 0).2 / f (M, M + 0).1 ∈ (↑t : Set G)
succ :
  ∀ (k : ℕ) (ih : f (M, M + k).2 / f (M, M + k).1 ∈ (↑t : Set G)),
    f (M, M + (k + 1)).2 / f (M, M + (k + 1)).1 ∈ (↑t : Set G)
⊢ f (M, M + k).2 / f (M, M + k).1 ∈ (↑t : Set G)

Tactic:
induction k with
  | zero => simp
  | succ k ih => simpa using t.mul_mem (hN _ (by lia : N ≤ M + k)) ih
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
Goal:
α : Type u_1
G : Type u_2
inst : CommGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
inst_3 : NonarchimedeanGroup G
inst_4 : CompleteSpace G
f : α → G
hf : Tendsto f cofinite (𝓝 1)
⊢ Multipliable f

Tactic:
CompleteSpace.complete (cauchySeq_prod_of_tendsto_cofinite_one hf)

Premises used: HasProd, Multipliable, Filter.Tendsto, CompleteSpace.complete, NonarchimedeanGroup.cauchySeq_prod_of_tendsto_cofinite_one
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
Goal:
α : Type u_1
G : Type u_2
inst : CommGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
inst_3 : NonarchimedeanGroup G
inst_4 : CompleteSpace G
f : α → G
⊢ Multipliable f ↔ Tendsto f cofinite (𝓝 1)

Tactic:
⟨Multipliable.tendsto_cofinite_one, multipliable_of_tendsto_cofinite_one⟩

Premises used: NonarchimedeanGroup.multipliable_of_tendsto_cofinite_one, Multipliable.tendsto_cofinite_one, Iff.intro
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
Goal:
α : Type u_1
β : Type u_2
R : Type u_3
inst : Ring R
inst_1 : UniformSpace R
inst_2 : IsUniformAddGroup R
inst_3 : NonarchimedeanRing R
inst_4 : CompleteSpace R
f : α → R
g : β → R
hf : Summable f
hg : Summable g
rw :
  ∀ (hf : Tendsto f cofinite (𝓝 0)) (hg : Tendsto g cofinite (𝓝 0)),
    Tendsto (β := R) (fun (i : α × β) ↦ f i.1 * g i.2) cofinite (𝓝 0)
⊢ Summable (α := R) fun (i : α × β) ↦ f i.1 * g i.2

Tactic:
rw [NonarchimedeanAddGroup.summable_iff_tendsto_cofinite_zero] at *

Premises used: NonarchimedeanAddGroup.summable_iff_tendsto_cofinite_zero