awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 → ∃ (N : ℕ), ∀ t ⊆ {n : ℕ | N ≤ n}, ∏' (n : (↑t : Type)), f (↑n : ℕ) ∈ e
e : Set G
he : Membership.mem (γ := Filter G) (𝓝 1) e
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
⊢ ∃ (s : Finset ℕ), ∀ (t : Set ℕ), Disjoint t (↑s : Set ℕ) → ∏' (b : (↑t : Type)), f (↑b : ℕ) ∈ e

Tactic:
obtain ⟨N, hN⟩ := 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 → ∃ (N : ℕ), ∀ t ⊆ {n : ℕ | N ≤ n}, ∏' (n : (↑t : Type)), f (↑n : ℕ) ∈ e
e : Set G
he : Membership.mem (γ := Filter G) (𝓝 1) e
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:
⟨range N, fun t ht ↦ hN _ fun n hnt ↦
      le_of_not_gt fun h ↦ Set.disjoint_left.mp ht hnt (mem_range.mpr h)⟩

Premises used: Iff.mpr, Set.disjoint_left, le_of_not_gt, Finset.mem_range, Finset.range, Exists.intro, Iff.mp
-- 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 → ∃ (N : ℕ), ∀ t ⊆ {n : ℕ | N ≤ n}, ∏' (n : (↑t : Type)), f (↑n : ℕ) ∈ e
e : Set G
he : Membership.mem (γ := Filter G) (𝓝 1) e
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:
exact ⟨range N, fun t ht ↦ hN _ fun n hnt ↦
      le_of_not_gt fun h ↦ Set.disjoint_left.mp ht hnt (mem_range.mpr h)⟩
-- 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
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
rw₁ 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
⊢ Multipliable f ↔
    ∀ (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]

Premises used: cauchySeq_finset_iff_nat_tprod_vanishing, multipliable_iff_cauchySeq_finset
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
f : ℕ → G
hf : Multipliable f
e : Set G
he : Membership.mem (γ := Filter G) (𝓝 1) e
⊢ ∃ (N : ℕ), ∀ t ⊆ {n : ℕ | N ≤ n}, ∏' (n : (↑t : Type)), f (↑n : ℕ) ∈ e

Tactic:
letI : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
  have : IsUniformGroup G := isUniformGroup_of_commGroup
  cauchySeq_finset_iff_nat_tprod_vanishing.1 hf.hasProd.cauchySeq e he

Premises used: Set.Mem, cauchySeq_finset_iff_nat_tprod_vanishing, Filter.Tendsto.cauchySeq, Multipliable.hasProd, Iff.mp, isUniformGroup_of_commGroup
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
f : ℕ → G
hf : Multipliable f
rw : Tendsto f cofinite (𝓝 1)
⊢ Tendsto f atTop (𝓝 1)

Tactic:
rw [← Nat.cofinite_eq_atTop]

Premises used: Nat.cofinite_eq_atTop
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
f : ℕ → G
hf : Multipliable f
⊢ Tendsto f cofinite (𝓝 1)

Tactic:
hf.tendsto_cofinite_one

Premises used: Multipliable.tendsto_cofinite_one
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
f : ℕ → G
hf : Multipliable f
⊢ Tendsto f cofinite (𝓝 1)

Tactic:
exact hf.tendsto_cofinite_one

Premises used: Multipliable.tendsto_cofinite_one
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
f : ℤ → M
hf : HasProd f m
change : HasProd (fun (n : ℕ) ↦ f (↑n : ℤ) * f (Int.negSucc n)) m
⊢ HasProd (fun (n : ℕ) ↦ f (↑n : ℤ) * f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) m

Tactic:
change HasProd (fun n : ℕ ↦ f n * f (Int.negSucc n)) m

Premises used: HMul.hMul, HasProd, Nat.cast, Int.negSucc, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
f : ℤ → M
hf : HasProd f m
⊢ Injective Int.negSucc

Tactic:
have : Injective Int.negSucc := @Int.negSucc.inj
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
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

Tactic:
hf.hasProd_of_prod_eq fun u ↦ ?_

Premises used: HasProd.hasProd_of_prod_eq
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
f : ℤ → M
hf : HasProd f m
this : Injective Int.negSucc
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))
⊢ HasProd (fun (n : ℕ) ↦ f (↑n : ℤ) * f (Int.negSucc n)) m

Tactic:
refine hf.hasProd_of_prod_eq fun u ↦ ?_

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

