awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
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
⊢ decode₂ β n = none

Tactic:
rw [← decode₂_ne_none_iff, ne_eq, not_not] at hn

Premises used: Classical.not_not, ne_eq, Encodable.decode₂_ne_none_iff
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
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 : decode₂ β n = none
⊢ m (⨆ b ∈ decode₂ β n, s b) = 1 n

Tactic:
simp [hn, m0]
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
α : Type u_3
β : Type u_4
inst_2 : Encodable β
m : Set α → M
m0 : m ∅ = 1
s : β → Set α
⊢ Eq.{u_1 + 1} (α := M) (∏' (i : ℕ), m (⋃ b ∈ decode₂ β i, s b)) (∏' (b : β), m (s b))

Tactic:
tprod_iSup_decode₂ m m0 s

Premises used: tprod_iSup_decode₂, Set.iUnion
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
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 : β → α
intro : ∀ (val : Encodable β), R (m (⨆ (b : β), s b)) (∏' (b : β), m (s b))
⊢ R (m (⨆ (b : β), s b)) (∏' (b : β), m (s b))

Tactic:
cases nonempty_encodable β

Premises used: nonempty_encodable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
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 β
intro : R (m (⨆ (i : ℕ), ⨆ b ∈ decode₂ β i, s b)) (∏' (i : ℕ), m (⨆ b ∈ decode₂ β i, s b))
⊢ R (m (⨆ (b : β), s b)) (∏' (b : β), m (s b))

Tactic:
rw [← iSup_decode₂, ← tprod_iSup_decode₂ _ m0 s]

Premises used: Encodable.iSup_decode₂, tprod_iSup_decode₂
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
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 (⨆ (i : ℕ), ⨆ b ∈ decode₂ β i, s b)) (∏' (i : ℕ), m (⨆ b ∈ decode₂ β i, s b))

Tactic:
m_iSup _
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
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 (⨆ (i : ℕ), ⨆ b ∈ decode₂ β i, s b)) (∏' (i : ℕ), m (⨆ b ∈ decode₂ β i, s b))

Tactic:
exact m_iSup _
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
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 γ
rw : R (m (⨆ (x : Subtype (Membership.mem t)), s (↑x : γ))) (∏' (x : ↥t), m (s (↑x : γ)))
⊢ R (m (⨆ d ∈ t, s d)) (∏ d ∈ t, m (s d))

Tactic:
rw [iSup_subtype', ← Finset.tprod_subtype]

Premises used: iSup_subtype', Finset.tprod_subtype
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
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 (⨆ (x : Subtype (Membership.mem t)), s (↑x : γ))) (∏' (x : ↥t), m (s (↑x : γ)))

Tactic:
rel_iSup_tprod m m0 R m_iSup _

Premises used: rel_iSup_tprod
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
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 (⨆ (x : Subtype (Membership.mem t)), s (↑x : γ))) (∏' (x : ↥t), m (s (↑x : γ)))

Tactic:
exact rel_iSup_tprod m m0 R m_iSup _

Premises used: rel_iSup_tprod
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
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 (⨆ (b : Bool), bif b then s₁ else s₂)) (∏' (b : Bool), m (bif b then s₁ else s₂))

Tactic:
rel_iSup_tprod m m0 R m_iSup fun b ↦ cond b s₁ s₂

Premises used: cond, rel_iSup_tprod
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
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₂
h₁ : m s₁ * m s₂ = ∏' (b : Bool), m (bif b then s₁ else s₂)
⊢ R (m (s₁ ⊔ s₂)) (m s₁ * m s₂)

Tactic:
convert! rel_iSup_tprod m m0 R m_iSup fun b ↦ cond b s₁ s₂

Premises used: cond, rel_iSup_tprod
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
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₂ : α
⊢ s₁ ⊔ s₂ = ⨆ (b : Bool), bif b then s₁ else s₂

Tactic:
simp only [iSup_bool_eq, cond]

Premises used: cond, iSup_bool_eq
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
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₂)
h₃ h₄ : m s₁ * m s₂ = m s₁ * m s₂
⊢ m s₁ * m s₂ = ∏' (b : Bool), m (bif b then s₁ else s₂)

Tactic:
rw [tprod_fintype, Fintype.prod_bool, cond, cond]

Premises used: cond, tprod_fintype, Fintype.prod_bool
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
inst_2 : T2Space M
inst_3 : ContinuousMul M
f : ℕ → M
k : ℕ
h : Multipliable.{u_1, 0} (α := M) fun (n : ℕ) ↦ f (n + k)
⊢ HMul.hMul (α := M) (∏ i ∈ range k, f i) (∏' (i : ℕ), f (i + k)) = ∏' (i : ℕ), f i

Tactic:
h.hasProd.prod_range_mul.tprod_eq.symm

Premises used: HasProd.tprod_eq, Multipliable.hasProd, Eq.symm, HasProd.prod_range_mul
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
inst_2 : T2Space M
inst_3 : ContinuousMul M
f : ℕ → M
hf : Multipliable.{u_1, 0} (α := M) fun (n : ℕ) ↦ f (n + 1)
⊢ ∏' (b : ℕ), f b = f 0 * ∏' (b : ℕ), f (b + 1)

Tactic:
simpa only [prod_range_one] using hf.prod_mul_tprod_nat_mul'.symm

Premises used: Finset.prod_range_one, Multipliable.prod_mul_tprod_nat_mul', Eq.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
inst_2 : T2Space M
inst_3 : ContinuousMul M
f : ℕ → M
he : Multipliable.{u_1, 0} (α := M) fun (k : ℕ) ↦ f (2 * k)
ho : Multipliable.{u_1, 0} (α := M) fun (k : ℕ) ↦ f (2 * k + 1)
⊢ HMul.hMul (α := M) (∏' (k : ℕ), f (2 * k)) (∏' (k : ℕ), f (2 * k + 1)) = ∏' (k : ℕ), f k

Tactic:
(he.hasProd.even_mul_odd ho.hasProd).tprod_eq.symm

Premises used: HasProd.tprod_eq, Multipliable.hasProd, HasProd.even_mul_odd, Eq.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
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)

Tactic:
Iff.trans ?_ (range k).hasProd_compl_iff

Premises used: Finset.range, Iff.trans, Finset.hasProd_compl_iff
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
G : Type u_2
inst : CommGroup G
g : G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
f : ℕ → G
k : ℕ
refine : HasProd (fun (n : ℕ) ↦ f (n + k)) g ↔ HasProd (fun (x : { x : ℕ // x ∉ range k }) ↦ f (↑x : ℕ)) g
⊢ HasProd (fun (n : ℕ) ↦ f (n + k)) g ↔ HasProd f (g * ∏ i ∈ range k, f i)

Tactic:
refine Iff.trans ?_ (range k).hasProd_compl_iff

Premises used: Finset.range, Iff.trans, Finset.hasProd_compl_iff
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
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
rw₂ rw₃ :
  HasProd (fun (n : ℕ) ↦ f (n + k)) g ↔
    HasProd
      (fun (x : ℕ) ↦
        f (↑((fun (j : ℕ) ↦ (Subtype.mk (p := fun (n : ℕ) ↦ n ∉ range k) (j + k) ⋯ : { n : ℕ // n ∉ range k })) x) : ℕ))
      g
⊢ HasProd (fun (n : ℕ) ↦ f (n + k)) g ↔ HasProd (fun (x : { x : ℕ // x ∉ range k }) ↦ f (↑x : ℕ)) g

Tactic:
rw [← (notMemRangeEquiv k).symm.hasProd_iff, Function.comp_def, coe_notMemRangeEquiv_symm]

Premises used: Equiv.hasProd_iff, Function.comp_def, coe_notMemRangeEquiv_symm, Equiv.symm, notMemRangeEquiv
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
f : ℕ → G
k : ℕ
⊢ (Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (n + k)) ↔ Multipliable f

Tactic:
Iff.symm <|
    (Equiv.mulRight (∏ i ∈ range k, f i)).surjective.multipliable_iff_of_hasProd_iff
      (hasProd_nat_add_iff k).symm

Premises used: hasProd_nat_add_iff, Finset.prod, Finset.range, Equiv.mulRight, Equiv.surjective, Function.Surjective.multipliable_iff_of_hasProd_iff, Iff.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
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 / ∏ i ∈ range k, f i) ↔ HasProd f g

Tactic:
simp [hasProd_nat_add_iff]

Premises used: hasProd_nat_add_iff
-- 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
k : ℕ
h : Multipliable f
⊢ HMul.hMul (α := G) (∏ i ∈ range k, f i) (∏' (i : ℕ), f (i + k)) = ∏' (i : ℕ), f i

Tactic:
Multipliable.prod_mul_tprod_nat_mul' <| (multipliable_nat_add_iff k).2 h

Premises used: Iff.mpr, multipliable_nat_add_iff, Multipliable.prod_mul_tprod_nat_mul'
-- 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
⊢ ∏' (b : ℕ), f b = f 0 * ∏' (b : ℕ), f (b + 1)

Tactic:
tprod_eq_zero_mul' <| (multipliable_nat_add_iff 1).2 hf

Premises used: tprod_eq_zero_mul', Iff.mpr, multipliable_nat_add_iff, OfNat.ofNat
-- 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
pos : ∀ (hf : Multipliable f), Tendsto.{0, u_2} (β := G) (fun (i : ℕ) ↦ ∏' (k : ℕ), f (k + i)) atTop (𝓝 1)
neg : ∀ (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)

Tactic:
by_cases hf : Multipliable f

Premises used: Multipliable, SummationFilter.unconditional
-- 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
h : ∀ (i : ℕ), HDiv.hDiv (α := G) (∏' (i : ℕ), f i) (∏ j ∈ range i, f j) = ∏' (k : ℕ), f (k + i)
⊢ 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:
ext1 i
-- 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
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))
h₂ h₃ : Eq.{u_2 + 1} (α := G) (∏' (i : ℕ), f i) (∏' (i : ℕ), f i)
⊢ HDiv.hDiv (α := G) (∏' (i : ℕ), f i) (∏ 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]

Premises used: Multipliable.prod_mul_tprod_nat_add, div_eq_iff_eq_mul, mul_comm
-- 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
⊢ 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]
-- 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
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 (x : ℕ) ↦ ∏' (i : ℕ), f i) atTop (𝓝 (∏' (i : ℕ), f i))

Tactic:
have h₁ : Tendsto (fun _ : ℕ ↦ ∏' i, f i) atTop (𝓝 (∏' i, f i)) := tendsto_const_nhds
-- 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
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)
h₁ : Tendsto.{0, u_2} (β := G) (fun (x : ℕ) ↦ ∏' (i : ℕ), f i) atTop (𝓝 (∏' (i : ℕ), f i))
⊢ Tendsto.{0, u_2} (β := G) (fun (i : ℕ) ↦ ∏' (k : ℕ), f (k + i)) atTop (𝓝 1)

Tactic:
simpa only [h₀, div_self'] using Tendsto.div' h₁ hf.hasProd.tendsto_prod_nat

Premises used: HasProd.tendsto_prod_nat, Multipliable.hasProd, div_self', Filter.Tendsto.div'
-- 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
⊢ Tendsto.{0, u_2} (β := G) (fun (i : ℕ) ↦ ∏' (k : ℕ), f (k + i)) atTop (𝓝 1)

Tactic:
tendsto_const_nhds.congr fun n ↦ (tprod_eq_one_of_not_multipliable ?_).symm

Premises used: tendsto_const_nhds, tprod_eq_one_of_not_multipliable, Filter.Tendsto.congr, 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
neg : ∀ (n : ℕ), ¬Multipliable.{u_2, 0} (α := G) fun (k : ℕ) ↦ f (k + n)
⊢ Tendsto.{0, u_2} (β := G) (fun (i : ℕ) ↦ ∏' (k : ℕ), f (k + i)) atTop (𝓝 1)

Tactic:
refine tendsto_const_nhds.congr fun n ↦ (tprod_eq_one_of_not_multipliable ?_).symm

Premises used: tendsto_const_nhds, tprod_eq_one_of_not_multipliable, Filter.Tendsto.congr, 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
n : ℕ
neg neg₁ neg₂ neg₃ : ¬Multipliable f
⊢ ¬Multipliable.{u_2, 0} (α := G) fun (k : ℕ) ↦ f (k + n)

Tactic:
rwa [multipliable_nat_add_iff n]

Premises used: multipliable_nat_add_iff
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
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

Tactic:
cauchySeq_finset_iff_tprod_vanishing.trans ⟨fun vanish e he ↦ ?_, fun vanish e he ↦ ?_⟩

Premises used: cauchySeq_finset_iff_tprod_vanishing, Iff.intro, Iff.trans
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
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
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
⊢ (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

Tactic:
refine cauchySeq_finset_iff_tprod_vanishing.trans ⟨fun vanish e he ↦ ?_, fun vanish e he ↦ ?_⟩

Premises used: cauchySeq_finset_iff_tprod_vanishing, Iff.intro, Iff.trans
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
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
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
⊢ ∃ (N : ℕ), ∀ t ⊆ {n : ℕ | N ≤ n}, ∏' (n : (↑t : Type)), f (↑n : ℕ) ∈ e

Tactic:
obtain ⟨s, hs⟩ := vanish e he
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
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

Tactic:
⟨if h : s.Nonempty then s.max' h + 1 else 0,
      fun t ht ↦ hs _ <| Set.disjoint_left.mpr ?_⟩

Premises used: Iff.mpr, Set.disjoint_left, Finset.max', dite, HAdd.hAdd, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
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
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 ℕ)
⊢ ∃ (N : ℕ), ∀ t ⊆ {n : ℕ | N ≤ n}, ∏' (n : (↑t : Type)), f (↑n : ℕ) ∈ e

Tactic:
refine ⟨if h : s.Nonempty then s.max' h + 1 else 0,
      fun t ht ↦ hs _ <| Set.disjoint_left.mpr ?_⟩
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
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 ℕ)
neg : ∀ (h : ¬s.Nonempty) (ht : t ⊆ {n : ℕ | 0 ≤ n}) ⦃a : ℕ⦄, a ∈ t → a ∉ (↑s : Set ℕ)
⊢ ∀ ⦃a : ℕ⦄, a ∈ t → a ∉ (↑s : Set ℕ)

Tactic:
split_ifs at ht with h
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
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 ℕ
h : s.Nonempty
ht : t ⊆ {n : ℕ | s.max' h + 1 ≤ n}
⊢ ∀ ⦃a : ℕ⦄, a ∈ t → a ∉ (↑s : Set ℕ)

Tactic:
fun m hmt hms ↦ (s.le_max' _ hms).not_gt (Nat.succ_le_iff.mp <| ht hmt)

Premises used: LE.le.not_gt, Finset.le_max', Iff.mp, Nat.succ_le_iff, Not
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
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 ℕ
h : s.Nonempty
ht : t ⊆ {n : ℕ | s.max' h + 1 ≤ n}
⊢ ∀ ⦃a : ℕ⦄, a ∈ t → a ∉ (↑s : Set ℕ)

Tactic:
exact fun m hmt hms ↦ (s.le_max' _ hms).not_gt (Nat.succ_le_iff.mp <| ht hmt)

Premises used: LE.le.not_gt, Finset.le_max', Iff.mp, Nat.succ_le_iff
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
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 ℕ
h : ¬s.Nonempty
ht : t ⊆ {n : ℕ | 0 ≤ n}
⊢ ∀ ⦃a : ℕ⦄, a ∈ t → a ∉ (↑s : Set ℕ)

Tactic:
fun _ _ hs ↦ h ⟨_, hs⟩

Premises used: Exists.intro, Not
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
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 ℕ
h : ¬s.Nonempty
ht : t ⊆ {n : ℕ | 0 ≤ n}
⊢ ∀ ⦃a : ℕ⦄, a ∈ t → a ∉ (↑s : Set ℕ)

Tactic:
exact fun _ _ hs ↦ h ⟨_, hs⟩

Premises used: Exists.intro