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
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 : x ≤ 0
⊢ (∃ a ∈ v', (↑a : ℤ) = x) ∨ ∃ a ∈ v', -(↑a : ℤ) = x

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

Premises used: Iff.mpr, Finset.mem_image, And.intro, Exists.intro, Or.inr, 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 : x ≤ 0
inr : -(↑x.natAbs : ℤ) = x
⊢ (∃ a ∈ v', (↑a : ℤ) = x) ∨ ∃ a ∈ v', -(↑a : ℤ) = x

Tactic:
refine Or.inr ⟨_, hv' <| mem_image.mpr ⟨x, 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
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 : x ≤ 0
⊢ -(↑x.natAbs : ℤ) = x

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

Premises used: neg_neg, abs_of_nonpos, Int.natCast_natAbs
-- 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'
⊢ u ⊆ u1 ∪ u2

Tactic:
have A : u ⊆ u1 ∪ u2 := by
    intro x hx
    simp only [u1, u2, mem_union, mem_image]
    rcases le_total 0 x with (h'x | h'x)
    · refine Or.inl ⟨_, hv' <| mem_image.mpr ⟨x, hx, rfl⟩, ?_⟩
      simp only [Int.natCast_natAbs, abs_eq_self, h'x]
    · refine Or.inr ⟨_, hv' <| mem_image.mpr ⟨x, hx, rfl⟩, ?_⟩
      simp only [abs_of_nonpos h'x, Int.natCast_natAbs, neg_neg]
-- 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'
A : u ⊆ u1 ∪ u2
rw :
  HMul.hMul (α := M) (∏ x ∈ u1 ∪ u2, f x) (∏ x ∈ u1 ∪ u2, if x = 0 then f 0 else 1) =
    HMul.hMul (α := M) (∏ x ∈ u1 ∪ u2, f x) (∏ x ∈ u1 ∩ u2, f x)
⊢ (∏ x ∈ u1 ∪ u2, f x * if x = 0 then f 0 else 1) = HMul.hMul (α := M) (∏ x ∈ u1 ∪ u2, f x) (∏ x ∈ u1 ∩ u2, f x)

Tactic:
rw [prod_mul_distrib]

Premises used: Finset.prod_mul_distrib
-- 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'
A : u ⊆ u1 ∪ u2
e_a : Eq.{u_1 + 1} (α := M) (∏ x ∈ u1 ∪ u2, if x = 0 then f 0 else 1) (∏ x ∈ u1 ∩ u2, f x)
⊢ HMul.hMul (α := M) (∏ x ∈ u1 ∪ u2, f x) (∏ x ∈ u1 ∪ u2, if x = 0 then f 0 else 1) =
    HMul.hMul (α := M) (∏ x ∈ u1 ∪ u2, f x) (∏ x ∈ u1 ∩ u2, f x)

Tactic:
congr 1
-- 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'
A : u ⊆ u1 ∪ u2
⊢ Eq.{u_1 + 1} (α := M) (∏ x ∈ u1 ∪ u2, if x = 0 then f 0 else 1) (∏ x ∈ u1 ∩ u2, f x)

Tactic:
(prod_subset_one_on_sdiff inter_subset_union ?_ ?_).symm

Premises used: Finset.inter_subset_union, Eq.symm, Finset.prod_subset_one_on_sdiff
-- 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'
A : u ⊆ u1 ∪ u2
e_a : ∀ x ∈ (u1 ∪ u2) \ (u1 ∩ u2), (if x = 0 then f 0 else 1) = 1
e_a₁ : ∀ x ∈ u1 ∩ u2, f x = if x = 0 then f 0 else 1
⊢ Eq.{u_1 + 1} (α := M) (∏ x ∈ u1 ∪ u2, if x = 0 then f 0 else 1) (∏ x ∈ u1 ∩ u2, f x)

Tactic:
refine (prod_subset_one_on_sdiff inter_subset_union ?_ ?_).symm

Premises used: Finset.inter_subset_union, Eq.symm, Finset.prod_subset_one_on_sdiff
-- 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'
A : u ⊆ u1 ∪ u2
x : ℤ
hx : x ∈ (u1 ∪ u2) \ (u1 ∩ u2)
this : x ≠ 0
⊢ (if x = 0 then f 0 else 1) = 1

Tactic:
simp only [this, if_false]

Premises used: if_false
-- 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'
A : u ⊆ u1 ∪ u2
x : ℤ
hx : x ∈ (u1 ∪ u2) \ (u1 ∩ u2)
e_a : x ≠ 0
⊢ (if x = 0 then f 0 else 1) = 1

Tactic:
suffices x ≠ 0 by simp only [this, if_false]
-- 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'
A : u ⊆ u1 ∪ u2
hx : 0 ∈ (u1 ∪ u2) \ (u1 ∩ u2)
⊢ False

Tactic:
simp [u1, u2] at hx
-- 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'
A : u ⊆ u1 ∪ u2
x : ℤ
hx : x ∈ u1 ∩ u2
⊢ (∃ a ∈ v', (↑a : ℤ) = x) ∧ ∃ a ∈ v', -(↑a : ℤ) = x

Tactic:
simp only [u1, u2, mem_inter, mem_image] at hx

Premises used: Finset.mem_image, Finset.mem_inter
-- 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'
A : u ⊆ u1 ∪ u2
x : ℤ
hx : (∃ a ∈ v', (↑a : ℤ) = x) ∧ ∃ a ∈ v', -(↑a : ℤ) = x
this : x = 0
⊢ f x = if x = 0 then f 0 else 1

Tactic:
simp only [this, if_true]

Premises used: if_true
-- 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'
A : u ⊆ u1 ∪ u2
x : ℤ
hx : (∃ a ∈ v', (↑a : ℤ) = x) ∧ ∃ a ∈ v', -(↑a : ℤ) = x
e_a : x = 0
⊢ f x = if x = 0 then f 0 else 1

Tactic:
suffices x = 0 by simp only [this, if_true]
-- 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'
A : u ⊆ u1 ∪ u2
x : ℤ
hx : (∃ a ∈ v', (↑a : ℤ) = x) ∧ ∃ a ∈ v', -(↑a : ℤ) = x
⊢ x = 0

Tactic:
lia
-- 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'
A : u ⊆ u1 ∪ u2
⊢ HMul.hMul (α := M) (∏ x ∈ u1, f x) (∏ x ∈ u2, f x) =
    HMul.hMul (α := M) (∏ b ∈ v', f (↑b : ℤ)) (∏ b ∈ v', f (-(↑b : ℤ)))

Tactic:
simp [u1, u2]
-- 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'
A : u ⊆ u1 ∪ u2
⊢ ∃ (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:
exact ⟨_, A, calc
    (∏ x ∈ u1 ∪ u2, (f x * if x = 0 then f 0 else 1)) =
        (∏ x ∈ u1 ∪ u2, f x) * ∏ x ∈ u1 ∩ u2, f x := by
      rw [prod_mul_distrib]
      congr 1
      refine (prod_subset_one_on_sdiff inter_subset_union ?_ ?_).symm
      · intro x hx
        suffices x ≠ 0 by simp only [this, if_false]
        rintro rfl
        simp [u1, u2] at hx
      · intro x hx
        simp only [u1, u2, mem_inter, mem_image] at hx
        suffices x = 0 by simp only [this, if_true]
        lia
    _ = (∏ x ∈ u1, f x) * ∏ x ∈ u2, f x := prod_union_inter
    _ = (∏ b ∈ v', f b) * ∏ b ∈ v', f (-b) := by simp [u1, u2]
    _ = ∏ b ∈ v', (f b * f (-b)) := prod_mul_distrib.symm⟩
-- 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 f
⊢ Multipliable.{u_1, 0} (α := M) fun (n : ℕ) ↦ f (↑n : ℤ) * f (-(↑n : ℤ))

Tactic:
hf.hasProd.nat_mul_neg.multipliable

Premises used: HasProd.nat_mul_neg, 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 f
⊢ ∏' (n : ℕ), f (↑n : ℤ) * f (-(↑n : ℤ)) = (∏' (n : ℤ), f n) * f 0

Tactic:
hf.hasProd.nat_mul_neg.tprod_eq

Premises used: HasProd.nat_mul_neg, 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 : ℤ → M
hf₁ : HasProd (fun (n : ℕ) ↦ f (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) m
hf₂ : HasProd (fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) m'
⊢ HasProd f (m * f 0 * m')

Tactic:
HasProd.of_nat_of_neg_add_one (mul_comm _ m ▸ HasProd.zero_mul hf₁) hf₂

Premises used: HasProd.zero_mul, HasProd.of_nat_of_neg_add_one, Eq.rec, mul_comm
-- 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 (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
hf₂ : Multipliable.{u_1, 0} (α := M) fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
⊢ Multipliable f

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

Premises used: HasProd.of_add_one_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 (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
hf₂ : Multipliable.{u_1, 0} (α := M) fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
⊢ ∏' (n : ℤ), f n =
    (∏' (n : ℕ), f (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) * f 0 * ∏' (n : ℕ), f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)

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

Premises used: HasProd.of_add_one_of_neg_add_one, HasProd.tprod_eq, Multipliable.hasProd
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
G : Type u_2
inst : CommGroup G
g g' : G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
f : ℤ → G
hf₁ : HasProd (fun (n : ℕ) ↦ f (↑n : ℤ)) g
hf₂ : HasProd (fun (n : ℕ) ↦ f (-(↑n : ℤ))) g'
⊢ HasProd f (g * g' / f 0)

Tactic:
mul_div_assoc' g .. ▸ hf₁.of_nat_of_neg_add_one (m' := g' / f 0) ?_

Premises used: HasProd.of_nat_of_neg_add_one, Eq.rec, mul_div_assoc'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
G : Type u_2
inst : CommGroup G
g g' : G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
f : ℤ → G
hf₁ : HasProd (fun (n : ℕ) ↦ f (↑n : ℤ)) g
hf₂ : HasProd (fun (n : ℕ) ↦ f (-(↑n : ℤ))) g'
refine : HasProd (fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (g' / f 0)
⊢ HasProd f (g * g' / f 0)

Tactic:
refine mul_div_assoc' g .. ▸ hf₁.of_nat_of_neg_add_one (m' := g' / f 0) ?_
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
G : Type u_2
inst : CommGroup G
g g' : G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
f : ℤ → G
hf₁ : HasProd (fun (n : ℕ) ↦ f (↑n : ℤ)) g
hf₂ : HasProd (fun (n : ℕ) ↦ f (-(↑n : ℤ))) g'
rwa :
  ∀ (hf₂ : HasProd (fun (n : ℕ) ↦ f (-(↑(n + 1) : ℤ))) (g' / ∏ i ∈ range 1, f (-(↑i : ℤ)))),
    HasProd (fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (g' / f 0)
rwa₁ :
  ∀ (hf₂ : HasProd (fun (n : ℕ) ↦ f (-(↑(n + 1) : ℤ))) (g' / f (-(↑0 : ℤ)))),
    HasProd (fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (g' / f 0)
rwa₂ :
  ∀ (hf₂ : HasProd (fun (n : ℕ) ↦ f (-(↑(n + 1) : ℤ))) (g' / f (-0))),
    HasProd (fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (g' / f 0)
rwa₃ rwa₄ rwa₅ rwa₆ :
  ∀ (hf₂ : HasProd (fun (n : ℕ) ↦ f (-(↑(n + 1) : ℤ))) (g' / f 0)),
    HasProd (fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (g' / f 0)
⊢ HasProd (fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (g' / f 0)

Tactic:
rwa [← hasProd_nat_add_iff' 1, prod_range_one, Nat.cast_zero, neg_zero] at hf₂

Premises used: Finset.prod_range_one, hasProd_nat_add_iff', Nat.cast_zero, OfNat.ofNat, neg_zero
-- 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.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (↑n : ℤ)
hf₂ : Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (-(↑n : ℤ))
⊢ Multipliable f

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

Premises used: Multipliable.hasProd, HasProd.multipliable, HasProd.of_nat_of_neg
-- 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.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (↑n : ℤ)
hf₂ : Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (-(↑n : ℤ))
⊢ ∏' (n : ℤ), f n = HMul.hMul (α := G) (∏' (n : ℕ), f (↑n : ℤ)) (∏' (n : ℕ), f (-(↑n : ℤ))) / f 0

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

Premises used: HasProd.tprod_eq, Multipliable.hasProd, HasProd.of_nat_of_neg
-- 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
⊢ Multipliable f ↔
    (Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (↑n : ℤ)) ∧
      Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)

Tactic:
⟨fun p ↦ ⟨?_, ?_⟩, fun ⟨hf₁, hf₂⟩ ↦ Multipliable.of_nat_of_neg_add_one hf₁ hf₂⟩

Premises used: Multipliable.of_nat_of_neg_add_one, Int, Multipliable, _private.0.multipliable_int_iff_multipliable_nat_and_neg_add_one.match_1, And.intro, Iff.intro, SummationFilter.unconditional
-- 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
refine_1 : ∀ (p : Multipliable f), Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (↑n : ℤ)
refine_2 : ∀ (p : Multipliable f), Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
⊢ Multipliable f ↔
    (Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (↑n : ℤ)) ∧
      Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)

Tactic:
refine ⟨fun p ↦ ⟨?_, ?_⟩, fun ⟨hf₁, hf₂⟩ ↦ Multipliable.of_nat_of_neg_add_one hf₁ hf₂⟩
-- 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
p : Multipliable f
refine_1 : Injective (β := ℤ) Nat.cast
⊢ Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (↑n : ℤ)

Tactic:
apply p.comp_injective

Premises used: Multipliable.comp_injective
-- 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
p : Multipliable f
refine_2 : Injective (β := ℤ) fun (n : ℕ) ↦ -HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
⊢ Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)

Tactic:
apply p.comp_injective

Premises used: Multipliable.comp_injective
-- 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
p : Multipliable f
⊢ Injective (β := ℤ) Nat.cast

Tactic:
Nat.cast_injective

Premises used: Nat.cast_injective
-- 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
p : Multipliable f
⊢ Injective (β := ℤ) fun (n : ℕ) ↦ -HAdd.hAdd (α := ℤ) (↑n : ℤ) 1

Tactic:
@Int.negSucc.inj

Premises used: Int.negSucc.inj, Function.Injective, Int.neg, Int.negOfNat
-- 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
p : Multipliable f
⊢ Injective (β := ℤ) Nat.cast

Tactic:
exacts [Nat.cast_injective, @Int.negSucc.inj]

Premises used: Int.negSucc.inj, Nat.cast_injective
-- 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
⊢ Multipliable f ↔
    (Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (↑n : ℤ)) ∧
      Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (-(↑n : ℤ))

Tactic:
⟨fun p ↦ ⟨?_, ?_⟩, fun ⟨hf₁, hf₂⟩ ↦ Multipliable.of_nat_of_neg hf₁ hf₂⟩

Premises used: Multipliable.of_nat_of_neg, Int, Multipliable, _private.0.multipliable_int_iff_multipliable_nat_and_neg.match_1, And.intro, Iff.intro, SummationFilter.unconditional
-- 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
refine_1 : ∀ (p : Multipliable f), Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (↑n : ℤ)
refine_2 : ∀ (p : Multipliable f), Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (-(↑n : ℤ))
⊢ Multipliable f ↔
    (Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (↑n : ℤ)) ∧
      Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (-(↑n : ℤ))

Tactic:
refine ⟨fun p ↦ ⟨?_, ?_⟩, fun ⟨hf₁, hf₂⟩ ↦ Multipliable.of_nat_of_neg hf₁ hf₂⟩
-- 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
p : Multipliable f
refine_2 : Injective (β := ℤ) fun (n : ℕ) ↦ -(↑n : ℤ)
⊢ Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (-(↑n : ℤ))

Tactic:
apply p.comp_injective

Premises used: Multipliable.comp_injective
-- 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
p : Multipliable f
⊢ Injective (β := ℤ) fun (n : ℕ) ↦ -(↑n : ℤ)

Tactic:
neg_injective.comp Nat.cast_injective

Premises used: neg_injective, Function.Injective.comp, Nat.cast_injective
-- 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
p : Multipliable f
⊢ Injective (β := ℤ) Nat.cast

Tactic:
exacts [Nat.cast_injective, neg_injective.comp Nat.cast_injective]

Premises used: neg_injective, Function.Injective.comp, Nat.cast_injective
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
α : Type u_3
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsUniformAddGroup α
inst_3 : CompleteSpace α
f : ℕ → α
hf : Summable f
he : Summable.{u_3, 0} (α := α) fun (k : ℕ) ↦ HPow.hPow (α := α) (-1) (2 * k) * f (2 * k)
ho : Summable.{u_3, 0} (α := α) fun (k : ℕ) ↦ HPow.hPow (α := α) (-1) (2 * k + 1) * f (2 * k + 1)
⊢ Summable.{u_3, 0} (α := α) fun (n : ℕ) ↦ HPow.hPow (α := α) (-1) n * f n

Tactic:
apply Summable.even_add_odd

Premises used: Summable.even_add_odd
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
α : Type u_3
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsUniformAddGroup α
inst_3 : CompleteSpace α
f : ℕ → α
hf : Summable f
he : Summable.{u_3, 0} (α := α) fun (k : ℕ) ↦ f (2 * k)
⊢ Summable.{u_3, 0} (α := α) fun (k : ℕ) ↦ HPow.hPow (α := α) (-1) (2 * k) * f (2 * k)

Tactic:
simp only [even_two, Even.mul_right, Even.neg_pow, one_pow, one_mul]

Premises used: one_pow, even_two, Even.neg_pow, Even.mul_right, one_mul
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
α : Type u_3
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsUniformAddGroup α
inst_3 : CompleteSpace α
f : ℕ → α
hf : Summable f
⊢ Summable.{u_3, 0} (α := α) fun (k : ℕ) ↦ f (2 * k)

Tactic:
hf.comp_injective (mul_right_injective₀ (two_ne_zero' ℕ))

Premises used: mul_right_injective₀, two_ne_zero', Summable.comp_injective, Nat
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
α : Type u_3
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsUniformAddGroup α
inst_3 : CompleteSpace α
f : ℕ → α
hf : Summable f
⊢ Summable.{u_3, 0} (α := α) fun (k : ℕ) ↦ f (2 * k)

Tactic:
exact hf.comp_injective (mul_right_injective₀ (two_ne_zero' ℕ))

Premises used: mul_right_injective₀, two_ne_zero', Summable.comp_injective, Nat
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
α : Type u_3
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsUniformAddGroup α
inst_3 : CompleteSpace α
f : ℕ → α
hf : Summable f
ho : Summable.{u_3, 0} (α := α) fun (k : ℕ) ↦ -f (2 * k + 1)
⊢ Summable.{u_3, 0} (α := α) fun (k : ℕ) ↦ HPow.hPow (α := α) (-1) (2 * k + 1) * f (2 * k + 1)

Tactic:
simp only [pow_add, even_two, Even.mul_right, Even.neg_pow, one_pow, pow_one, mul_neg, mul_one,
      neg_mul, one_mul]

Premises used: one_pow, even_two, Even.neg_pow, pow_add, Even.mul_right, pow_one, neg_mul, mul_one, one_mul, mul_neg
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
α : Type u_3
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsUniformAddGroup α
inst_3 : CompleteSpace α
f : ℕ → α
hf : Summable f
ho : Summable.{u_3, 0} (α := α) fun (b : ℕ) ↦ f (2 * b + 1)
⊢ Summable.{u_3, 0} (α := α) fun (k : ℕ) ↦ -f (2 * k + 1)

Tactic:
apply Summable.neg

Premises used: Summable.neg
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
α : Type u_3
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsUniformAddGroup α
inst_3 : CompleteSpace α
f : ℕ → α
hf : Summable f
ho : Injective (β := ℕ) fun (b : ℕ) ↦ 2 * b + 1
⊢ Summable.{u_3, 0} (α := α) fun (b : ℕ) ↦ f (2 * b + 1)

Tactic:
apply hf.comp_injective

Premises used: Summable.comp_injective