awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
f : ℕ → G
⊢ (Multipliable.{u_2, 0} (α := G) fun (n : ℕ+) ↦ f (↑n : ℕ)) ↔ Multipliable f
have rw : (Multipliable.{u_2, 0} (α := G) fun (x : ℕ) ↦ f (x + 1)) ↔ Multipliable f
Tactic: rw [multipliable_pnat_iff_multipliable_succ, multipliable_nat_add_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
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
⊢ (Multipliable.{u_2, 0} (α := G) fun (n : ℕ+) ↦ f (↑n : ℕ)) ↔ Multipliable f
have rw₁ : Multipliable f ↔ Multipliable f
Tactic: rw [multipliable_pnat_iff_multipliable_succ, multipliable_nat_add_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (hypothesis)
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
⊢ ∏' (n : ℤ), f n = (f 0 * ∏' (n : ℕ+), f (↑(↑n : ℕ) : ℤ)) * ∏' (n : ℕ+), f (-(↑(↑n : ℕ) : ℤ))
have h1 : 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
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (hypothesis)
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 : ℤ)
⊢ ∏' (n : ℤ), f n = (f 0 * ∏' (n : ℕ+), f (↑(↑n : ℕ) : ℤ)) * ∏' (n : ℕ+), f (-(↑(↑n : ℕ) : ℤ))
have h2 : 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
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
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 : ℕ) : ℤ)
have rwa : Multipliable.{u_2, 0} (α := G) fun (x : ℕ) ↦ f (↑(x + 1) : ℤ)
Tactic: rwa [multipliable_pnat_iff_multipliable_succ (f := (f ·)),
      multipliable_nat_add_iff 1 (f := (f ·))]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (hypothesis)
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 : ℤ))
⊢ ∏' (n : ℤ), f n = (f 0 * ∏' (n : ℕ+), f (↑(↑n : ℕ) : ℤ)) * ∏' (n : ℕ+), f (-(↑(↑n : ℕ) : ℤ))
have h3 : 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 ·))]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
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 : ℕ) : ℤ))
have rwa : Multipliable.{u_2, 0} (α := G) fun (x : ℕ) ↦ f (-(↑(x + 1) : ℤ))
Tactic: rwa [multipliable_pnat_iff_multipliable_succ (f := (fun x ↦ f (-x))),
      multipliable_nat_add_iff 1 (f := (fun x ↦ f (-x)))]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (hypothesis)
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 : ℕ) : ℤ)
⊢ ∏' (n : ℤ), f n = (f 0 * ∏' (n : ℕ+), f (↑(↑n : ℕ) : ℤ)) * ∏' (n : ℕ+), f (-(↑(↑n : ℕ) : ℤ))
have h4 : 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)))]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (hypothesis)
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 0 * ∏' (n : ℕ+), f (↑(↑n : ℕ) : ℤ)) * ∏' (n : ℕ+), f (-(↑(↑n : ℕ) : ℤ))
have this : ∏' (n : ℕ), f (↑n : ℤ) * f (-(↑n : ℤ)) = (∏' (n : ℤ), f n) * f 0
Tactic: have := tprod_nat_mul_neg hf2
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (hypothesis)
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
⊢ ∏' (n : ℤ), f n = (f 0 * ∏' (n : ℕ+), f (↑(↑n : ℕ) : ℤ)) * ∏' (n : ℕ+), f (-(↑(↑n : ℕ) : ℤ))
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean (goal)
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)
⊢ CauchySeq.{u_2, u_1} (α := G) fun (s : Finset α) ↦ ∏ i ∈ s, f i
have apply : ∀ (e : Set G),
  Membership.mem (γ := Filter G) (𝓝 1) e → ∃ (s : Finset α), ∀ (t : Finset α), Disjoint t s → ∏ b ∈ t, f b ∈ e
