α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
u : Finset ℤ
⊢ ∃ v,
    ∀ (v' : Finset ℕ), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∑ x in u', (f x + if x = 0 then f 0 else 0) = ∑ b in v', (f ↑b + f (-↑b))
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
⊢ HasSum (fun n => f ↑n + f (-↑n)) (a + f 0)
apply (hf.add (hasSum_ite_eq (0 : ℤ) (f 0))).hasSum_of_sum_eq fun u => ?_
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
⊢ ∃ u', u ⊆ u' ∧ ∑ x in u', (f x + if x = 0 then f 0 else 0) = ∑ b in v', (f ↑b + f (-↑b))
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
u : Finset ℤ
⊢ ∃ v,
    ∀ (v' : Finset ℕ), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∑ x in u', (f x + if x = 0 then f 0 else 0) = ∑ b in v', (f ↑b + f (-↑b))
refine' ⟨u.image Int.natAbs, fun v' hv' => _⟩
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun x => ↑x) v'
⊢ ∃ u', u ⊆ u' ∧ ∑ x in u', (f x + if x = 0 then f 0 else 0) = ∑ b in v', (f ↑b + f (-↑b))
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
⊢ ∃ u', u ⊆ u' ∧ ∑ x in u', (f x + if x = 0 then f 0 else 0) = ∑ b in v', (f ↑b + f (-↑b))
let u1 := v'.image fun x : ℕ => (x : ℤ)
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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', u ⊆ u' ∧ ∑ x in u', (f x + if x = 0 then f 0 else 0) = ∑ b in v', (f ↑b + f (-↑b))
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun x => ↑x) v'
⊢ ∃ u', u ⊆ u' ∧ ∑ x in u', (f x + if x = 0 then f 0 else 0) = ∑ b in v', (f ↑b + f (-↑b))
let u2 := v'.image fun x : ℕ => -(x : ℤ)
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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 in u1 ∪ u2, (f x + if x = 0 then f 0 else 0) = ∑ b in v', (f ↑b + f (-↑b))
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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', u ⊆ u' ∧ ∑ x in u', (f x + if x = 0 then f 0 else 0) = ∑ b in v', (f ↑b + f (-↑b))
refine' ⟨u1 ∪ u2, A, _⟩
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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
intro x hx
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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, a ∈ v' ∧ ↑a = x) ∨ ∃ a, a ∈ v' ∧ -↑a = x
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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
simp only [mem_union, mem_image, exists_prop]
case inl
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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, a ∈ v' ∧ ↑a = x) ∨ ∃ a, a ∈ v' ∧ -↑a = x

case inr
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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, a ∈ v' ∧ ↑a = x) ∨ ∃ a, a ∈ v' ∧ -↑a = x
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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, a ∈ v' ∧ ↑a = x) ∨ ∃ a, a ∈ v' ∧ -↑a = x
rcases le_total 0 x with (h'x | h'x)
case inl.h
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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, a ∈ v' ∧ ↑a = x
case inl
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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, a ∈ v' ∧ ↑a = x) ∨ ∃ a, a ∈ v' ∧ -↑a = x
left
case inl.h.refine'_1
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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
⊢ Int.natAbs x ∈ image Int.natAbs u

case inl.h.refine'_2
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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
⊢ ↑(Int.natAbs x) = x
case inl.h
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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, a ∈ v' ∧ ↑a = x
refine' ⟨Int.natAbs x, hv' _, _⟩
case inl.h.refine'_1
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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, a ∈ u ∧ Int.natAbs a = Int.natAbs x
case inl.h.refine'_1
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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
⊢ Int.natAbs x ∈ image Int.natAbs u
simp only [mem_image, exists_prop]
no goals
case inl.h.refine'_1
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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, a ∈ u ∧ Int.natAbs a = Int.natAbs x
exact ⟨x, hx, rfl⟩
no goals
case inl.h.refine'_2
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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
⊢ ↑(Int.natAbs x) = x
simp only [h'x, Int.coe_natAbs, abs_eq_self]
case inr.h
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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, a ∈ v' ∧ -↑a = x
case inr
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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, a ∈ v' ∧ ↑a = x) ∨ ∃ a, a ∈ v' ∧ -↑a = x
right
case inr.h.refine'_1
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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
⊢ Int.natAbs x ∈ image Int.natAbs u

case inr.h.refine'_2
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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
⊢ -↑(Int.natAbs x) = x
case inr.h
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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, a ∈ v' ∧ -↑a = x
refine' ⟨Int.natAbs x, hv' _, _⟩
case inr.h.refine'_1
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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, a ∈ u ∧ Int.natAbs a = Int.natAbs x
case inr.h.refine'_1
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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
⊢ Int.natAbs x ∈ image Int.natAbs u
simp only [mem_image, exists_prop]
no goals
case inr.h.refine'_1
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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, a ∈ u ∧ Int.natAbs a = Int.natAbs x
exact ⟨x, hx, rfl⟩
no goals
case inr.h.refine'_2
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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
⊢ -↑(Int.natAbs x) = x
simp only [abs_of_nonpos h'x, Int.coe_natAbs, neg_neg]
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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 in u1 ∪ u2, f x + ∑ x in u1 ∪ u2, if x = 0 then f 0 else 0) = ∑ x in u1 ∪ u2, f x + ∑ x in u1 ∩ u2, f x
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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 in u1 ∪ u2, (f x + if x = 0 then f 0 else 0) = ∑ x in u1 ∪ u2, f x + ∑ x in u1 ∩ u2, f x
rw [sum_add_distrib]
case e_a
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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 in u1 ∪ u2, if x = 0 then f 0 else 0) = ∑ x in u1 ∩ u2, f x
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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 in u1 ∪ u2, f x + ∑ x in u1 ∪ u2, if x = 0 then f 0 else 0) = ∑ x in u1 ∪ u2, f x + ∑ x in u1 ∩ u2, f x
congr 1
case e_a.refine'_1
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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 : ℤ), x ∈ (u1 ∪ u2) \ (u1 ∩ u2) → (if x = 0 then f 0 else 0) = 0