Tactic:
⟨u.preimage _ Nat.cast_injective.injOn ∪ u.preimage _ this.injOn,
      fun v' hv' ↦ ⟨v'.image Nat.cast ∪ v'.image Int.negSucc, fun x hx ↦ ?_, ?_⟩⟩

Premises used: Function.Injective.injOn, Nat.cast, Finset.preimage, And.intro, Exists.intro, Int.negSucc, Union.union, Nat.cast_injective, Finset.image
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
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'
refine_2 :
  ∀ (v' : Finset ℕ) (hv' : u.preimage Nat.cast ⋯ ∪ u.preimage Int.negSucc ⋯ ⊆ 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))
⊢ ∃ (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 ⟨u.preimage _ Nat.cast_injective.injOn ∪ u.preimage _ this.injOn,
      fun v' hv' ↦ ⟨v'.image Nat.cast ∪ v'.image Int.negSucc, fun x hx ↦ ?_, ?_⟩⟩
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
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
refine_1 : (∃ a ∈ v', (↑a : ℤ) = x) ∨ ∃ a ∈ v', Int.negSucc a = x
⊢ x ∈ image Nat.cast v' ∪ image Int.negSucc v'

Tactic:
simp only [mem_union, mem_image]

Premises used: Finset.mem_image, Finset.mem_union
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
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
refine_1 :
  ∀ (a : ℕ) (hx : Int.ofNat a ∈ u), (∃ a_1 ∈ v', (↑a_1 : ℤ) = Int.ofNat a) ∨ ∃ a_1 ∈ v', Int.negSucc a_1 = Int.ofNat a
refine_1₁ :
  ∀ (a : ℕ) (hx : Int.negSucc a ∈ u),
    (∃ a_1 ∈ v', (↑a_1 : ℤ) = Int.negSucc a) ∨ ∃ a_1 ∈ v', Int.negSucc a_1 = Int.negSucc a
⊢ (∃ a ∈ v', (↑a : ℤ) = x) ∨ ∃ a ∈ v', Int.negSucc a = x

Tactic:
cases x
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
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'
a : ℕ
hx : Int.ofNat a ∈ u
⊢ a ∈ u.preimage Nat.cast ⋯ ∪ u.preimage Int.negSucc ⋯

Tactic:
simpa using Or.inl hx

Premises used: Or.inl
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
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'
a : ℕ
hx : Int.ofNat a ∈ u
⊢ (∃ a_1 ∈ v', (↑a_1 : ℤ) = Int.ofNat a) ∨ ∃ a_1 ∈ v', Int.negSucc a_1 = Int.ofNat a

Tactic:
exact Or.inl ⟨_, hv' (by simpa using Or.inl hx), rfl⟩

Premises used: Or.inl
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
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'
a : ℕ
hx : Int.negSucc a ∈ u
⊢ a ∈ u.preimage Nat.cast ⋯ ∪ u.preimage Int.negSucc ⋯

Tactic:
simpa using Or.inr hx

Premises used: Or.inr
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
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'
a : ℕ
hx : Int.negSucc a ∈ u
⊢ (∃ a_1 ∈ v', (↑a_1 : ℤ) = Int.negSucc a) ∨ ∃ a_1 ∈ v', Int.negSucc a_1 = Int.negSucc a

Tactic:
exact Or.inr ⟨_, hv' (by simpa using Or.inr hx), rfl⟩

Premises used: Or.inr
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
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'
refine_2 : Disjoint (image Nat.cast v') (image Int.negSucc 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:
rw [prod_union, prod_image Nat.cast_injective.injOn, prod_image this.injOn,
      prod_mul_distrib]

Premises used: Finset.prod_mul_distrib, Function.Injective.injOn, Finset.prod_union, Nat.cast_injective, Finset.prod_image
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
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'
⊢ Disjoint (image Nat.cast v') (image Int.negSucc v')

Tactic:
simp only [disjoint_iff_ne, mem_image, ne_eq, forall_exists_index, and_imp,
      forall_apply_eq_imp_iff₂, not_false_eq_true, implies_true, reduceCtorEq]

Premises used: reduceCtorEq, Finset.mem_image, and_imp, forall_exists_index, Finset.disjoint_iff_ne, ne_eq, implies_true, not_false_eq_true, forall_apply_eq_imp_iff₂
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
f : ℤ → M
hf : Multipliable f
⊢ Multipliable.{u_1, 0} (α := M) fun (n : ℕ) ↦ f (↑n : ℤ) * f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)

Tactic:
hf.hasProd.nat_mul_neg_add_one.multipliable

Premises used: Multipliable.hasProd, HasProd.multipliable, HasProd.nat_mul_neg_add_one
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
inst_2 : T2Space M
f : ℤ → M
hf : Multipliable f
⊢ Eq.{u_1 + 1} (α := M) (∏' (n : ℕ), f (↑n : ℤ) * f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (∏' (n : ℤ), f n)

Tactic:
hf.hasProd.nat_mul_neg_add_one.tprod_eq

Premises used: HasProd.tprod_eq, Multipliable.hasProd, HasProd.nat_mul_neg_add_one
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m m' : M
inst_2 : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun (n : ℕ) ↦ f (↑n : ℤ)) m
hf₂ : HasProd (fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) m'
⊢ Injective Int.negSucc

Tactic:
have hi₂ : Injective Int.negSucc := @Int.negSucc.inj
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m m' : M
inst_2 : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun (n : ℕ) ↦ f (↑n : ℤ)) m
hf₂ : HasProd (fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) m'
hi₂ : Injective Int.negSucc
disjoint : Disjoint (Set.range Nat.cast) (Set.range Int.negSucc)
codisjoint : Codisjoint (Set.range Nat.cast) (Set.range Int.negSucc)
⊢ IsCompl (Set.range Nat.cast) (Set.range Int.negSucc)

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m m' : M
inst_2 : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun (n : ℕ) ↦ f (↑n : ℤ)) m
hf₂ : HasProd (fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) m'
hi₂ : Injective Int.negSucc
disjoint : Set.range Nat.cast ⊓ Set.range Int.negSucc ≤ ⊥
⊢ Disjoint (Set.range Nat.cast) (Set.range Int.negSucc)

Tactic:
rw [disjoint_iff_inf_le]

Premises used: disjoint_iff_inf_le
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m m' : M
inst_2 : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun (n : ℕ) ↦ f (↑n : ℤ)) m
hf₂ : HasProd (fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) m'
hi₂ : Injective Int.negSucc
codisjoint : ⊤ ≤ Set.range Nat.cast ⊔ Set.range Int.negSucc
⊢ Codisjoint (Set.range Nat.cast) (Set.range Int.negSucc)

Tactic:
rw [codisjoint_iff_le_sup]

Premises used: codisjoint_iff_le_sup
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m m' : M
inst_2 : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun (n : ℕ) ↦ f (↑n : ℤ)) m
hf₂ : HasProd (fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) m'
hi₂ : Injective Int.negSucc
i : ℕ
⊢ Membership.mem (γ := Set ℤ) ⊤ (Int.ofNat i) → Int.ofNat i ∈ Set.range Nat.cast ⊔ Set.range Int.negSucc

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m m' : M
inst_2 : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun (n : ℕ) ↦ f (↑n : ℤ)) m
hf₂ : HasProd (fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) m'
hi₂ : Injective Int.negSucc
j : ℕ
⊢ Membership.mem (γ := Set ℤ) ⊤ (Int.negSucc j) → Int.negSucc j ∈ Set.range Nat.cast ⊔ Set.range Int.negSucc

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m m' : M
inst_2 : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun (n : ℕ) ↦ f (↑n : ℤ)) m
hf₂ : HasProd (fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) m'
hi₂ : Injective Int.negSucc
⊢ IsCompl (Set.range Nat.cast) (Set.range Int.negSucc)