Tactic: apply cauchySeq_finset_iff_prod_vanishing.mpr
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean (goal)
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
⊢ ∃ (s : Finset α), ∀ (t : Finset α), Disjoint t s → ∏ b ∈ t, f b ∈ U
have rcases : ∀ (V : OpenSubgroup G) (hV : (↑V : Set G) ⊆ U), ∃ (s : Finset α), ∀ (t : Finset α), Disjoint t s → ∏ b ∈ t, f b ∈ U
Tactic: rcases is_nonarchimedean U hU with ⟨V, hV⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean (goal)
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
⊢ ∃ (s : Finset α), ∀ (t : Finset α), Disjoint t s → ∏ b ∈ t, f b ∈ U
have h : ∀ (t : Finset α), Disjoint t (Set.Finite.toFinset (s := (f ⁻¹' (↑V : Set G))ᶜ) sorry) → ∏ b ∈ t, f b ∈ U
Tactic: use (tendsto_def.mp hf V V.mem_nhds_one).toFinset
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean (goal)
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))ᶜ) ⋯)
⊢ ∏ b ∈ t, f b ∈ U
have h : ∏ b ∈ t, f b ∈ (↑V : Set G)
Tactic: apply hV
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean (goal)
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))ᶜ) ⋯)
⊢ ∏ b ∈ t, f b ∈ (↑V : Set G)
have h : ∀ c ∈ t, f c ∈ (↑V : Subgroup G)
Tactic: apply Subgroup.prod_mem
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean (goal)
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)
⊢ CauchySeq f
have suffices : Tendsto.{0, u_2} (β := G) (fun (p : ℕ × ℕ) ↦ f p.2 / f p.1) atTop (𝓝 1)
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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean (goal)
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)
⊢ Tendsto.{0, u_2} (β := G) (fun (p : ℕ × ℕ) ↦ f p.2 / f p.1) atTop (𝓝 1)
have rw : ∀ (s : Set G), Membership.mem (γ := Filter G) (𝓝 1) s → ∃ (a : ℕ × ℕ), ∀ b ≥ a, f b.2 / f b.1 ∈ s
Tactic: rw [tendsto_atTop']
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean (goal)
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
⊢ ∃ (a : ℕ × ℕ), ∀ b ≥ a, f b.2 / f b.1 ∈ s
have obtain : ∀ (t : OpenSubgroup G) (ht : (↑t : Set G) ⊆ s), ∃ (a : ℕ × ℕ), ∀ b ≥ a, f b.2 / f b.1 ∈ s
Tactic: obtain ⟨t, ht⟩ := is_nonarchimedean s hs
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean (goal)
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
⊢ ∃ (a : ℕ × ℕ), ∀ b ≥ a, f b.2 / f b.1 ∈ s
have obtain : ∀ (N : ℕ) (hN : ∀ (b : ℕ), N ≤ b → f (b + 1) / f b ∈ t), ∃ (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
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean (goal)
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
have refine : ∀ b ≥ (N, N), f b.2 / f b.1 ∈ s
Tactic: refine ⟨(N, N), ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean (goal)
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'
⊢ f (M, M').2 / f (M, M').1 ∈ s
have a : f (M, M').2 / f (M, M').1 ∈ (↑t : Set G)
Tactic: apply ht
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean (goal)
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'
⊢ f (M, M').2 / f (M, M').1 ∈ (↑t : Set G)
have 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)
Tactic: wlog h : M ≤ M' generalizing M M'
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean (goal)
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)
⊢ f (M, M').2 / f (M, M').1 ∈ (↑t : Set G)
have wlog : ∀ (M M' : ℕ) (hMN : N ≤ M) (hMN' : N ≤ M') (h : M ≤ M'), f (M, M').2 / f (M, M').1 ∈ (↑t : Set G)
Tactic: wlog h : M ≤ M' generalizing M M'
Cleared hypotheses: M, M', hMN, hMN'
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean (goal)
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'
⊢ f (M, M').2 / f (M, M').1 ∈ (↑t : Set G)
have obtain : ∀ (k : ℕ) (hMN' : N ≤ M + k) (h : M ≤ M + k), f (M, M + k).2 / f (M, M + k).1 ∈ (↑t : Set G)
Tactic: obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h
Cleared hypotheses: M', hMN', h
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean (goal)
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 : ℕ
⊢ f (M, M + k).2 / f (M, M + k).1 ∈ (↑t : Set G)
have zero : f (M, M + 0).2 / f (M, M + 0).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
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean (goal)
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)
⊢ f (M, M + k).2 / f (M, M + k).1 ∈ (↑t : Set G)
have 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)
Tactic: induction k with
  | zero => simp
  | succ k ih => simpa using t.mul_mem (hN _ (by lia : N ≤ M + k)) ih
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean (goal)
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
⊢ Summable (α := R) fun (i : α × β) ↦ f i.1 * g i.2
have rw : ∀ (hf : Tendsto f cofinite (𝓝 0)) (hg : Tendsto g cofinite (𝓝 0)),
  Tendsto (β := R) (fun (i : α × β) ↦ f i.1 * g i.2) cofinite (𝓝 0)
Tactic: rw [NonarchimedeanAddGroup.summable_iff_tendsto_cofinite_zero] at *
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean (goal)
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
f : α → R
g : β → R
a b : R
hf : HasSum f a
hg : HasSum g b
⊢ HasSum (fun (i : α × β) ↦ f i.1 * g i.2) (a * b)
have rw : ∀
  (hf :
    HasSum (α := UniformSpace.Completion R)
      ((⇑UniformSpace.Completion.toCompl : (a : R) → UniformSpace.Completion R) ∘ f) (↑a : UniformSpace.Completion R))
  (hg :
    HasSum (α := UniformSpace.Completion R)
      ((⇑UniformSpace.Completion.toCompl : (a : R) → UniformSpace.Completion R) ∘ g) (↑b : UniformSpace.Completion R)),
  HasSum (α := UniformSpace.Completion R) (β := α × β)
    (Function.comp (β := R) (⇑UniformSpace.Completion.toCompl : (a : R) → UniformSpace.Completion R) fun (i : α × β) ↦
      f i.1 * g i.2)
    (↑(a * b) : UniformSpace.Completion R)
