awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (hypothesis)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
α : Type u_3
β : Type u_4
inst_2 : Encodable β
inst_3 : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
s : β → α
n : ℕ
hn : n ∉ Set.range.{0, u_4 + 1} (ι := β) encode
⊢ m (⨆ b ∈ decode₂ β n, s b) = 1 n
have hn₁ : decode₂ β n = none
Tactic: rw [← decode₂_ne_none_iff, ne_eq, not_not] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
α : Type u_3
β : Type u_4
inst_2 : Countable β
inst_3 : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
R : M → M → Prop
m_iSup : ∀ (s : ℕ → α), R (m (⨆ (i : ℕ), s i)) (∏' (i : ℕ), m (s i))
s : β → α
⊢ R (m (⨆ (b : β), s b)) (∏' (b : β), m (s b))
have intro : ∀ (val : Encodable β), R (m (⨆ (b : β), s b)) (∏' (b : β), m (s b))
Tactic: cases nonempty_encodable β
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
α : Type u_3
β : Type u_4
inst_2 : Countable β
inst_3 : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
R : M → M → Prop
m_iSup : ∀ (s : ℕ → α), R (m (⨆ (i : ℕ), s i)) (∏' (i : ℕ), m (s i))
s : β → α
val : Encodable β
⊢ R (m (⨆ (b : β), s b)) (∏' (b : β), m (s b))
have intro : R (m (⨆ (i : ℕ), ⨆ b ∈ decode₂ β i, s b)) (∏' (i : ℕ), m (⨆ b ∈ decode₂ β i, s b))
Tactic: rw [← iSup_decode₂, ← tprod_iSup_decode₂ _ m0 s]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
α : Type u_3
γ : Type u_5
inst_2 : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
R : M → M → Prop
m_iSup : ∀ (s : ℕ → α), R (m (⨆ (i : ℕ), s i)) (∏' (i : ℕ), m (s i))
s : γ → α
t : Finset γ
⊢ R (m (⨆ d ∈ t, s d)) (∏ d ∈ t, m (s d))
have rw : R (m (⨆ (x : Subtype (Membership.mem t)), s (↑x : γ))) (∏' (x : ↥t), m (s (↑x : γ)))
Tactic: rw [iSup_subtype', ← Finset.tprod_subtype]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
α : Type u_3
inst_2 : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
R : M → M → Prop
m_iSup : ∀ (s : ℕ → α), R (m (⨆ (i : ℕ), s i)) (∏' (i : ℕ), m (s i))
s₁ s₂ : α
⊢ R (m (s₁ ⊔ s₂)) (m s₁ * m s₂)
have h : s₁ ⊔ s₂ = ⨆ (b : Bool), bif b then s₁ else s₂
Tactic: convert! rel_iSup_tprod m m0 R m_iSup fun b ↦ cond b s₁ s₂
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
α : Type u_3
inst_2 : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
R : M → M → Prop
m_iSup : ∀ (s : ℕ → α), R (m (⨆ (i : ℕ), s i)) (∏' (i : ℕ), m (s i))
s₁ s₂ : α
h : s₁ ⊔ s₂ = ⨆ (b : Bool), bif b then s₁ else s₂
⊢ R (m (s₁ ⊔ s₂)) (m s₁ * m s₂)
have h₁ : m s₁ * m s₂ = ∏' (b : Bool), m (bif b then s₁ else s₂)
Tactic: convert! rel_iSup_tprod m m0 R m_iSup fun b ↦ cond b s₁ s₂
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
α : Type u_3
inst_2 : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
R : M → M → Prop
m_iSup : ∀ (s : ℕ → α), R (m (⨆ (i : ℕ), s i)) (∏' (i : ℕ), m (s i))
s₁ s₂ : α
⊢ m s₁ * m s₂ = ∏' (b : Bool), m (bif b then s₁ else s₂)
have h : m s₁ * m s₂ = ∏ b : Bool, m (bif b then s₁ else s₂)
Tactic: rw [tprod_fintype, Fintype.prod_bool, cond, cond]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
α : Type u_3
inst_2 : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
R : M → M → Prop
m_iSup : ∀ (s : ℕ → α), R (m (⨆ (i : ℕ), s i)) (∏' (i : ℕ), m (s i))
s₁ s₂ : α
h : m s₁ * m s₂ = ∏ b : Bool, m (bif b then s₁ else s₂)
⊢ m s₁ * m s₂ = ∏' (b : Bool), m (bif b then s₁ else s₂)
have h₁ : m s₁ * m s₂ = m (bif true then s₁ else s₂) * m (bif false then s₁ else s₂)
Tactic: rw [tprod_fintype, Fintype.prod_bool, cond, cond]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
α : Type u_3
inst_2 : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
R : M → M → Prop
m_iSup : ∀ (s : ℕ → α), R (m (⨆ (i : ℕ), s i)) (∏' (i : ℕ), m (s i))
s₁ s₂ : α
h : m s₁ * m s₂ = ∏ b : Bool, m (bif b then s₁ else s₂)
h₁ : m s₁ * m s₂ = m (bif true then s₁ else s₂) * m (bif false then s₁ else s₂)
⊢ m s₁ * m s₂ = ∏' (b : Bool), m (bif b then s₁ else s₂)
have h₂ : m s₁ * m s₂ = m s₁ * m (bif false then s₁ else s₂)
Tactic: rw [tprod_fintype, Fintype.prod_bool, cond, cond]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
α : Type u_3
inst_2 : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
R : M → M → Prop
m_iSup : ∀ (s : ℕ → α), R (m (⨆ (i : ℕ), s i)) (∏' (i : ℕ), m (s i))
s₁ s₂ : α
h : m s₁ * m s₂ = ∏ b : Bool, m (bif b then s₁ else s₂)
h₁ : m s₁ * m s₂ = m (bif true then s₁ else s₂) * m (bif false then s₁ else s₂)
h₂ : m s₁ * m s₂ = m s₁ * m (bif false then s₁ else s₂)
⊢ m s₁ * m s₂ = ∏' (b : Bool), m (bif b then s₁ else s₂)
have h₃ : m s₁ * m s₂ = m s₁ * m s₂
Tactic: rw [tprod_fintype, Fintype.prod_bool, cond, cond]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
G : Type u_2
inst : CommGroup G
g : G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
f : ℕ → G
k : ℕ
⊢ HasProd (fun (n : ℕ) ↦ f (n + k)) g ↔ HasProd f (g * ∏ i ∈ range k, f i)
have refine : HasProd (fun (n : ℕ) ↦ f (n + k)) g ↔ HasProd (fun (x : { x : ℕ // x ∉ range k }) ↦ f (↑x : ℕ)) g
Tactic: refine Iff.trans ?_ (range k).hasProd_compl_iff
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
G : Type u_2
inst : CommGroup G
g : G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
f : ℕ → G
k : ℕ
⊢ HasProd (fun (n : ℕ) ↦ f (n + k)) g ↔ HasProd (fun (x : { x : ℕ // x ∉ range k }) ↦ f (↑x : ℕ)) g
have rw : HasProd (fun (n : ℕ) ↦ f (n + k)) g ↔
  HasProd
    ((fun (x : { x : ℕ // x ∉ range k }) ↦ f (↑x : ℕ)) ∘
      (⇑(notMemRangeEquiv k).symm : (a : ℕ) → { n : ℕ // n ∉ range k }))
    g
Tactic: rw [← (notMemRangeEquiv k).symm.hasProd_iff, Function.comp_def, coe_notMemRangeEquiv_symm]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
G : Type u_2
inst : CommGroup G
g : G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
f : ℕ → G
k : ℕ
rw :
  HasProd (fun (n : ℕ) ↦ f (n + k)) g ↔
    HasProd
      ((fun (x : { x : ℕ // x ∉ range k }) ↦ f (↑x : ℕ)) ∘
        (⇑(notMemRangeEquiv k).symm : (a : ℕ) → { n : ℕ // n ∉ range k }))
      g
⊢ HasProd (fun (n : ℕ) ↦ f (n + k)) g ↔ HasProd (fun (x : { x : ℕ // x ∉ range k }) ↦ f (↑x : ℕ)) g
have rw₁ : HasProd (fun (n : ℕ) ↦ f (n + k)) g ↔
  HasProd (fun (x : ℕ) ↦ f (↑(((notMemRangeEquiv k).symm : (a : ℕ) → { n : ℕ // n ∉ range k }) x) : ℕ)) g
Tactic: rw [← (notMemRangeEquiv k).symm.hasProd_iff, Function.comp_def, coe_notMemRangeEquiv_symm]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
G : Type u_2
inst : CommGroup G
g : G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
f : ℕ → G
k : ℕ
rw :
  HasProd (fun (n : ℕ) ↦ f (n + k)) g ↔
    HasProd
      ((fun (x : { x : ℕ // x ∉ range k }) ↦ f (↑x : ℕ)) ∘
        (⇑(notMemRangeEquiv k).symm : (a : ℕ) → { n : ℕ // n ∉ range k }))
      g
rw₁ :
  HasProd (fun (n : ℕ) ↦ f (n + k)) g ↔
    HasProd (fun (x : ℕ) ↦ f (↑(((notMemRangeEquiv k).symm : (a : ℕ) → { n : ℕ // n ∉ range k }) x) : ℕ)) g
⊢ HasProd (fun (n : ℕ) ↦ f (n + k)) g ↔ HasProd (fun (x : { x : ℕ // x ∉ range k }) ↦ f (↑x : ℕ)) g
have rw₂ : HasProd (fun (n : ℕ) ↦ f (n + k)) g ↔
  HasProd
    (fun (x : ℕ) ↦
      f (↑((fun (j : ℕ) ↦ (Subtype.mk (p := fun (n : ℕ) ↦ n ∉ range k) (j + k) sorry : { n : ℕ // n ∉ range k })) x) : ℕ))
    g
Tactic: rw [← (notMemRangeEquiv k).symm.hasProd_iff, Function.comp_def, coe_notMemRangeEquiv_symm]
-- 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
inst_3 : T2Space G
f : ℕ → G
⊢ Tendsto.{0, u_2} (β := G) (fun (i : ℕ) ↦ ∏' (k : ℕ), f (k + i)) atTop (𝓝 1)
have pos : ∀ (hf : Multipliable f), Tendsto.{0, u_2} (β := G) (fun (i : ℕ) ↦ ∏' (k : ℕ), f (k + i)) atTop (𝓝 1)
Tactic: by_cases hf : Multipliable f
-- 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
inst_3 : T2Space G
f : ℕ → G
pos : ∀ (hf : Multipliable f), Tendsto.{0, u_2} (β := G) (fun (i : ℕ) ↦ ∏' (k : ℕ), f (k + i)) atTop (𝓝 1)
⊢ Tendsto.{0, u_2} (β := G) (fun (i : ℕ) ↦ ∏' (k : ℕ), f (k + i)) atTop (𝓝 1)
have neg : ∀ (hf : ¬Multipliable f), Tendsto.{0, u_2} (β := G) (fun (i : ℕ) ↦ ∏' (k : ℕ), f (k + i)) atTop (𝓝 1)
Tactic: by_cases hf : Multipliable f
-- 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
inst_3 : T2Space G
f : ℕ → G
hf : Multipliable f
⊢ Eq.{u_2 + 1} (α := (i : ℕ) → G) (fun (i : ℕ) ↦ HDiv.hDiv (α := G) (∏' (i : ℕ), f i) (∏ j ∈ range i, f j))
    fun (i : ℕ) ↦ ∏' (k : ℕ), f (k + i)
have h : ∀ (i : ℕ), HDiv.hDiv (α := G) (∏' (i : ℕ), f i) (∏ j ∈ range i, f j) = ∏' (k : ℕ), f (k + i)
Tactic: ext1 i
-- 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
inst_3 : T2Space G
f : ℕ → G
hf : Multipliable f
i : ℕ
⊢ HDiv.hDiv (α := G) (∏' (i : ℕ), f i) (∏ j ∈ range i, f j) = ∏' (k : ℕ), f (k + i)
have h : ∏' (i : ℕ), f i = HMul.hMul (α := G) (∏' (k : ℕ), f (k + i)) (∏ j ∈ range i, f j)
Tactic: rw [div_eq_iff_eq_mul, mul_comm, hf.prod_mul_tprod_nat_add i]
-- 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
inst_3 : T2Space G
f : ℕ → G
hf : Multipliable f
i : ℕ
h : ∏' (i : ℕ), f i = HMul.hMul (α := G) (∏' (k : ℕ), f (k + i)) (∏ j ∈ range i, f j)
⊢ HDiv.hDiv (α := G) (∏' (i : ℕ), f i) (∏ j ∈ range i, f j) = ∏' (k : ℕ), f (k + i)
have h₁ : ∏' (i : ℕ), f i = HMul.hMul (α := G) (∏ j ∈ range i, f j) (∏' (k : ℕ), f (k + i))
Tactic: rw [div_eq_iff_eq_mul, mul_comm, hf.prod_mul_tprod_nat_add i]
-- 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
inst_3 : T2Space G
f : ℕ → G
hf : Multipliable f
i : ℕ
h : ∏' (i : ℕ), f i = HMul.hMul (α := G) (∏' (k : ℕ), f (k + i)) (∏ j ∈ range i, f j)
h₁ : ∏' (i : ℕ), f i = HMul.hMul (α := G) (∏ j ∈ range i, f j) (∏' (k : ℕ), f (k + i))
⊢ HDiv.hDiv (α := G) (∏' (i : ℕ), f i) (∏ j ∈ range i, f j) = ∏' (k : ℕ), f (k + i)
have h₂ : Eq.{u_2 + 1} (α := G) (∏' (i : ℕ), f i) (∏' (i : ℕ), f i)
Tactic: rw [div_eq_iff_eq_mul, mul_comm, hf.prod_mul_tprod_nat_add i]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (hypothesis)
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
⊢ Tendsto.{0, u_2} (β := G) (fun (i : ℕ) ↦ ∏' (k : ℕ), f (k + i)) atTop (𝓝 1)
have h₀ : Eq.{u_2 + 1} (α := (i : ℕ) → G) (fun (i : ℕ) ↦ HDiv.hDiv (α := G) (∏' (i : ℕ), f i) (∏ j ∈ range i, f j)) fun (i : ℕ) ↦
  ∏' (k : ℕ), f (k + i)
Tactic: have h₀ : (fun i ↦ (∏' i, f i) / ∏ j ∈ range i, f j) = fun i ↦ ∏' k : ℕ, f (k + i) := by
      ext1 i
      rw [div_eq_iff_eq_mul, mul_comm, hf.prod_mul_tprod_nat_add i]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (hypothesis)
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
h₀ :
  Eq.{u_2 + 1} (α := (i : ℕ) → G) (fun (i : ℕ) ↦ HDiv.hDiv (α := G) (∏' (i : ℕ), f i) (∏ j ∈ range i, f j))
    fun (i : ℕ) ↦ ∏' (k : ℕ), f (k + i)
⊢ Tendsto.{0, u_2} (β := G) (fun (i : ℕ) ↦ ∏' (k : ℕ), f (k + i)) atTop (𝓝 1)
have h₁ : Tendsto.{0, u_2} (β := G) (fun (x : ℕ) ↦ ∏' (i : ℕ), f i) atTop (𝓝 (∏' (i : ℕ), f i))
Tactic: have h₁ : Tendsto (fun _ : ℕ ↦ ∏' i, f i) atTop (𝓝 (∏' i, f i)) := tendsto_const_nhds
-- 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
inst_3 : T2Space G
f : ℕ → G
hf : ¬Multipliable f
⊢ Tendsto.{0, u_2} (β := G) (fun (i : ℕ) ↦ ∏' (k : ℕ), f (k + i)) atTop (𝓝 1)
have neg : ∀ (n : ℕ), ¬Multipliable.{u_2, 0} (α := G) fun (k : ℕ) ↦ f (k + n)
Tactic: refine tendsto_const_nhds.congr fun n ↦ (tprod_eq_one_of_not_multipliable ?_).symm
-- 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
f : ℕ → G
⊢ (CauchySeq.{u_2, 0} (α := G) fun (s : Finset ℕ) ↦ ∏ n ∈ s, f n) ↔
    ∀ (e : Set G),
      Membership.mem (γ := Filter G) (𝓝 1) e → ∃ (N : ℕ), ∀ t ⊆ {n : ℕ | N ≤ n}, ∏' (n : (↑t : Type)), f (↑n : ℕ) ∈ e
have refine_1 : ∀
  (vanish :
    ∀ (e : Set G),
      Membership.mem (γ := Filter G) (𝓝 1) e →
        ∃ (s : Finset ℕ), ∀ (t : Set ℕ), Disjoint t (↑s : Set ℕ) → ∏' (b : (↑t : Type)), f (↑b : ℕ) ∈ e)
  (e : Set G) (he : Membership.mem (γ := Filter G) (𝓝 1) e),
  ∃ (N : ℕ), ∀ t ⊆ {n : ℕ | N ≤ n}, ∏' (n : (↑t : Type)), f (↑n : ℕ) ∈ e
Tactic: refine cauchySeq_finset_iff_tprod_vanishing.trans ⟨fun vanish e he ↦ ?_, fun vanish e he ↦ ?_⟩
-- 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
f : ℕ → G
refine_1 :
  ∀
    (vanish :
      ∀ (e : Set G),
        Membership.mem (γ := Filter G) (𝓝 1) e →
          ∃ (s : Finset ℕ), ∀ (t : Set ℕ), Disjoint t (↑s : Set ℕ) → ∏' (b : (↑t : Type)), f (↑b : ℕ) ∈ e)
    (e : Set G) (he : Membership.mem (γ := Filter G) (𝓝 1) e),
    ∃ (N : ℕ), ∀ t ⊆ {n : ℕ | N ≤ n}, ∏' (n : (↑t : Type)), f (↑n : ℕ) ∈ e
⊢ (CauchySeq.{u_2, 0} (α := G) fun (s : Finset ℕ) ↦ ∏ n ∈ s, f n) ↔
    ∀ (e : Set G),
      Membership.mem (γ := Filter G) (𝓝 1) e → ∃ (N : ℕ), ∀ t ⊆ {n : ℕ | N ≤ n}, ∏' (n : (↑t : Type)), f (↑n : ℕ) ∈ e
have refine_2 : ∀
  (vanish :
    ∀ (e : Set G),
      Membership.mem (γ := Filter G) (𝓝 1) e → ∃ (N : ℕ), ∀ t ⊆ {n : ℕ | N ≤ n}, ∏' (n : (↑t : Type)), f (↑n : ℕ) ∈ e)
  (e : Set G) (he : Membership.mem (γ := Filter G) (𝓝 1) e),
  ∃ (s : Finset ℕ), ∀ (t : Set ℕ), Disjoint t (↑s : Set ℕ) → ∏' (b : (↑t : Type)), f (↑b : ℕ) ∈ e
Tactic: refine cauchySeq_finset_iff_tprod_vanishing.trans ⟨fun vanish e he ↦ ?_, fun vanish e he ↦ ?_⟩
-- 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
f : ℕ → G
vanish :
  ∀ (e : Set G),
    Membership.mem (γ := Filter G) (𝓝 1) e →
      ∃ (s : Finset ℕ), ∀ (t : Set ℕ), Disjoint t (↑s : Set ℕ) → ∏' (b : (↑t : Type)), f (↑b : ℕ) ∈ e
e : Set G
he : Membership.mem (γ := Filter G) (𝓝 1) e
⊢ ∃ (N : ℕ), ∀ t ⊆ {n : ℕ | N ≤ n}, ∏' (n : (↑t : Type)), f (↑n : ℕ) ∈ e
have refine_1 : ∀ (s : Finset ℕ) (hs : ∀ (t : Set ℕ), Disjoint t (↑s : Set ℕ) → ∏' (b : (↑t : Type)), f (↑b : ℕ) ∈ e),
  ∃ (N : ℕ), ∀ t ⊆ {n : ℕ | N ≤ n}, ∏' (n : (↑t : Type)), f (↑n : ℕ) ∈ e
Tactic: obtain ⟨s, hs⟩ := vanish e he
-- 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
f : ℕ → G
vanish :
  ∀ (e : Set G),
    Membership.mem (γ := Filter G) (𝓝 1) e →
      ∃ (s : Finset ℕ), ∀ (t : Set ℕ), Disjoint t (↑s : Set ℕ) → ∏' (b : (↑t : Type)), f (↑b : ℕ) ∈ e
e : Set G
he : Membership.mem (γ := Filter G) (𝓝 1) e
s : Finset ℕ
hs : ∀ (t : Set ℕ), Disjoint t (↑s : Set ℕ) → ∏' (b : (↑t : Type)), f (↑b : ℕ) ∈ e
⊢ ∃ (N : ℕ), ∀ t ⊆ {n : ℕ | N ≤ n}, ∏' (n : (↑t : Type)), f (↑n : ℕ) ∈ e
have refine_1 : ∀ (t : Set ℕ) (ht : t ⊆ {n : ℕ | (if h : s.Nonempty then s.max' h + 1 else 0) ≤ n}) ⦃a : ℕ⦄, a ∈ t → a ∉ (↑s : Set ℕ)
Tactic: refine ⟨if h : s.Nonempty then s.max' h + 1 else 0,
      fun t ht ↦ hs _ <| Set.disjoint_left.mpr ?_⟩
-- 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
f : ℕ → G
vanish :
  ∀ (e : Set G),
    Membership.mem (γ := Filter G) (𝓝 1) e →
      ∃ (s : Finset ℕ), ∀ (t : Set ℕ), Disjoint t (↑s : Set ℕ) → ∏' (b : (↑t : Type)), f (↑b : ℕ) ∈ e
e : Set G
he : Membership.mem (γ := Filter G) (𝓝 1) e
s : Finset ℕ
hs : ∀ (t : Set ℕ), Disjoint t (↑s : Set ℕ) → ∏' (b : (↑t : Type)), f (↑b : ℕ) ∈ e
t : Set ℕ
ht : t ⊆ {n : ℕ | (if h : s.Nonempty then s.max' h + 1 else 0) ≤ n}
⊢ ∀ ⦃a : ℕ⦄, a ∈ t → a ∉ (↑s : Set ℕ)
have pos : ∀ (h : s.Nonempty) (ht : t ⊆ {n : ℕ | s.max' h + 1 ≤ n}) ⦃a : ℕ⦄, a ∈ t → a ∉ (↑s : Set ℕ)
Tactic: split_ifs at ht with h
Cleared hypotheses: ht
-- 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
f : ℕ → G
vanish :
  ∀ (e : Set G),
    Membership.mem (γ := Filter G) (𝓝 1) e →
      ∃ (s : Finset ℕ), ∀ (t : Set ℕ), Disjoint t (↑s : Set ℕ) → ∏' (b : (↑t : Type)), f (↑b : ℕ) ∈ e
e : Set G
he : Membership.mem (γ := Filter G) (𝓝 1) e
s : Finset ℕ
hs : ∀ (t : Set ℕ), Disjoint t (↑s : Set ℕ) → ∏' (b : (↑t : Type)), f (↑b : ℕ) ∈ e
t : Set ℕ
ht : t ⊆ {n : ℕ | (if h : s.Nonempty then s.max' h + 1 else 0) ≤ n}
pos : ∀ (h : s.Nonempty) (ht : t ⊆ {n : ℕ | s.max' h + 1 ≤ n}) ⦃a : ℕ⦄, a ∈ t → a ∉ (↑s : Set ℕ)
⊢ ∀ ⦃a : ℕ⦄, a ∈ t → a ∉ (↑s : Set ℕ)
have neg : ∀ (h : ¬s.Nonempty) (ht : t ⊆ {n : ℕ | 0 ≤ n}) ⦃a : ℕ⦄, a ∈ t → a ∉ (↑s : Set ℕ)
Tactic: split_ifs at ht with h
Cleared hypotheses: ht
-- 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
f : ℕ → G
vanish :
  ∀ (e : Set G),
    Membership.mem (γ := Filter G) (𝓝 1) e → ∃ (N : ℕ), ∀ t ⊆ {n : ℕ | N ≤ n}, ∏' (n : (↑t : Type)), f (↑n : ℕ) ∈ e
e : Set G
he : Membership.mem (γ := Filter G) (𝓝 1) e
⊢ ∃ (s : Finset ℕ), ∀ (t : Set ℕ), Disjoint t (↑s : Set ℕ) → ∏' (b : (↑t : Type)), f (↑b : ℕ) ∈ e
have refine_2 : ∀ (N : ℕ) (hN : ∀ t ⊆ {n : ℕ | N ≤ n}, ∏' (n : (↑t : Type)), f (↑n : ℕ) ∈ e),
  ∃ (s : Finset ℕ), ∀ (t : Set ℕ), Disjoint t (↑s : Set ℕ) → ∏' (b : (↑t : Type)), f (↑b : ℕ) ∈ e
Tactic: obtain ⟨N, hN⟩ := vanish e he
-- 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
f : ℕ → G
⊢ Multipliable f ↔
    ∀ (e : Set G),
      Membership.mem (γ := Filter G) (𝓝 1) e → ∃ (N : ℕ), ∀ t ⊆ {n : ℕ | N ≤ n}, ∏' (n : (↑t : Type)), f (↑n : ℕ) ∈ e
have rw : (CauchySeq.{u_2, 0} (α := G) fun (s : Finset ℕ) ↦ ∏ b ∈ s, f b) ↔
  ∀ (e : Set G),
    Membership.mem (γ := Filter G) (𝓝 1) e → ∃ (N : ℕ), ∀ t ⊆ {n : ℕ | N ≤ n}, ∏' (n : (↑t : Type)), f (↑n : ℕ) ∈ e
Tactic: rw [multipliable_iff_cauchySeq_finset, cauchySeq_finset_iff_nat_tprod_vanishing]
-- 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
f : ℕ → G
rw :
  (CauchySeq.{u_2, 0} (α := G) fun (s : Finset ℕ) ↦ ∏ b ∈ s, f b) ↔
    ∀ (e : Set G),
      Membership.mem (γ := Filter G) (𝓝 1) e → ∃ (N : ℕ), ∀ t ⊆ {n : ℕ | N ≤ n}, ∏' (n : (↑t : Type)), f (↑n : ℕ) ∈ e
⊢ Multipliable f ↔
    ∀ (e : Set G),
      Membership.mem (γ := Filter G) (𝓝 1) e → ∃ (N : ℕ), ∀ t ⊆ {n : ℕ | N ≤ n}, ∏' (n : (↑t : Type)), f (↑n : ℕ) ∈ e
have rw₁ : (∀ (e : Set G),
    Membership.mem (γ := Filter G) (𝓝 1) e → ∃ (N : ℕ), ∀ t ⊆ {n : ℕ | N ≤ n}, ∏' (n : (↑t : Type)), f (↑n : ℕ) ∈ e) ↔
  ∀ (e : Set G),
    Membership.mem (γ := Filter G) (𝓝 1) e → ∃ (N : ℕ), ∀ t ⊆ {n : ℕ | N ≤ n}, ∏' (n : (↑t : Type)), f (↑n : ℕ) ∈ e
Tactic: rw [multipliable_iff_cauchySeq_finset, cauchySeq_finset_iff_nat_tprod_vanishing]
-- 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
hf : Multipliable f
⊢ Tendsto f atTop (𝓝 1)
have rw : Tendsto f cofinite (𝓝 1)
Tactic: rw [← Nat.cofinite_eq_atTop]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
f : ℤ → M
hf : HasProd f m
⊢ HasProd (fun (n : ℕ) ↦ f (↑n : ℤ) * f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) m
have change : HasProd (fun (n : ℕ) ↦ f (↑n : ℤ) * f (Int.negSucc n)) m
Tactic: change HasProd (fun n : ℕ ↦ f n * f (Int.negSucc n)) m
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (hypothesis)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
f : ℤ → M
hf : HasProd f m
⊢ HasProd (fun (n : ℕ) ↦ f (↑n : ℤ) * f (Int.negSucc n)) m
have this : Injective Int.negSucc
Tactic: have : Injective Int.negSucc := @Int.negSucc.inj
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
f : ℤ → M
hf : HasProd f m
this : Injective Int.negSucc
⊢ HasProd (fun (n : ℕ) ↦ f (↑n : ℤ) * f (Int.negSucc n)) m
have refine : ∀ (u : Finset ℤ),
  ∃ (v : Finset ℕ),
    ∀ (v' : Finset ℕ),
      v ⊆ v' →
        ∃ (u' : Finset ℤ), u ⊆ u' ∧ Eq.{u_1 + 1} (α := M) (∏ x ∈ u', f x) (∏ b ∈ v', f (↑b : ℤ) * f (Int.negSucc b))
Tactic: refine hf.hasProd_of_prod_eq fun u ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
f : ℤ → M
hf : HasProd f m
this : Injective Int.negSucc
u : Finset ℤ
⊢ ∃ (v : Finset ℕ),
    ∀ (v' : Finset ℕ),
      v ⊆ v' →
        ∃ (u' : Finset ℤ), u ⊆ u' ∧ Eq.{u_1 + 1} (α := M) (∏ x ∈ u', f x) (∏ b ∈ v', f (↑b : ℤ) * f (Int.negSucc b))
have refine_1 : ∀ (v' : Finset ℕ) (hv' : u.preimage Nat.cast sorry ∪ u.preimage Int.negSucc sorry ⊆ v') (x : ℤ) (hx : x ∈ u),
  x ∈ image Nat.cast v' ∪ image Int.negSucc v'
Tactic: refine ⟨u.preimage _ Nat.cast_injective.injOn ∪ u.preimage _ this.injOn,
      fun v' hv' ↦ ⟨v'.image Nat.cast ∪ v'.image Int.negSucc, fun x hx ↦ ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
f : ℤ → M
hf : HasProd f m
this : Injective Int.negSucc
u : Finset ℤ
refine_1 :
  ∀ (v' : Finset ℕ) (hv' : u.preimage Nat.cast ⋯ ∪ u.preimage Int.negSucc ⋯ ⊆ v') (x : ℤ) (hx : x ∈ u),
    x ∈ image Nat.cast v' ∪ image Int.negSucc v'
⊢ ∃ (v : Finset ℕ),
    ∀ (v' : Finset ℕ),
      v ⊆ v' →
        ∃ (u' : Finset ℤ), u ⊆ u' ∧ Eq.{u_1 + 1} (α := M) (∏ x ∈ u', f x) (∏ b ∈ v', f (↑b : ℤ) * f (Int.negSucc b))
have refine_2 : ∀ (v' : Finset ℕ) (hv' : u.preimage Nat.cast sorry ∪ u.preimage Int.negSucc sorry ⊆ v'),
  Eq.{u_1 + 1} (α := M) (∏ x ∈ image Nat.cast v' ∪ image Int.negSucc v', f x) (∏ b ∈ v', f (↑b : ℤ) * f (Int.negSucc b))
Tactic: refine ⟨u.preimage _ Nat.cast_injective.injOn ∪ u.preimage _ this.injOn,
      fun v' hv' ↦ ⟨v'.image Nat.cast ∪ v'.image Int.negSucc, fun x hx ↦ ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
f : ℤ → M
hf : HasProd f m
this : Injective Int.negSucc
u : Finset ℤ
v' : Finset ℕ
hv' : u.preimage Nat.cast ⋯ ∪ u.preimage Int.negSucc ⋯ ⊆ v'
x : ℤ
hx : x ∈ u
⊢ x ∈ image Nat.cast v' ∪ image Int.negSucc v'
have refine_1 : (∃ a ∈ v', (↑a : ℤ) = x) ∨ ∃ a ∈ v', Int.negSucc a = x
Tactic: simp only [mem_union, mem_image]