case e_a.refine'_2
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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 : ℤ), x ∈ u1 ∩ u2 → f x = if x = 0 then f 0 else 0
case e_a
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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 in u1 ∪ u2, if x = 0 then f 0 else 0) = ∑ x in u1 ∩ u2, f x
refine' (sum_subset_zero_on_sdiff inter_subset_union _ _).symm
case e_a.refine'_1
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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)
⊢ (if x = 0 then f 0 else 0) = 0
case e_a.refine'_1
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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 : ℤ), x ∈ (u1 ∪ u2) \ (u1 ∩ u2) → (if x = 0 then f 0 else 0) = 0
intro x hx
case e_a.refine'_1
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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
case e_a.refine'_1
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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)
⊢ (if x = 0 then f 0 else 0) = 0
suffices x ≠ 0 by simp only [this, if_false]
case e_a.refine'_1
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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
case e_a.refine'_1
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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
rintro rfl
no goals
case e_a.refine'_1
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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
simp at hx
no goals
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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 0) = 0
simp only [this, if_false]
case e_a.refine'_2
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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 0
case e_a.refine'_2
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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 : ℤ), x ∈ u1 ∩ u2 → f x = if x = 0 then f 0 else 0
intro x hx
case e_a.refine'_2
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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, a ∈ v' ∧ ↑a = x) ∧ ∃ a, a ∈ v' ∧ -↑a = x
⊢ f x = if x = 0 then f 0 else 0
case e_a.refine'_2
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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 0
simp only [mem_inter, mem_image, exists_prop] at hx
no goals
case e_a.refine'_2
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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, a ∈ v' ∧ ↑a = x) ∧ ∃ a, a ∈ v' ∧ -↑a = x
this : x = 0
⊢ f x = if x = 0 then f 0 else 0
simp only [this, eq_self_iff_true, if_true]
case a
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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, a ∈ v' ∧ ↑a = x) ∧ ∃ a, a ∈ v' ∧ -↑a = x
⊢ x ≤ 0

case a
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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, a ∈ v' ∧ ↑a = x) ∧ ∃ a, a ∈ v' ∧ -↑a = x
⊢ 0 ≤ x
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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, a ∈ v' ∧ ↑a = x) ∧ ∃ a, a ∈ v' ∧ -↑a = x
⊢ x = 0
apply le_antisymm
case a.intro.intro
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝¹ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a✝ : α
f : ℤ → α
hf : HasSum f a✝
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
a : ℕ
left✝ : a ∈ v'
hx : (∃ a_1, a_1 ∈ v' ∧ ↑a_1 = -↑a) ∧ ∃ a_1, a_1 ∈ v' ∧ -↑a_1 = -↑a
⊢ -↑a ≤ 0
case a
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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, a ∈ v' ∧ ↑a = x) ∧ ∃ a, a ∈ v' ∧ -↑a = x
⊢ x ≤ 0
rcases hx.2 with ⟨a, _, rfl⟩
no goals
case a.intro.intro
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝¹ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a✝ : α
f : ℤ → α
hf : HasSum f a✝
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
a : ℕ
left✝ : a ∈ v'
hx : (∃ a_1, a_1 ∈ v' ∧ ↑a_1 = -↑a) ∧ ∃ a_1, a_1 ∈ v' ∧ -↑a_1 = -↑a
⊢ -↑a ≤ 0
simp only [Right.neg_nonpos_iff, Nat.cast_nonneg]
case a.intro.intro
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝¹ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a✝ : α
f : ℤ → α
hf : HasSum f a✝
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
a : ℕ
left✝ : a ∈ v'
hx : (∃ a_1, a_1 ∈ v' ∧ ↑a_1 = ↑a) ∧ ∃ a_1, a_1 ∈ v' ∧ -↑a_1 = ↑a
⊢ 0 ≤ ↑a
case a
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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, a ∈ v' ∧ ↑a = x) ∧ ∃ a, a ∈ v' ∧ -↑a = x
⊢ 0 ≤ x
rcases hx.1 with ⟨a, _, rfl⟩
no goals
case a.intro.intro
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝¹ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a✝ : α
f : ℤ → α
hf : HasSum f a✝
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
a : ℕ
left✝ : a ∈ v'
hx : (∃ a_1, a_1 ∈ v' ∧ ↑a_1 = ↑a) ∧ ∃ a_1, a_1 ∈ v' ∧ -↑a_1 = ↑a
⊢ 0 ≤ ↑a
simp only [Nat.cast_nonneg]
no goals
α✝ : Type ?u.645559
β : Type ?u.645562
γ : Type ?u.645565
δ : Type ?u.645568
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
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 in u1, f x + ∑ x in u2, f x = ∑ b in v', f ↑b + ∑ b in v', f (-↑b)
simp