Tactic: rw [← hasSum_iff_hasSum_compl] at *
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean (goal)
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
f : α → R
g : β → R
a b : R
hf :
  HasSum (α := UniformSpace.Completion R) ((⇑UniformSpace.Completion.toCompl : (a : R) → UniformSpace.Completion R) ∘ f)
    (↑a : UniformSpace.Completion R)
hg :
  HasSum (α := UniformSpace.Completion R) ((⇑UniformSpace.Completion.toCompl : (a : R) → UniformSpace.Completion R) ∘ g)
    (↑b : UniformSpace.Completion R)
⊢ HasSum (α := UniformSpace.Completion R) (β := α × β)
    (Function.comp (β := R) (⇑UniformSpace.Completion.toCompl : (a : R) → UniformSpace.Completion R) fun (i : α × β) ↦
      f i.1 * g i.2)
    (↑(a * b) : UniformSpace.Completion R)
have simp : HasSum
  (fun (x : α × β) ↦
    HMul.hMul (α := UniformSpace.Completion R) (↑(f x.1) : UniformSpace.Completion R)
      (↑(g x.2) : UniformSpace.Completion R))
  (HMul.hMul (α := UniformSpace.Completion R) (↑a : UniformSpace.Completion R) (↑b : UniformSpace.Completion R))
Tactic: simp only [Function.comp_def, UniformSpace.Completion.toCompl_apply,
    UniformSpace.Completion.coe_mul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (hypothesis)
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd f a₁
hg : HasProd g a₂
⊢ a₁ ≤ a₂
have hf₁ : HasProd (extend e f 1) a₁
Tactic: rw [← hasProd_extend_one he] at hf
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (goal)
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd (extend e f 1) a₁
hg : HasProd g a₂
⊢ a₁ ≤ a₂
have refine : ∀ (c : κ), extend e f 1 c ≤ g c
Tactic: refine hasProd_le (fun c ↦ ?_) hf hg
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (goal)
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd (extend e f 1) a₁
hg : HasProd g a₂
c : κ
⊢ extend e f 1 c ≤ g c
have inl : ∀ (i : ι), extend e f 1 (e i) ≤ g (e i)
Tactic: obtain ⟨i, rfl⟩ | h := em (c ∈ Set.range e)
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (goal)
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd (extend e f 1) a₁
hg : HasProd g a₂
c : κ
inl : ∀ (i : ι), extend e f 1 (e i) ≤ g (e i)
⊢ extend e f 1 c ≤ g c
have inr : ∀ (h : c ∉ Set.range e), extend e f 1 c ≤ g c
Tactic: obtain ⟨i, rfl⟩ | h := em (c ∈ Set.range e)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (goal)
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd (extend e f 1) a₁
hg : HasProd g a₂
i : ι
⊢ extend e f 1 (e i) ≤ g (e i)
have inl : f i ≤ g (e i)
Tactic: rw [he.extend_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (goal)
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h_1 : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd (extend e f 1) a₁
hg : HasProd g a₂
c : κ
h : c ∉ Set.range e
⊢ extend e f 1 c ≤ g c
have inr : 1 c ≤ g c
Tactic: rw [extend_apply' _ _ _ h]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
a : α
inst_5 : L.NeBot
inst_6 : L.LeAtTop
s : Finset ι
hs : ∀ i ∉ s, 1 ≤ f i
hf : HasProd f a L
⊢ ∏ i ∈ s, f i ≤ a
have refine : ∃ (a : Finset ι), ∀ b ≥ a, LE.le.{u_3} (α := α) (∏ i ∈ s, f i) (∏ b ∈ b, f b)
Tactic: refine ge_of_tendsto hf <| .filter_mono L.le_atTop <| eventually_atTop.2 ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
a : α
inst_5 : L.NeBot
inst_6 : L.LeAtTop
hf : HasProd f a L
i : ι
hb : ∀ (j : ι), j ≠ i → 1 ≤ f j
⊢ f i = ∏ i ∈ {i}, f i
have rw : f i = f i
Tactic: rw [prod_singleton]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
a : α
inst_5 : L.NeBot
inst_6 : L.LeAtTop
inst_7 : MulRightStrictMono α
hf : HasProd f a L
i : ι
hi : ∀ (j : ι), j ≠ i → 1 ≤ f j
j : ι
hij : j ≠ i
hj : 1 < f j
⊢ f j * f i = ∏ k ∈ {j, i}, f k
have rw : f j * f i = f j * f i
Tactic: rw [Finset.prod_pair hij]