-- Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean
theorem HasProd.nat_mul_neg {f : ℤ → M} (hf : HasProd f m) :
    HasProd (fun n : ℕ ↦ f n * f (-n)) (m * f 0)

Proof state:
case e_a.refine_2
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : 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
⊢ f x = if x = 0 then f 0 else 1

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

Result:
case e_a.refine_2
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : 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
⊢ f x = if x = 0 then f 0 else 1

Proof state:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
⊢ ∃ v, ∀ (v' : Finset ℕ), v ⊆ v' → ∃ u', u ⊆ u' ∧ (∏ 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' ↦ ?_⟩

Result:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
⊢ ∃ u', u ⊆ u' ∧ (∏ x ∈ u', f x * if x = 0 then f 0 else 1) = ∏ b ∈ v', f ↑b * f (-↑b)

Proof state:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : 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 ∈ u1 ∪ u2, f x) * ∏ x ∈ u1 ∪ u2, if x = 0 then f 0 else 1) = (∏ x ∈ u1 ∪ u2, f x) * ∏ x ∈ u1 ∩ u2, f x

Tactic:
congr 1

Result:
case e_a
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : 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 ∈ u1 ∪ u2, if x = 0 then f 0 else 1) = ∏ x ∈ u1 ∩ u2, f x

Proof state:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : 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, eq_self_iff_true, if_true]

Result:
no goals

Proof state:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : 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 ∈ u1 ∪ u2, f x * if x = 0 then f 0 else 1) = (∏ x ∈ u1 ∪ u2, f x) * ∏ x ∈ u1 ∩ u2, f x

Tactic:
rw [prod_mul_distrib]

Result:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : 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 ∈ u1 ∪ u2, f x) * ∏ x ∈ u1 ∪ u2, if x = 0 then f 0 else 1) = (∏ x ∈ u1 ∪ u2, f x) * ∏ x ∈ u1 ∩ u2, f x

Proof state:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : 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
⊢ x ∈ u1 ∪ u2

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

Result:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : 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
⊢ (∃ a ∈ v', ↑a = x) ∨ ∃ a ∈ v', -↑a = x

Proof state:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : 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 ∈ u1, f x) * ∏ x ∈ u2, f x = (∏ b ∈ v', f ↑b) * ∏ b ∈ v', f (-↑b)

Tactic:
simp only [u1, u2, Nat.cast_inj, imp_self, implies_true, forall_const, prod_image, neg_inj]

Result:
no goals

Proof state:
case e_a.refine_1
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : 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)
⊢ x ≠ 0

Tactic:
rintro rfl

Result:
case e_a.refine_1
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : 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

Proof state:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : 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
⊢ (∃ a ∈ v', ↑a = x) ∨ ∃ a ∈ v', -↑a = x

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

Result:
case inl
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : 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

case inr
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : 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

Proof state:
case inl
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : 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:
refine Or.inl ⟨_, hv' <| mem_image.mpr ⟨x, hx, rfl⟩, ?_⟩

Result:
case inl
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : 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