α : Type u_1
β : Type ?u.477720
γ : Type ?u.477723
δ : Type ?u.477726
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g : β → α
a a₁ a₂ b : α
f : ℤ → α
hnonneg : HasSum (fun n => f ↑n) a
hneg : HasSum (fun n => f (Int.negSucc n)) b
⊢ HasSum f (a + b)
α : Type u_1
β : Type ?u.477720
γ : Type ?u.477723
δ : Type ?u.477726
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g : β → α
a a₁ a₂ b : α
f : ℤ → α
hnonneg : HasSum (fun n => f ↑n) a
hneg : HasSum (fun n => f (-↑(Nat.succ n))) b
⊢ HasSum f (a + b)
simp_rw [← Int.negSucc_coe] at hneg
case h.e'_5
α : Type u_1
β : Type ?u.477720
γ : Type ?u.477723
δ : Type ?u.477726
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g : β → α
a a₁ a₂ b : α
f : ℤ → α
hnonneg : HasSum (fun n => f ↑n) a
hneg : HasSum (fun n => f (Int.negSucc n)) b
⊢ f = Int.rec (fun n => f ↑n) fun n => f (Int.negSucc n)
α : Type u_1
β : Type ?u.477720
γ : Type ?u.477723
δ : Type ?u.477726
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g : β → α
a a₁ a₂ b : α
f : ℤ → α
hnonneg : HasSum (fun n => f ↑n) a
hneg : HasSum (fun n => f (Int.negSucc n)) b
⊢ HasSum f (a + b)
convert hnonneg.int_rec hneg using 1
no goals
case h.e'_5
α : Type u_1
β : Type ?u.477720
γ : Type ?u.477723
δ : Type ?u.477726
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g : β → α
a a₁ a₂ b : α
f : ℤ → α
hnonneg : HasSum (fun n => f ↑n) a
hneg : HasSum (fun n => f (Int.negSucc n)) b
⊢ f = Int.rec (fun n => f ↑n) fun n => f (Int.negSucc n)
ext (i | j) <;> rfl