Tactic:
have : IsCompl (Set.range ((↑) : ℕ → ℤ)) (Set.range Int.negSucc) := by
    constructor
    · rw [disjoint_iff_inf_le]
      rintro _ ⟨⟨i, rfl⟩, ⟨j, ⟨⟩⟩⟩
    · rw [codisjoint_iff_le_sup]
      rintro (i | j) <;> simp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m m' : M
inst_2 : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun (n : ℕ) ↦ f (↑n : ℤ)) m
hf₂ : HasProd (fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) m'
hi₂ : Injective Int.negSucc
this : IsCompl (Set.range Nat.cast) (Set.range Int.negSucc)
⊢ HasProd f (m * m')

Tactic:
(Nat.cast_injective.hasProd_range_iff.mpr hf₁).mul_isCompl
    this (hi₂.hasProd_range_iff.mpr hf₂)

Premises used: Iff.mpr, HasProd.mul_isCompl, Nat.cast_injective, Function.Injective.hasProd_range_iff
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m m' : M
inst_2 : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun (n : ℕ) ↦ f (↑n : ℤ)) m
hf₂ : HasProd (fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) m'
hi₂ : Injective Int.negSucc
this : IsCompl (Set.range Nat.cast) (Set.range Int.negSucc)
⊢ HasProd f (m * m')

Tactic:
exact (Nat.cast_injective.hasProd_range_iff.mpr hf₁).mul_isCompl
    this (hi₂.hasProd_range_iff.mpr hf₂)

Premises used: Iff.mpr, HasProd.mul_isCompl, Nat.cast_injective, Function.Injective.hasProd_range_iff
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
f : ℤ → M
hf₁ : Multipliable.{u_1, 0} (α := M) fun (n : ℕ) ↦ f (↑n : ℤ)
hf₂ : Multipliable.{u_1, 0} (α := M) fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
⊢ Multipliable f

Tactic:
(hf₁.hasProd.of_nat_of_neg_add_one hf₂.hasProd).multipliable

Premises used: HasProd.of_nat_of_neg_add_one, Multipliable.hasProd, HasProd.multipliable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
inst_3 : T2Space M
f : ℤ → M
hf₁ : Multipliable.{u_1, 0} (α := M) fun (n : ℕ) ↦ f (↑n : ℤ)
hf₂ : Multipliable.{u_1, 0} (α := M) fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
⊢ ∏' (n : ℤ), f n = HMul.hMul (α := M) (∏' (n : ℕ), f (↑n : ℤ)) (∏' (n : ℕ), f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))

Tactic:
(hf₁.hasProd.of_nat_of_neg_add_one hf₂.hasProd).tprod_eq

Premises used: HasProd.of_nat_of_neg_add_one, HasProd.tprod_eq, Multipliable.hasProd
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m m' : M
inst_2 : ContinuousMul M
f g : ℕ → M
hf : HasProd f m
hg : HasProd g m'
⊢ HasProd (fun (t : ℤ) ↦ Int.rec (motive := fun (x : ℤ) ↦ M) f g t) (m * m')

Tactic:
HasProd.of_nat_of_neg_add_one hf hg

Premises used: HasProd.of_nat_of_neg_add_one
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
f g : ℕ → M
hf : Multipliable f
hg : Multipliable g
⊢ Multipliable.{u_1, 0} (α := M) fun (t : ℤ) ↦ Int.rec (motive := fun (x : ℤ) ↦ M) f g t

Tactic:
.of_nat_of_neg_add_one hf hg

Premises used: Multipliable.of_nat_of_neg_add_one
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
inst_3 : T2Space M
f g : ℕ → M
hf : Multipliable f
hg : Multipliable g
⊢ ∏' (n : ℤ), Int.rec (motive := fun (x : ℤ) ↦ M) f g n = HMul.hMul (α := M) (∏' (n : ℕ), f n) (∏' (n : ℕ), g n)

Tactic:
(hf.hasProd.int_rec hg.hasProd).tprod_eq

Premises used: HasProd.tprod_eq, HasProd.int_rec, Multipliable.hasProd
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
inst_2 : ContinuousMul M
f : ℤ → M
hf : HasProd f m
apply :
  ∀ (u : Finset ℤ),
    ∃ (v : Finset ℕ),
      ∀ (v' : Finset ℕ),
        v ⊆ v' →
          ∃ (u' : Finset ℤ),
            u ⊆ u' ∧
              Eq.{u_1 + 1} (α := M) (∏ x ∈ u', f x * if x = 0 then f 0 else 1) (∏ b ∈ v', f (↑b : ℤ) * f (-(↑b : ℤ)))
⊢ HasProd (fun (n : ℕ) ↦ f (↑n : ℤ) * f (-(↑n : ℤ))) (m * f 0)

Tactic:
apply (hf.mul (hasProd_ite_eq (0 : ℤ) (f 0))).hasProd_of_prod_eq fun u ↦ ?_

Premises used: hasProd_ite_eq, HasProd.hasProd_of_prod_eq, HasProd.mul, OfNat.ofNat, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
inst_2 : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
⊢ ∃ (v : Finset ℕ),
    ∀ (v' : Finset ℕ),
      v ⊆ v' →
        ∃ (u' : Finset ℤ),
          u ⊆ u' ∧
            Eq.{u_1 + 1} (α := M) (∏ x ∈ u', f x * if x = 0 then f 0 else 1) (∏ b ∈ v', f (↑b : ℤ) * f (-(↑b : ℤ)))

Tactic:
⟨u.image Int.natAbs, fun v' hv' ↦ ?_⟩

Premises used: Int.natAbs, Exists.intro, Finset.image
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
inst_2 : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
refine :
  ∀ (v' : Finset ℕ) (hv' : image Int.natAbs u ⊆ v'),
    ∃ (u' : Finset ℤ),
      u ⊆ u' ∧ Eq.{u_1 + 1} (α := M) (∏ x ∈ u', f x * if x = 0 then f 0 else 1) (∏ b ∈ v', f (↑b : ℤ) * f (-(↑b : ℤ)))
⊢ ∃ (v : Finset ℕ),
    ∀ (v' : Finset ℕ),
      v ⊆ v' →
        ∃ (u' : Finset ℤ),
          u ⊆ u' ∧
            Eq.{u_1 + 1} (α := M) (∏ x ∈ u', f x * if x = 0 then f 0 else 1) (∏ b ∈ v', f (↑b : ℤ) * f (-(↑b : ℤ)))

Tactic:
refine ⟨u.image Int.natAbs, fun v' hv' ↦ ?_⟩
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
inst_2 : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun (x : ℕ) ↦ (↑x : ℤ)) v'
u2 : Finset ℤ := image (fun (x : ℕ) ↦ -(↑x : ℤ)) v'
x : ℤ
hx : x ∈ u
simp : (∃ a ∈ v', (↑a : ℤ) = x) ∨ ∃ a ∈ v', -(↑a : ℤ) = x
⊢ x ∈ u1 ∪ u2

Tactic:
simp only [u1, u2, mem_union, mem_image]

Premises used: Finset.mem_image, Finset.mem_union
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
inst_2 : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun (x : ℕ) ↦ (↑x : ℤ)) v'
u2 : Finset ℤ := image (fun (x : ℕ) ↦ -(↑x : ℤ)) v'
x : ℤ
hx : x ∈ u
inl : ∀ (h'x : 0 ≤ x), (∃ a ∈ v', (↑a : ℤ) = x) ∨ ∃ a ∈ v', -(↑a : ℤ) = x
inr : ∀ (h'x : x ≤ 0), (∃ a ∈ v', (↑a : ℤ) = x) ∨ ∃ a ∈ v', -(↑a : ℤ) = x
⊢ (∃ a ∈ v', (↑a : ℤ) = x) ∨ ∃ a ∈ v', -(↑a : ℤ) = x

Tactic:
rcases le_total 0 x with (h'x | h'x)

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
inst_2 : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun (x : ℕ) ↦ (↑x : ℤ)) v'
u2 : Finset ℤ := image (fun (x : ℕ) ↦ -(↑x : ℤ)) v'
x : ℤ
hx : x ∈ u
h'x : 0 ≤ x
⊢ (∃ a ∈ v', (↑a : ℤ) = x) ∨ ∃ a ∈ v', -(↑a : ℤ) = x

Tactic:
Or.inl ⟨_, hv' <| mem_image.mpr ⟨x, hx, rfl⟩, ?_⟩

Premises used: Iff.mpr, Finset.mem_image, And.intro, Exists.intro, Or.inl, rfl
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
inst_2 : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun (x : ℕ) ↦ (↑x : ℤ)) v'
u2 : Finset ℤ := image (fun (x : ℕ) ↦ -(↑x : ℤ)) v'
x : ℤ
hx : x ∈ u
h'x : 0 ≤ x
inl : (↑x.natAbs : ℤ) = x
⊢ (∃ a ∈ v', (↑a : ℤ) = x) ∨ ∃ a ∈ v', -(↑a : ℤ) = x

Tactic:
refine Or.inl ⟨_, hv' <| mem_image.mpr ⟨x, hx, rfl⟩, ?_⟩

Premises used: Or.inl
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
inst_2 : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun (x : ℕ) ↦ (↑x : ℤ)) v'
u2 : Finset ℤ := image (fun (x : ℕ) ↦ -(↑x : ℤ)) v'
x : ℤ
hx : x ∈ u
h'x : 0 ≤ x
⊢ (↑x.natAbs : ℤ) = x

Tactic:
simp only [Int.natCast_natAbs, abs_eq_self, h'x]

Premises used: abs_eq_self, Int.natCast_natAbs