[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f g : β → α
a b : α
s : Finset β
⊢ HasSum (fun x => 0) 0
[PROOFSTEP]
simp [HasSum, tendsto_const_nhds]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a b : α
s : Finset β
inst✝ : IsEmpty β
⊢ HasSum f 0
[PROOFSTEP]
convert @hasSum_zero α β _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f g : β → α
a b : α
s : Finset β
h : ¬Summable f
⊢ ∑' (b : β), f b = 0
[PROOFSTEP]
simp [tsum_def, h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f g✝ : β → α
a b : α
s : Finset β
g : γ → β
hg : Injective g
hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 0
⊢ HasSum (f ∘ g) a ↔ HasSum f a
[PROOFSTEP]
simp only [HasSum, Tendsto, comp_apply, hg.map_atTop_finset_sum_eq hf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f g✝ : β → α
a b : α
s : Finset β
g : β → γ
hg : Injective g
⊢ HasSum (extend g f 0) a ↔ HasSum f a
[PROOFSTEP]
rw [← hg.hasSum_iff, extend_comp hg]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f g✝ : β → α
a b : α
s : Finset β
g : β → γ
hg : Injective g
⊢ ∀ (x : γ), ¬x ∈ Set.range g → extend g f 0 x = 0
[PROOFSTEP]
exact extend_apply' _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f g : β → α
a b : α
s✝ : Finset β
s : Set β
hf : support f ⊆ s
⊢ ∀ (x : β), (¬x ∈ Set.range fun a => ↑a) → f x = 0
[PROOFSTEP]
simpa using support_subset_iff'.1 hf
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f g : β → α
a b : α
s✝ : Finset β
s : Set β
⊢ HasSum (f ∘ Subtype.val) a ↔ HasSum (Set.indicator s f) a
[PROOFSTEP]
rw [← Set.indicator_range_comp, Subtype.range_coe, hasSum_subtype_iff_of_support_subset Set.support_indicator_subset]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f✝ g : β → α
a b : α
s✝ s : Finset β
f : β → α
⊢ HasSum (f ∘ Subtype.val) (∑ b in s, f b)
[PROOFSTEP]
rw [← sum_attach]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f✝ g : β → α
a b : α
s✝ s : Finset β
f : β → α
⊢ HasSum (f ∘ Subtype.val) (∑ x in attach s, f ↑x)
[PROOFSTEP]
exact hasSum_fintype _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f✝ g : β → α
a b : α
s✝ : Finset β
s : Set β
hs : Set.Finite s
f : β → α
⊢ Summable (f ∘ Subtype.val)
[PROOFSTEP]
have := hs.toFinset.summable f
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f✝ g : β → α
a b : α
s✝ : Finset β
s : Set β
hs : Set.Finite s
f : β → α
this : Summable (f ∘ Subtype.val)
⊢ Summable (f ∘ Subtype.val)
[PROOFSTEP]
rwa [hs.coe_toFinset] at this 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f g : β → α
a b : α
s : Finset β
h : Set.Finite (support f)
⊢ Summable f
[PROOFSTEP]
apply summable_of_ne_finset_zero (s := h.toFinset)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f g : β → α
a b : α
s : Finset β
h : Set.Finite (support f)
⊢ ∀ (b : β), ¬b ∈ Set.Finite.toFinset h → f b = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f g : β → α
a b : α
s : Finset β
ha : Summable f
⊢ HasSum f (∑' (b : β), f b)
[PROOFSTEP]
simp only [tsum_def, ha, dite_true]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f g : β → α
a b : α
s : Finset β
ha : Summable f
⊢ HasSum f (if Set.Finite (support fun b => f b) then ∑ᶠ (b : β), f b else Classical.choose (_ : Summable fun b => f b))
[PROOFSTEP]
by_cases H : (support f).Finite
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f g : β → α
a b : α
s : Finset β
ha : Summable f
H : Set.Finite (support f)
⊢ HasSum f (if Set.Finite (support fun b => f b) then ∑ᶠ (b : β), f b else Classical.choose (_ : Summable fun b => f b))
[PROOFSTEP]
simp [H, hasSum_sum_of_ne_finset_zero, finsum_eq_sum]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f g : β → α
a b : α
s : Finset β
ha : Summable f
H : ¬Set.Finite (support f)
⊢ HasSum f (if Set.Finite (support fun b => f b) then ∑ᶠ (b : β), f b else Classical.choose (_ : Summable fun b => f b))
[PROOFSTEP]
simpa [H] using Classical.choose_spec ha
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f✝ g : β → α
a b✝ : α
s : Finset β
f : β → α
b : β
hf : ∀ (b' : β), b' ≠ b → f b' = 0
⊢ ∀ (b_1 : β), ¬b_1 ∈ {b} → f b_1 = 0
[PROOFSTEP]
simpa [hf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f✝ g : β → α
a b✝ : α
s : Finset β
f : β → α
b : β
hf : ∀ (b' : β), b' ≠ b → f b' = 0
this : HasSum f (∑ b' in {b}, f b')
⊢ HasSum f (f b)
[PROOFSTEP]
simpa using this
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a✝ b✝ : α
s : Finset β
b : β
inst✝ : DecidablePred fun x => x = b
a : α
⊢ HasSum (fun b' => if b' = b then a else 0) a
[PROOFSTEP]
convert @hasSum_single _ _ _ _ (fun b' => if b' = b then a else 0) b (fun b' hb' => if_neg hb')
[GOAL]
case h.e'_6
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a✝ b✝ : α
s : Finset β
b : β
inst✝ : DecidablePred fun x => x = b
a : α
⊢ a = if b = b then a else 0
[PROOFSTEP]
exact (if_pos rfl).symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a✝ b✝ : α
s : Finset β
inst✝ : DecidableEq β
b : β
a : α
⊢ HasSum (Pi.single b a) a
[PROOFSTEP]
convert hasSum_ite_eq b a
[GOAL]
case h.e'_5.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a✝ b✝ : α
s : Finset β
inst✝ : DecidableEq β
b : β
a : α
x✝ : β
⊢ Pi.single b a x✝ = if x✝ = b then a else 0
[PROOFSTEP]
simp [Pi.single_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f g : β → α
a b : α
s : Finset β
e : γ ≃ β
⊢ ∀ (x : β), ¬x ∈ Set.range ↑e → f x = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f g✝ : β → α
a b : α
s : Finset β
g : γ → α
e : ↑(support f) ≃ ↑(support g)
he : ∀ (x : ↑(support f)), g ↑(↑e x) = f ↑x
⊢ HasSum f a ↔ HasSum g a
[PROOFSTEP]
have : (g ∘ (↑)) ∘ e = f ∘ (↑) := funext he
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f g✝ : β → α
a b : α
s : Finset β
g : γ → α
e : ↑(support f) ≃ ↑(support g)
he : ∀ (x : ↑(support f)), g ↑(↑e x) = f ↑x
this : (g ∘ Subtype.val) ∘ ↑e = f ∘ Subtype.val
⊢ HasSum f a ↔ HasSum g a
[PROOFSTEP]
rw [← hasSum_subtype_support, ← this, e.hasSum_iff, hasSum_subtype_support]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : AddCommMonoid α
inst✝⁴ : TopologicalSpace α
f g✝ : β → α
a b : α
s : Finset β
inst✝³ : AddCommMonoid γ
inst✝² : TopologicalSpace γ
G : Type u_5
G' : Type u_6
inst✝¹ : AddMonoidHomClass G α γ
inst✝ : AddMonoidHomClass G' γ α
g : G
g' : G'
hg : Continuous ↑g
hg' : Continuous ↑g'
hinv : LeftInverse ↑g' ↑g
h : Summable (↑g ∘ f)
⊢ Summable f
[PROOFSTEP]
have := h.map _ hg'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : AddCommMonoid α
inst✝⁴ : TopologicalSpace α
f g✝ : β → α
a b : α
s : Finset β
inst✝³ : AddCommMonoid γ
inst✝² : TopologicalSpace γ
G : Type u_5
G' : Type u_6
inst✝¹ : AddMonoidHomClass G α γ
inst✝ : AddMonoidHomClass G' γ α
g : G
g' : G'
hg : Continuous ↑g
hg' : Continuous ↑g'
hinv : LeftInverse ↑g' ↑g
h : Summable (↑g ∘ f)
this : Summable (↑g' ∘ ↑g ∘ f)
⊢ Summable f
[PROOFSTEP]
rwa [← Function.comp.assoc, hinv.id] at this 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f✝ g : β → α
a✝ b : α
s : Finset β
inst✝ : T2Space α
f : ℕ → α
a : α
hf : Summable f
⊢ HasSum f a ↔ Tendsto (fun n => ∑ i in range n, f i) atTop (𝓝 a)
[PROOFSTEP]
refine' ⟨fun h => h.tendsto_sum_nat, fun h => _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f✝ g : β → α
a✝ b : α
s : Finset β
inst✝ : T2Space α
f : ℕ → α
a : α
hf : Summable f
h : Tendsto (fun n => ∑ i in range n, f i) atTop (𝓝 a)
⊢ HasSum f a
[PROOFSTEP]
rw [tendsto_nhds_unique h hf.hasSum.tendsto_sum_nat]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f✝ g : β → α
a✝ b : α
s : Finset β
inst✝ : T2Space α
f : ℕ → α
a : α
hf : Summable f
h : Tendsto (fun n => ∑ i in range n, f i) atTop (𝓝 a)
⊢ HasSum f (∑' (b : ℕ), f b)
[PROOFSTEP]
exact hf.hasSum
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a b : α
s : Finset β
inst✝ : ContinuousAdd α
hf : HasSum f a
hg : HasSum g b
⊢ HasSum (fun b => f b + g b) (a + b)
[PROOFSTEP]
dsimp only [HasSum] at hf hg ⊢
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a b : α
s : Finset β
inst✝ : ContinuousAdd α
hf : Tendsto (fun s => ∑ b in s, f b) atTop (𝓝 a)
hg : Tendsto (fun s => ∑ b in s, g b) atTop (𝓝 b)
⊢ Tendsto (fun s => ∑ b in s, (f b + g b)) atTop (𝓝 (a + b))
[PROOFSTEP]
simp_rw [sum_add_distrib]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a b : α
s : Finset β
inst✝ : ContinuousAdd α
hf : Tendsto (fun s => ∑ b in s, f b) atTop (𝓝 a)
hg : Tendsto (fun s => ∑ b in s, g b) atTop (𝓝 b)
⊢ Tendsto (fun s => ∑ x in s, f x + ∑ x in s, g x) atTop (𝓝 (a + b))
[PROOFSTEP]
exact hf.add hg
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f✝ g : β → α
a✝ b : α
s✝ : Finset β
inst✝ : ContinuousAdd α
f : γ → β → α
a : γ → α
s : Finset γ
⊢ (∀ (i : γ), i ∈ ∅ → HasSum (f i) (a i)) → HasSum (fun b => ∑ i in ∅, f i b) (∑ i in ∅, a i)
[PROOFSTEP]
simp only [hasSum_zero, sum_empty, forall_true_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f✝ g : β → α
a✝ b : α
s✝ : Finset β
inst✝ : ContinuousAdd α
f : γ → β → α
a : γ → α
s : Finset γ
⊢ ∀ ⦃a_1 : γ⦄ {s : Finset γ},
    ¬a_1 ∈ s →
      ((∀ (i : γ), i ∈ s → HasSum (f i) (a i)) → HasSum (fun b => ∑ i in s, f i b) (∑ i in s, a i)) →
        (∀ (i : γ), i ∈ insert a_1 s → HasSum (f i) (a i)) →
          HasSum (fun b => ∑ i in insert a_1 s, f i b) (∑ i in insert a_1 s, a i)
[PROOFSTEP]
simp (config := { contextual := true }) only [mem_insert, forall_eq_or_imp, not_false_iff, sum_insert, and_imp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f✝ g : β → α
a✝ b : α
s✝ : Finset β
inst✝ : ContinuousAdd α
f : γ → β → α
a : γ → α
s : Finset γ
⊢ ∀ ⦃a_1 : γ⦄ {s : Finset γ},
    ¬a_1 ∈ s →
      ((∀ (i : γ), i ∈ s → HasSum (f i) (a i)) → HasSum (fun b => ∑ i in s, f i b) (∑ i in s, a i)) →
        HasSum (f a_1) (a a_1) →
          (∀ (a_5 : γ), a_5 ∈ s → HasSum (f a_5) (a a_5)) →
            HasSum (fun b => f a_1 b + ∑ i in s, f i b) (a a_1 + ∑ i in s, a i)
[PROOFSTEP]
exact fun x s _ IH hx h ↦ hx.add (IH h)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a b : α
s✝ : Finset β
inst✝ : ContinuousAdd α
s t : Set β
hs : Disjoint s t
ha : HasSum (f ∘ Subtype.val) a
hb : HasSum (f ∘ Subtype.val) b
⊢ HasSum (f ∘ Subtype.val) (a + b)
[PROOFSTEP]
rw [hasSum_subtype_iff_indicator] at *
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a b : α
s✝ : Finset β
inst✝ : ContinuousAdd α
s t : Set β
hs : Disjoint s t
ha : HasSum (Set.indicator s f) a
hb : HasSum (Set.indicator t f) b
⊢ HasSum (Set.indicator (s ∪ t) f) (a + b)
[PROOFSTEP]
rw [Set.indicator_union_of_disjoint hs]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a b : α
s✝ : Finset β
inst✝ : ContinuousAdd α
s t : Set β
hs : Disjoint s t
ha : HasSum (Set.indicator s f) a
hb : HasSum (Set.indicator t f) b
⊢ HasSum (fun a => Set.indicator s f a + Set.indicator t f a) (a + b)
[PROOFSTEP]
exact ha.add hb
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a✝ b : α
s✝ : Finset β
inst✝ : ContinuousAdd α
ι : Type u_5
s : Finset ι
t : ι → Set β
a : ι → α
hs : Set.Pairwise (↑s) (Disjoint on t)
hf : ∀ (i : ι), i ∈ s → HasSum (f ∘ Subtype.val) (a i)
⊢ HasSum (f ∘ Subtype.val) (∑ i in s, a i)
[PROOFSTEP]
simp_rw [hasSum_subtype_iff_indicator] at *
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a✝ b : α
s✝ : Finset β
inst✝ : ContinuousAdd α
ι : Type u_5
s : Finset ι
t : ι → Set β
a : ι → α
hs : Set.Pairwise (↑s) (Disjoint on t)
hf : ∀ (i : ι), i ∈ s → HasSum (Set.indicator (t i) f) (a i)
⊢ HasSum (Set.indicator (⋃ (i : ι) (_ : i ∈ s), t i) f) (∑ i in s, a i)
[PROOFSTEP]
rw [Set.indicator_finset_biUnion _ _ hs]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a✝ b : α
s✝ : Finset β
inst✝ : ContinuousAdd α
ι : Type u_5
s : Finset ι
t : ι → Set β
a : ι → α
hs : Set.Pairwise (↑s) (Disjoint on t)
hf : ∀ (i : ι), i ∈ s → HasSum (Set.indicator (t i) f) (a i)
⊢ HasSum (fun a => ∑ i in s, Set.indicator (t i) f a) (∑ i in s, a i)
[PROOFSTEP]
exact hasSum_sum hf
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a b : α
s✝ : Finset β
inst✝ : ContinuousAdd α
s t : Set β
hs : IsCompl s t
ha : HasSum (f ∘ Subtype.val) a
hb : HasSum (f ∘ Subtype.val) b
⊢ HasSum f (a + b)
[PROOFSTEP]
simpa [← hs.compl_eq] using (hasSum_subtype_iff_indicator.1 ha).add (hasSum_subtype_iff_indicator.1 hb)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f✝ g : β → α
a b : α
s : Finset β
inst✝ : ContinuousAdd α
f : ℕ → α
he : HasSum (fun k => f (2 * k)) a
ho : HasSum (fun k => f (2 * k + 1)) b
⊢ HasSum f (a + b)
[PROOFSTEP]
have := mul_right_injective₀ (two_ne_zero' ℕ)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f✝ g : β → α
a b : α
s : Finset β
inst✝ : ContinuousAdd α
f : ℕ → α
he : HasSum (fun k => f (2 * k)) a
ho : HasSum (fun k => f (2 * k + 1)) b
this : Injective ((fun x x_1 => x * x_1) 2)
⊢ HasSum f (a + b)
[PROOFSTEP]
replace he := this.hasSum_range_iff.2 he
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f✝ g : β → α
a b : α
s : Finset β
inst✝ : ContinuousAdd α
f : ℕ → α
ho : HasSum (fun k => f (2 * k + 1)) b
this : Injective ((fun x x_1 => x * x_1) 2)
he : HasSum (fun x => f ↑x) a
⊢ HasSum f (a + b)
[PROOFSTEP]
replace ho := ((add_left_injective 1).comp this).hasSum_range_iff.2 ho
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f✝ g : β → α
a b : α
s : Finset β
inst✝ : ContinuousAdd α
f : ℕ → α
this : Injective ((fun x x_1 => x * x_1) 2)
he : HasSum (fun x => f ↑x) a
ho : HasSum (fun x => f ↑x) b
⊢ HasSum f (a + b)
[PROOFSTEP]
refine' he.add_isCompl _ ho
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f✝ g : β → α
a b : α
s : Finset β
inst✝ : ContinuousAdd α
f : ℕ → α
this : Injective ((fun x x_1 => x * x_1) 2)
he : HasSum (fun x => f ↑x) a
ho : HasSum (fun x => f ↑x) b
⊢ IsCompl (Set.range ((fun x x_1 => x * x_1) 2)) (Set.range ((fun x => x + 1) ∘ (fun x x_1 => x * x_1) 2))
[PROOFSTEP]
simpa [(· ∘ ·)] using Nat.isCompl_even_odd
[GOAL]
α : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
f✝ g✝ : β → α
a✝ b : α
s : Finset β
inst✝¹ : ContinuousAdd α
inst✝ : RegularSpace α
γ : β → Type u_5
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasSum f a
hf : ∀ (b : β), HasSum (fun c => f { fst := b, snd := c }) (g b)
⊢ HasSum g a
[PROOFSTEP]
refine' (atTop_basis.tendsto_iff (closed_nhds_basis a)).mpr _
[GOAL]
α : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
f✝ g✝ : β → α
a✝ b : α
s : Finset β
inst✝¹ : ContinuousAdd α
inst✝ : RegularSpace α
γ : β → Type u_5
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasSum f a
hf : ∀ (b : β), HasSum (fun c => f { fst := b, snd := c }) (g b)
⊢ ∀ (ib : Set α), ib ∈ 𝓝 a ∧ IsClosed ib → ∃ ia, True ∧ ∀ (x : Finset β), x ∈ Set.Ici ia → ∑ b in x, g b ∈ id ib
[PROOFSTEP]
rintro s ⟨hs, hsc⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
f✝ g✝ : β → α
a✝ b : α
s✝ : Finset β
inst✝¹ : ContinuousAdd α
inst✝ : RegularSpace α
γ : β → Type u_5
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasSum f a
hf : ∀ (b : β), HasSum (fun c => f { fst := b, snd := c }) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed s
⊢ ∃ ia, True ∧ ∀ (x : Finset β), x ∈ Set.Ici ia → ∑ b in x, g b ∈ id s
[PROOFSTEP]
rcases mem_atTop_sets.mp (ha hs) with ⟨u, hu⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
f✝ g✝ : β → α
a✝ b : α
s✝ : Finset β
inst✝¹ : ContinuousAdd α
inst✝ : RegularSpace α
γ : β → Type u_5
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasSum f a
hf : ∀ (b : β), HasSum (fun c => f { fst := b, snd := c }) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed s
u : Finset ((b : β) × γ b)
hu : ∀ (b : Finset ((b : β) × γ b)), b ≥ u → b ∈ (fun s => ∑ b in s, f b) ⁻¹' s
⊢ ∃ ia, True ∧ ∀ (x : Finset β), x ∈ Set.Ici ia → ∑ b in x, g b ∈ id s
[PROOFSTEP]
use u.image Sigma.fst, trivial
[GOAL]
case right
α : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
f✝ g✝ : β → α
a✝ b : α
s✝ : Finset β
inst✝¹ : ContinuousAdd α
inst✝ : RegularSpace α
γ : β → Type u_5
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasSum f a
hf : ∀ (b : β), HasSum (fun c => f { fst := b, snd := c }) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed s
u : Finset ((b : β) × γ b)
hu : ∀ (b : Finset ((b : β) × γ b)), b ≥ u → b ∈ (fun s => ∑ b in s, f b) ⁻¹' s
⊢ ∀ (x : Finset β), x ∈ Set.Ici (image Sigma.fst u) → ∑ b in x, g b ∈ id s
[PROOFSTEP]
intro bs hbs
[GOAL]
case right
α : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
f✝ g✝ : β → α
a✝ b : α
s✝ : Finset β
inst✝¹ : ContinuousAdd α
inst✝ : RegularSpace α
γ : β → Type u_5
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasSum f a
hf : ∀ (b : β), HasSum (fun c => f { fst := b, snd := c }) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed s
u : Finset ((b : β) × γ b)
hu : ∀ (b : Finset ((b : β) × γ b)), b ≥ u → b ∈ (fun s => ∑ b in s, f b) ⁻¹' s
bs : Finset β
hbs : bs ∈ Set.Ici (image Sigma.fst u)
⊢ ∑ b in bs, g b ∈ id s
[PROOFSTEP]
simp only [Set.mem_preimage, ge_iff_le, Finset.le_iff_subset] at hu 
[GOAL]
case right
α : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
f✝ g✝ : β → α
a✝ b : α
s✝ : Finset β
inst✝¹ : ContinuousAdd α
inst✝ : RegularSpace α
γ : β → Type u_5
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasSum f a
hf : ∀ (b : β), HasSum (fun c => f { fst := b, snd := c }) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed s
u : Finset ((b : β) × γ b)
bs : Finset β
hbs : bs ∈ Set.Ici (image Sigma.fst u)
hu : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → ∑ b in b, f b ∈ s
⊢ ∑ b in bs, g b ∈ id s
[PROOFSTEP]
have : Tendsto (fun t : Finset (Σ b, γ b) => ∑ p in t.filter fun p => p.1 ∈ bs, f p) atTop (𝓝 <| ∑ b in bs, g b) :=
  by
  simp only [← sigma_preimage_mk, sum_sigma]
  refine' tendsto_finset_sum _ fun b _ => _
  change Tendsto (fun t => (fun t => ∑ s in t, f ⟨b, s⟩) (preimage t (Sigma.mk b) _)) atTop (𝓝 (g b))
  exact (hf b).comp (tendsto_finset_preimage_atTop_atTop (sigma_mk_injective))
[GOAL]
α : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
f✝ g✝ : β → α
a✝ b : α
s✝ : Finset β
inst✝¹ : ContinuousAdd α
inst✝ : RegularSpace α
γ : β → Type u_5
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasSum f a
hf : ∀ (b : β), HasSum (fun c => f { fst := b, snd := c }) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed s
u : Finset ((b : β) × γ b)
bs : Finset β
hbs : bs ∈ Set.Ici (image Sigma.fst u)
hu : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → ∑ b in b, f b ∈ s
⊢ Tendsto (fun t => ∑ p in filter (fun p => p.fst ∈ bs) t, f p) atTop (𝓝 (∑ b in bs, g b))
[PROOFSTEP]
simp only [← sigma_preimage_mk, sum_sigma]
[GOAL]
α : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
f✝ g✝ : β → α
a✝ b : α
s✝ : Finset β
inst✝¹ : ContinuousAdd α
inst✝ : RegularSpace α
γ : β → Type u_5
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasSum f a
hf : ∀ (b : β), HasSum (fun c => f { fst := b, snd := c }) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed s
u : Finset ((b : β) × γ b)
bs : Finset β
hbs : bs ∈ Set.Ici (image Sigma.fst u)
hu : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → ∑ b in b, f b ∈ s
⊢ Tendsto
    (fun t =>
      ∑ a in bs,
        ∑ s in preimage t (Sigma.mk a) (_ : Set.InjOn (Sigma.mk a) (Sigma.mk a ⁻¹' ↑t)), f { fst := a, snd := s })
    atTop (𝓝 (∑ b in bs, g b))
[PROOFSTEP]
refine' tendsto_finset_sum _ fun b _ => _
[GOAL]
α : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
f✝ g✝ : β → α
a✝ b✝ : α
s✝ : Finset β
inst✝¹ : ContinuousAdd α
inst✝ : RegularSpace α
γ : β → Type u_5
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasSum f a
hf : ∀ (b : β), HasSum (fun c => f { fst := b, snd := c }) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed s
u : Finset ((b : β) × γ b)
bs : Finset β
hbs : bs ∈ Set.Ici (image Sigma.fst u)
hu : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → ∑ b in b, f b ∈ s
b : β
x✝ : b ∈ bs
⊢ Tendsto
    (fun t => ∑ s in preimage t (Sigma.mk b) (_ : Set.InjOn (Sigma.mk b) (Sigma.mk b ⁻¹' ↑t)), f { fst := b, snd := s })
    atTop (𝓝 (g b))
[PROOFSTEP]
change Tendsto (fun t => (fun t => ∑ s in t, f ⟨b, s⟩) (preimage t (Sigma.mk b) _)) atTop (𝓝 (g b))
[GOAL]
α : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
f✝ g✝ : β → α
a✝ b✝ : α
s✝ : Finset β
inst✝¹ : ContinuousAdd α
inst✝ : RegularSpace α
γ : β → Type u_5
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasSum f a
hf : ∀ (b : β), HasSum (fun c => f { fst := b, snd := c }) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed s
u : Finset ((b : β) × γ b)
bs : Finset β
hbs : bs ∈ Set.Ici (image Sigma.fst u)
hu : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → ∑ b in b, f b ∈ s
b : β
x✝ : b ∈ bs
⊢ Tendsto
    (fun t =>
      (fun t => ∑ s in t, f { fst := b, snd := s })
        (preimage t (Sigma.mk b) (_ : Set.InjOn (Sigma.mk b) (Sigma.mk b ⁻¹' ↑t))))
    atTop (𝓝 (g b))
[PROOFSTEP]
exact (hf b).comp (tendsto_finset_preimage_atTop_atTop (sigma_mk_injective))
[GOAL]
case right
α : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
f✝ g✝ : β → α
a✝ b : α
s✝ : Finset β
inst✝¹ : ContinuousAdd α
inst✝ : RegularSpace α
γ : β → Type u_5
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasSum f a
hf : ∀ (b : β), HasSum (fun c => f { fst := b, snd := c }) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed s
u : Finset ((b : β) × γ b)
bs : Finset β
hbs : bs ∈ Set.Ici (image Sigma.fst u)
hu : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → ∑ b in b, f b ∈ s
this : Tendsto (fun t => ∑ p in filter (fun p => p.fst ∈ bs) t, f p) atTop (𝓝 (∑ b in bs, g b))
⊢ ∑ b in bs, g b ∈ id s
[PROOFSTEP]
refine' hsc.mem_of_tendsto this (eventually_atTop.2 ⟨u, fun t ht => hu _ fun x hx => _⟩)
[GOAL]
case right
α : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
f✝ g✝ : β → α
a✝ b : α
s✝ : Finset β
inst✝¹ : ContinuousAdd α
inst✝ : RegularSpace α
γ : β → Type u_5
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasSum f a
hf : ∀ (b : β), HasSum (fun c => f { fst := b, snd := c }) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed s
u : Finset ((b : β) × γ b)
bs : Finset β
hbs : bs ∈ Set.Ici (image Sigma.fst u)
hu : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → ∑ b in b, f b ∈ s
this : Tendsto (fun t => ∑ p in filter (fun p => p.fst ∈ bs) t, f p) atTop (𝓝 (∑ b in bs, g b))
t : Finset ((b : β) × γ b)
ht : t ≥ u
x : (b : β) × γ b
hx : x ∈ u
⊢ x ∈ filter (fun p => p.fst ∈ bs) t
[PROOFSTEP]
exact mem_filter.2 ⟨ht hx, hbs <| mem_image_of_mem _ hx⟩
[GOAL]
α : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
f✝ g✝ : β → α
a✝ b : α
s : Finset β
inst✝¹ : ContinuousAdd α
inst✝ : T3Space α
γ : β → Type u_5
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasSum g a
hf : ∀ (b : β), HasSum (fun c => f { fst := b, snd := c }) (g b)
hf' : Summable f
⊢ HasSum f a
[PROOFSTEP]
simpa [(hf'.hasSum.sigma hf).unique ha] using hf'.hasSum
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : AddCommMonoid α✝
inst✝⁵ : TopologicalSpace α✝
f✝ g : β✝ → α✝
a✝ b✝ : α✝
s : Finset β✝
inst✝⁴ : ContinuousAdd α✝
α : Type u_5
β : Type u_6
inst✝³ : TopologicalSpace α
inst✝² : AddCommMonoid α
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
f : β → α
a a' : α
hf : HasSum f a
b : β
x : α
hf' : HasSum (update f b x) a'
⊢ a + x = a' + f b
[PROOFSTEP]
have : ∀ b', f b' + ite (b' = b) x 0 = update f b x b' + ite (b' = b) (f b) 0 :=
  by
  intro b'
  split_ifs with hb'
  · simpa only [Function.update_apply, hb', eq_self_iff_true] using add_comm (f b) x
  · simp only [Function.update_apply, hb', if_false]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : AddCommMonoid α✝
inst✝⁵ : TopologicalSpace α✝
f✝ g : β✝ → α✝
a✝ b✝ : α✝
s : Finset β✝
inst✝⁴ : ContinuousAdd α✝
α : Type u_5
β : Type u_6
inst✝³ : TopologicalSpace α
inst✝² : AddCommMonoid α
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
f : β → α
a a' : α
hf : HasSum f a
b : β
x : α
hf' : HasSum (update f b x) a'
⊢ ∀ (b' : β), (f b' + if b' = b then x else 0) = update f b x b' + if b' = b then f b else 0
[PROOFSTEP]
intro b'
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : AddCommMonoid α✝
inst✝⁵ : TopologicalSpace α✝
f✝ g : β✝ → α✝
a✝ b✝ : α✝
s : Finset β✝
inst✝⁴ : ContinuousAdd α✝
α : Type u_5
β : Type u_6
inst✝³ : TopologicalSpace α
inst✝² : AddCommMonoid α
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
f : β → α
a a' : α
hf : HasSum f a
b : β
x : α
hf' : HasSum (update f b x) a'
b' : β
⊢ (f b' + if b' = b then x else 0) = update f b x b' + if b' = b then f b else 0
[PROOFSTEP]
split_ifs with hb'
[GOAL]
case pos
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : AddCommMonoid α✝
inst✝⁵ : TopologicalSpace α✝
f✝ g : β✝ → α✝
a✝ b✝ : α✝
s : Finset β✝
inst✝⁴ : ContinuousAdd α✝
α : Type u_5
β : Type u_6
inst✝³ : TopologicalSpace α
inst✝² : AddCommMonoid α
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
f : β → α
a a' : α
hf : HasSum f a
b : β
x : α
hf' : HasSum (update f b x) a'
b' : β
hb' : b' = b
⊢ f b' + x = update f b x b' + f b
[PROOFSTEP]
simpa only [Function.update_apply, hb', eq_self_iff_true] using add_comm (f b) x
[GOAL]
case neg
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : AddCommMonoid α✝
inst✝⁵ : TopologicalSpace α✝
f✝ g : β✝ → α✝
a✝ b✝ : α✝
s : Finset β✝
inst✝⁴ : ContinuousAdd α✝
α : Type u_5
β : Type u_6
inst✝³ : TopologicalSpace α
inst✝² : AddCommMonoid α
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
f : β → α
a a' : α
hf : HasSum f a
b : β
x : α
hf' : HasSum (update f b x) a'
b' : β
hb' : ¬b' = b
⊢ f b' + 0 = update f b x b' + 0
[PROOFSTEP]
simp only [Function.update_apply, hb', if_false]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : AddCommMonoid α✝
inst✝⁵ : TopologicalSpace α✝
f✝ g : β✝ → α✝
a✝ b✝ : α✝
s : Finset β✝
inst✝⁴ : ContinuousAdd α✝
α : Type u_5
β : Type u_6
inst✝³ : TopologicalSpace α
inst✝² : AddCommMonoid α
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
f : β → α
a a' : α
hf : HasSum f a
b : β
x : α
hf' : HasSum (update f b x) a'
this : ∀ (b' : β), (f b' + if b' = b then x else 0) = update f b x b' + if b' = b then f b else 0
⊢ a + x = a' + f b
[PROOFSTEP]
have h := hf.add (hasSum_ite_eq b x)
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : AddCommMonoid α✝
inst✝⁵ : TopologicalSpace α✝
f✝ g : β✝ → α✝
a✝ b✝ : α✝
s : Finset β✝
inst✝⁴ : ContinuousAdd α✝
α : Type u_5
β : Type u_6
inst✝³ : TopologicalSpace α
inst✝² : AddCommMonoid α
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
f : β → α
a a' : α
hf : HasSum f a
b : β
x : α
hf' : HasSum (update f b x) a'
this : ∀ (b' : β), (f b' + if b' = b then x else 0) = update f b x b' + if b' = b then f b else 0
h : HasSum (fun b_1 => f b_1 + if b_1 = b then x else 0) (a + x)
⊢ a + x = a' + f b
[PROOFSTEP]
simp_rw [this] at h 
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : AddCommMonoid α✝
inst✝⁵ : TopologicalSpace α✝
f✝ g : β✝ → α✝
a✝ b✝ : α✝
s : Finset β✝
inst✝⁴ : ContinuousAdd α✝
α : Type u_5
β : Type u_6
inst✝³ : TopologicalSpace α
inst✝² : AddCommMonoid α
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
f : β → α
a a' : α
hf : HasSum f a
b : β
x : α
hf' : HasSum (update f b x) a'
this : ∀ (b' : β), (f b' + if b' = b then x else 0) = update f b x b' + if b' = b then f b else 0
h : HasSum (fun b_1 => update f b x b_1 + if b_1 = b then f b else 0) (a + x)
⊢ a + x = a' + f b
[PROOFSTEP]
exact HasSum.unique h (hf'.add (hasSum_ite_eq b (f b)))
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : AddCommMonoid α✝
inst✝⁵ : TopologicalSpace α✝
f✝ g : β✝ → α✝
a✝ b✝ : α✝
s : Finset β✝
inst✝⁴ : ContinuousAdd α✝
α : Type u_5
β : Type u_6
inst✝³ : TopologicalSpace α
inst✝² : AddCommMonoid α
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
f : β → α
a : α
hf : HasSum f a
b : β
a' : α
hf' : HasSum (fun n => if n = b then 0 else f n) a'
⊢ a = a' + f b
[PROOFSTEP]
refine' (add_zero a).symm.trans (hf.update' b 0 _)
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : AddCommMonoid α✝
inst✝⁵ : TopologicalSpace α✝
f✝ g : β✝ → α✝
a✝ b✝ : α✝
s : Finset β✝
inst✝⁴ : ContinuousAdd α✝
α : Type u_5
β : Type u_6
inst✝³ : TopologicalSpace α
inst✝² : AddCommMonoid α
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
f : β → α
a : α
hf : HasSum f a
b : β
a' : α
hf' : HasSum (fun n => if n = b then 0 else f n) a'
⊢ HasSum (update f b 0) a'
[PROOFSTEP]
convert hf'
[GOAL]
case h.e'_5.h
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : AddCommMonoid α✝
inst✝⁵ : TopologicalSpace α✝
f✝ g : β✝ → α✝
a✝ b✝ : α✝
s : Finset β✝
inst✝⁴ : ContinuousAdd α✝
α : Type u_5
β : Type u_6
inst✝³ : TopologicalSpace α
inst✝² : AddCommMonoid α
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
f : β → α
a : α
hf : HasSum f a
b : β
a' : α
hf' : HasSum (fun n => if n = b then 0 else f n) a'
x✝ : β
⊢ update f b 0 x✝ = if x✝ = b then 0 else f x✝
[PROOFSTEP]
apply update_apply
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f✝ g : β → α
a a₁ a₂ : α
f : β → α
s t : Set β
h : s = t
⊢ ∑' (x : ↑s), f ↑x = ∑' (x : ↑t), f ↑x
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
hf : Set.Finite (support f)
⊢ ∑' (b : β), f b = ∑ᶠ (b : β), f b
[PROOFSTEP]
simp [tsum_def, summable_of_finite_support hf, hf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
s : Finset β
hf : ∀ (b : β), ¬b ∈ s → f b = 0
⊢ ∑' (b : β), f b = ∑ b in s, f b
[PROOFSTEP]
have I : support f ⊆ s := by
  intros x hx
  contrapose! hx
  rw [nmem_support]
  exact hf _ hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
s : Finset β
hf : ∀ (b : β), ¬b ∈ s → f b = 0
⊢ support f ⊆ ↑s
[PROOFSTEP]
intros x hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
s : Finset β
hf : ∀ (b : β), ¬b ∈ s → f b = 0
x : β
hx : x ∈ support f
⊢ x ∈ ↑s
[PROOFSTEP]
contrapose! hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
s : Finset β
hf : ∀ (b : β), ¬b ∈ s → f b = 0
x : β
hx : ¬x ∈ ↑s
⊢ ¬x ∈ support f
[PROOFSTEP]
rw [nmem_support]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
s : Finset β
hf : ∀ (b : β), ¬b ∈ s → f b = 0
x : β
hx : ¬x ∈ ↑s
⊢ f x = 0
[PROOFSTEP]
exact hf _ hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
s : Finset β
hf : ∀ (b : β), ¬b ∈ s → f b = 0
I : support f ⊆ ↑s
⊢ ∑' (b : β), f b = ∑ b in s, f b
[PROOFSTEP]
simp [tsum_def, summable_of_ne_finset_zero hf, Set.Finite.subset (finite_toSet s) I]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
s : Finset β
hf : ∀ (b : β), ¬b ∈ s → f b = 0
I : support f ⊆ ↑s
⊢ ∑ᶠ (b : β), f b = ∑ b in s, f b
[PROOFSTEP]
exact finsum_eq_sum_of_support_subset f I
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
⊢ ∑' (x : β), 0 = 0
[PROOFSTEP]
rw [tsum_eq_finsum]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
⊢ ∑ᶠ (b : β), 0 = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
⊢ Set.Finite (support fun x => 0)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝ : IsEmpty β
⊢ ∑' (b : β), f b = 0
[PROOFSTEP]
rw [tsum_eq_sum (s := (∅ : Finset β))]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝ : IsEmpty β
⊢ ∑ b in ∅, f b = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝ : IsEmpty β
⊢ ∀ (b : β), ¬b ∈ ∅ → f b = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f✝ g : β → α
a a₁ a₂ : α
inst✝ : Fintype β
f : β → α
⊢ ∑' (b : β), f b = ∑ b : β, f b
[PROOFSTEP]
apply tsum_eq_sum
[GOAL]
case hf
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f✝ g : β → α
a a₁ a₂ : α
inst✝ : Fintype β
f : β → α
⊢ ∀ (b : β), ¬b ∈ univ → f b = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f✝ g : β → α
a a₁ a₂ : α
f : Bool → α
⊢ ∑' (i : Bool), f i = f (decide False) + f (decide True)
[PROOFSTEP]
rw [tsum_fintype, Finset.sum_eq_add]
[GOAL]
case hn
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f✝ g : β → α
a a₁ a₂ : α
f : Bool → α
⊢ decide False ≠ decide True
[PROOFSTEP]
simp
[GOAL]
case h₀
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f✝ g : β → α
a a₁ a₂ : α
f : Bool → α
⊢ ∀ (c : Bool), c ∈ univ → c ≠ decide False ∧ c ≠ decide True → f c = 0
[PROOFSTEP]
simp
[GOAL]
case ha
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f✝ g : β → α
a a₁ a₂ : α
f : Bool → α
⊢ ¬decide False ∈ univ → f (decide False) = 0
[PROOFSTEP]
simp
[GOAL]
case hb
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f✝ g : β → α
a a₁ a₂ : α
f : Bool → α
⊢ ¬decide True ∈ univ → f (decide True) = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f✝ g : β → α
a a₁ a₂ : α
f : β → α
b : β
hf : ∀ (b' : β), b' ≠ b → f b' = 0
⊢ ∑' (b : β), f b = f b
[PROOFSTEP]
rw [tsum_eq_sum (s := { b }), sum_singleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f✝ g : β → α
a a₁ a₂ : α
f : β → α
b : β
hf : ∀ (b' : β), b' ≠ b → f b' = 0
⊢ ∀ (b_1 : β), ¬b_1 ∈ {b} → f b_1 = 0
[PROOFSTEP]
exact fun b' hb' ↦ hf b' (by simpa using hb')
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f✝ g : β → α
a a₁ a₂ : α
f : β → α
b : β
hf : ∀ (b' : β), b' ≠ b → f b' = 0
b' : β
hb' : ¬b' ∈ {b}
⊢ b' ≠ b
[PROOFSTEP]
simpa using hb'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a✝ a₁ a₂ : α
b : β
inst✝ : DecidablePred fun x => x = b
a : α
⊢ (∑' (b' : β), if b' = b then a else 0) = a
[PROOFSTEP]
rw [tsum_eq_single b]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a✝ a₁ a₂ : α
b : β
inst✝ : DecidablePred fun x => x = b
a : α
⊢ (if b = b then a else 0) = a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a✝ a₁ a₂ : α
b : β
inst✝ : DecidablePred fun x => x = b
a : α
⊢ ∀ (b' : β), b' ≠ b → (if b' = b then a else 0) = 0
[PROOFSTEP]
intro b' hb'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a✝ a₁ a₂ : α
b : β
inst✝ : DecidablePred fun x => x = b
a : α
b' : β
hb' : b' ≠ b
⊢ (if b' = b then a else 0) = 0
[PROOFSTEP]
simp [hb']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a✝ a₁ a₂ : α
inst✝ : DecidableEq β
b : β
a : α
⊢ ∑' (b' : β), Pi.single b a b' = a
[PROOFSTEP]
rw [tsum_eq_single b]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a✝ a₁ a₂ : α
inst✝ : DecidableEq β
b : β
a : α
⊢ Pi.single b a b = a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a✝ a₁ a₂ : α
inst✝ : DecidableEq β
b : β
a : α
⊢ ∀ (b' : β), b' ≠ b → Pi.single b a b' = 0
[PROOFSTEP]
intro b' hb'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a✝ a₁ a₂ : α
inst✝ : DecidableEq β
b : β
a : α
b' : β
hb' : b' ≠ b
⊢ Pi.single b a b' = 0
[PROOFSTEP]
simp [hb']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f✝ g : β → α
a a₁ a₂ : α
s : Finset β
f : β → α
⊢ ∑' (x : { x // x ∈ s }), f ↑x = ∑ x in s, f x
[PROOFSTEP]
rw [← sum_attach]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f✝ g : β → α
a a₁ a₂ : α
s : Finset β
f : β → α
⊢ ∑' (x : { x // x ∈ s }), f ↑x = ∑ x in attach s, f ↑x
[PROOFSTEP]
exact tsum_fintype _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f✝ g : β → α
a a₁ a₂ : α
s : Finset β
f : β → α
⊢ ∑' (x : ↑↑s), f ↑x = ∑ x in s, f x
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f✝ g : β → α
a a₁ a₂ : α
b : β
f : β → α
⊢ ∑' (x : ↑{b}), f ↑x = f b
[PROOFSTEP]
rw [← coe_singleton, Finset.tsum_subtype', sum_singleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝¹ : T2Space α
P : Prop
inst✝ : Decidable P
x : β → ¬P → α
⊢ (∑' (b : β), if h : P then 0 else x b h) = if h : P then 0 else ∑' (b : β), x b h
[PROOFSTEP]
by_cases hP : P
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝¹ : T2Space α
P : Prop
inst✝ : Decidable P
x : β → ¬P → α
hP : P
⊢ (∑' (b : β), if h : P then 0 else x b h) = if h : P then 0 else ∑' (b : β), x b h
[PROOFSTEP]
simp [hP]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝¹ : T2Space α
P : Prop
inst✝ : Decidable P
x : β → ¬P → α
hP : ¬P
⊢ (∑' (b : β), if h : P then 0 else x b h) = if h : P then 0 else ∑' (b : β), x b h
[PROOFSTEP]
simp [hP]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝¹ : T2Space α
P : Prop
inst✝ : Decidable P
x : β → P → α
⊢ (∑' (b : β), if h : P then x b h else 0) = if h : P then ∑' (b : β), x b h else 0
[PROOFSTEP]
by_cases hP : P
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝¹ : T2Space α
P : Prop
inst✝ : Decidable P
x : β → P → α
hP : P
⊢ (∑' (b : β), if h : P then x b h else 0) = if h : P then ∑' (b : β), x b h else 0
[PROOFSTEP]
simp [hP]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝¹ : T2Space α
P : Prop
inst✝ : Decidable P
x : β → P → α
hP : ¬P
⊢ (∑' (b : β), if h : P then x b h else 0) = if h : P then ∑' (b : β), x b h else 0
[PROOFSTEP]
simp [hP]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
f✝ g✝ : β → α
a a₁ a₂ : α
inst✝² : T2Space α
α' : Type u_5
inst✝¹ : AddCommMonoid α'
inst✝ : TopologicalSpace α'
e : α' → α
hes : Surjective e
h0 : e 0 = 0
f : β → α
g : γ → α'
h : ∀ {a : α'}, HasSum f (e a) ↔ HasSum g a
hg : ¬Summable g
⊢ ∑' (b : β), f b = e (∑' (c : γ), g c)
[PROOFSTEP]
have hf : ¬Summable f := mt (hes.summable_iff_of_hasSum_iff @h).1 hg
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
f✝ g✝ : β → α
a a₁ a₂ : α
inst✝² : T2Space α
α' : Type u_5
inst✝¹ : AddCommMonoid α'
inst✝ : TopologicalSpace α'
e : α' → α
hes : Surjective e
h0 : e 0 = 0
f : β → α
g : γ → α'
h : ∀ {a : α'}, HasSum f (e a) ↔ HasSum g a
hg : ¬Summable g
hf : ¬Summable f
⊢ ∑' (b : β), f b = e (∑' (c : γ), g c)
[PROOFSTEP]
simp [tsum_def, hf, hg, h0]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f✝ g✝ : β → α
a a₁ a₂ : α
inst✝ : T2Space α
g : γ → β
f : β → α
hg : Injective g
⊢ ∑' (x : ↑(Set.range g)), f ↑x = ∑' (x : γ), f (g x)
[PROOFSTEP]
rw [← Set.image_univ, tsum_image f (hg.injOn _)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f✝ g✝ : β → α
a a₁ a₂ : α
inst✝ : T2Space α
g : γ → β
f : β → α
hg : Injective g
⊢ ∑' (x : ↑Set.univ), f (g ↑x) = ∑' (x : γ), f (g x)
[PROOFSTEP]
simp_rw [← comp_apply (g := g), tsum_univ (f ∘ g)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
f✝ g : β → α
a a₁ a₂ : α
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
f : β → α
b : β
hf : Summable (update f b 0)
n : β
⊢ f n = (if n = b then f n else 0) + update f b 0 n
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
f✝ g : β → α
a a₁ a₂ : α
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
f : β → α
b : β
hf : Summable (update f b 0)
n : β
h : n = b
⊢ f n = f n + update f b 0 n
[PROOFSTEP]
simp [update_apply, h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
f✝ g : β → α
a a₁ a₂ : α
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
f : β → α
b : β
hf : Summable (update f b 0)
n : β
h : ¬n = b
⊢ f n = 0 + update f b 0 n
[PROOFSTEP]
simp [update_apply, h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
f✝ g : β → α
a a₁ a₂ : α
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
f : β → α
b : β
hf : Summable (update f b 0)
⊢ (∑' (x : β), if x = b then f x else 0) + ∑' (x : β), update f b 0 x =
    (if b = b then f b else 0) + ∑' (x : β), update f b 0 x
[PROOFSTEP]
congr
[GOAL]
case e_a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
f✝ g : β → α
a a₁ a₂ : α
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
f : β → α
b : β
hf : Summable (update f b 0)
⊢ (∑' (x : β), if x = b then f x else 0) = if b = b then f b else 0
[PROOFSTEP]
exact tsum_eq_single b fun b' hb' => if_neg hb'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
f✝ g : β → α
a a₁ a₂ : α
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
f : β → α
b : β
hf : Summable (update f b 0)
⊢ (if b = b then f b else 0) + ∑' (x : β), update f b 0 x = f b + ∑' (x : β), if x = b then 0 else f x
[PROOFSTEP]
simp only [update, eq_self_iff_true, if_true, eq_rec_constant, dite_eq_ite]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁷ : AddCommMonoid α
inst✝⁶ : TopologicalSpace α
f✝ g : β → α
a a₁ a₂ : α
inst✝⁵ : T2Space α
inst✝⁴ : ContinuousAdd α
inst✝³ : AddCommMonoid δ
inst✝² : TopologicalSpace δ
inst✝¹ : T3Space δ
inst✝ : ContinuousAdd δ
f : β → γ → δ
h : Summable (uncurry f)
h₁ : ∀ (b : β), Summable (f b)
h₂ : ∀ (c : γ), Summable fun b => f b c
⊢ ∑' (c : γ) (b : β), f b c = ∑' (b : β) (c : γ), f b c
[PROOFSTEP]
erw [← tsum_prod' h h₁, ← tsum_prod' h.prod_symm h₂, ← (Equiv.prodComm γ β).tsum_eq (uncurry f)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁷ : AddCommMonoid α
inst✝⁶ : TopologicalSpace α
f✝ g : β → α
a a₁ a₂ : α
inst✝⁵ : T2Space α
inst✝⁴ : ContinuousAdd α
inst✝³ : AddCommMonoid δ
inst✝² : TopologicalSpace δ
inst✝¹ : T3Space δ
inst✝ : ContinuousAdd δ
f : β → γ → δ
h : Summable (uncurry f)
h₁ : ∀ (b : β), Summable (f b)
h₂ : ∀ (c : γ), Summable fun b => f b c
⊢ ∑' (p : γ × β), uncurry f (Prod.swap p) = ∑' (c : γ × β), uncurry f (↑(Equiv.prodComm γ β) c)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝² : T2Space α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
⊢ ∑' (i : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b) = ∑' (b : γ), m (s b)
[PROOFSTEP]
have H : ∀ n, m (⨆ b ∈ decode₂ γ n, s b) ≠ 0 → (decode₂ γ n).isSome :=
  by
  intro n h
  generalize decode₂ γ n = foo at *
  cases' foo with b
  · refine' (h <| by simp [m0]).elim
  · exact rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝² : T2Space α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
⊢ ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
[PROOFSTEP]
intro n h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝² : T2Space α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
n : ℕ
h : m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0
⊢ Option.isSome (decode₂ γ n) = true
[PROOFSTEP]
generalize decode₂ γ n = foo at *
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝² : T2Space α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
n : ℕ
foo : Option γ
h : m (⨆ (b : γ) (_ : b ∈ foo), s b) ≠ 0
⊢ Option.isSome foo = true
[PROOFSTEP]
cases' foo with b
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝² : T2Space α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
n : ℕ
h : m (⨆ (b : γ) (_ : b ∈ none), s b) ≠ 0
⊢ Option.isSome none = true
[PROOFSTEP]
refine' (h <| by simp [m0]).elim
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝² : T2Space α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
n : ℕ
h : m (⨆ (b : γ) (_ : b ∈ none), s b) ≠ 0
⊢ m (⨆ (b : γ) (_ : b ∈ none), s b) = 0
[PROOFSTEP]
simp [m0]
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝² : T2Space α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
n : ℕ
b : γ
h : m (⨆ (b_1 : γ) (_ : b_1 ∈ some b), s b_1) ≠ 0
⊢ Option.isSome (some b) = true
[PROOFSTEP]
exact rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝² : T2Space α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
⊢ ∑' (i : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b) = ∑' (b : γ), m (s b)
[PROOFSTEP]
symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝² : T2Space α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
⊢ ∑' (b : γ), m (s b) = ∑' (i : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
[PROOFSTEP]
refine' tsum_eq_tsum_of_ne_zero_bij (fun a => Option.get _ (H a.1 a.2)) _ _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝² : T2Space α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
⊢ ∀ ⦃x y : ↑(support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b))⦄,
    (fun a => Option.get (decode₂ γ ↑a) (_ : Option.isSome (decode₂ γ ↑a) = true)) x =
        (fun a => Option.get (decode₂ γ ↑a) (_ : Option.isSome (decode₂ γ ↑a) = true)) y →
      ↑x = ↑y
[PROOFSTEP]
dsimp only []
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝² : T2Space α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
⊢ ∀ ⦃x y : ↑(support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b))⦄,
    Option.get (decode₂ γ ↑x) (_ : Option.isSome (decode₂ γ ↑x) = true) =
        Option.get (decode₂ γ ↑y) (_ : Option.isSome (decode₂ γ ↑y) = true) →
      ↑x = ↑y
[PROOFSTEP]
rintro ⟨m, hm⟩ ⟨n, hn⟩ e
[GOAL]
case refine'_1.mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝² : T2Space α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m✝ : β → α
m0 : m✝ ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m✝ (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
m : ℕ
hm : m ∈ support fun i => m✝ (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
n : ℕ
hn : n ∈ support fun i => m✝ (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
e :
  Option.get (decode₂ γ ↑{ val := m, property := hm })
      (_ : Option.isSome (decode₂ γ ↑{ val := m, property := hm }) = true) =
    Option.get (decode₂ γ ↑{ val := n, property := hn })
      (_ : Option.isSome (decode₂ γ ↑{ val := n, property := hn }) = true)
⊢ ↑{ val := m, property := hm } = ↑{ val := n, property := hn }
[PROOFSTEP]
have := mem_decode₂.1 (Option.get_mem (H n hn))
[GOAL]
case refine'_1.mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝² : T2Space α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m✝ : β → α
m0 : m✝ ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m✝ (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
m : ℕ
hm : m ∈ support fun i => m✝ (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
n : ℕ
hn : n ∈ support fun i => m✝ (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
e :
  Option.get (decode₂ γ ↑{ val := m, property := hm })
      (_ : Option.isSome (decode₂ γ ↑{ val := m, property := hm }) = true) =
    Option.get (decode₂ γ ↑{ val := n, property := hn })
      (_ : Option.isSome (decode₂ γ ↑{ val := n, property := hn }) = true)
this : encode (Option.get (decode₂ γ n) (_ : Option.isSome (decode₂ γ n) = true)) = n
⊢ ↑{ val := m, property := hm } = ↑{ val := n, property := hn }
[PROOFSTEP]
rwa [← e, mem_decode₂.1 (Option.get_mem (H m hm))] at this 
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝² : T2Space α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
⊢ (support fun b => m (s b)) ⊆ Set.range fun a => Option.get (decode₂ γ ↑a) (_ : Option.isSome (decode₂ γ ↑a) = true)
[PROOFSTEP]
intro b h
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝² : T2Space α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
b : γ
h : b ∈ support fun b => m (s b)
⊢ b ∈ Set.range fun a => Option.get (decode₂ γ ↑a) (_ : Option.isSome (decode₂ γ ↑a) = true)
[PROOFSTEP]
refine' ⟨⟨encode b, _⟩, _⟩
[GOAL]
case refine'_2.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝² : T2Space α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
b : γ
h : b ∈ support fun b => m (s b)
⊢ encode b ∈ support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
[PROOFSTEP]
simp only [mem_support, encodek₂] at h ⊢
[GOAL]
case refine'_2.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝² : T2Space α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
b : γ
h : m (s b) ≠ 0
⊢ m (⨆ (b_1 : γ) (_ : b_1 ∈ some b), s b_1) ≠ 0
[PROOFSTEP]
convert h
[GOAL]
case h.e'_2.h.e'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝² : T2Space α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
b : γ
h : m (s b) ≠ 0
⊢ ⨆ (b_1 : γ) (_ : b_1 ∈ some b), s b_1 = s b
[PROOFSTEP]
simp [Set.ext_iff, encodek₂]
[GOAL]
case refine'_2.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝² : T2Space α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
b : γ
h : b ∈ support fun b => m (s b)
⊢ (fun a => Option.get (decode₂ γ ↑a) (_ : Option.isSome (decode₂ γ ↑a) = true))
      { val := encode b, property := (_ : encode b ∈ support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)) } =
    b
[PROOFSTEP]
exact Option.get_of_mem _ (encodek₂ _)
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝² : T2Space α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
⊢ ∀ (x : ↑(support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b))),
    m (s ((fun a => Option.get (decode₂ γ ↑a) (_ : Option.isSome (decode₂ γ ↑a) = true)) x)) =
      m (⨆ (b : γ) (_ : b ∈ decode₂ γ ↑x), s b)
[PROOFSTEP]
rintro ⟨n, h⟩
[GOAL]
case refine'_3.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝² : T2Space α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
n : ℕ
h : n ∈ support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
⊢ m (s ((fun a => Option.get (decode₂ γ ↑a) (_ : Option.isSome (decode₂ γ ↑a) = true)) { val := n, property := h })) =
    m (⨆ (b : γ) (_ : b ∈ decode₂ γ ↑{ val := n, property := h }), s b)
[PROOFSTEP]
dsimp only [Subtype.coe_mk]
[GOAL]
case refine'_3.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝² : T2Space α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
n : ℕ
h : n ∈ support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
⊢ m (s (Option.get (decode₂ γ n) (_ : Option.isSome (decode₂ γ n) = true))) = m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b)
[PROOFSTEP]
trans
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝² : T2Space α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
n : ℕ
h : n ∈ support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
⊢ m (s (Option.get (decode₂ γ n) (_ : Option.isSome (decode₂ γ n) = true))) = ?m.392413
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝² : T2Space α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
n : ℕ
h : n ∈ support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
⊢ ?m.392413 = m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b)
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝² : T2Space α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
n : ℕ
h : n ∈ support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
⊢ α
[PROOFSTEP]
swap
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝² : T2Space α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
n : ℕ
h : n ∈ support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
⊢ ?m.392413 = m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b)
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝² : T2Space α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
n : ℕ
h : n ∈ support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
⊢ m (s (Option.get (decode₂ γ n) (_ : Option.isSome (decode₂ γ n) = true))) = ?m.392413
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝² : T2Space α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
n : ℕ
h : n ∈ support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
⊢ α
[PROOFSTEP]
rw [show decode₂ γ n = _ from Option.get_mem (H n h)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝² : T2Space α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
n : ℕ
h : n ∈ support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
⊢ m (s (Option.get (decode₂ γ n) (_ : Option.isSome (decode₂ γ n) = true))) =
    m (⨆ (b : γ) (_ : b ∈ some (Option.get (decode₂ γ n) (_ : Option.isSome (decode₂ γ n) = true))), s b)
[PROOFSTEP]
congr
[GOAL]
case e_a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝² : T2Space α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
n : ℕ
h : n ∈ support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
⊢ s (Option.get (decode₂ γ n) (_ : Option.isSome (decode₂ γ n) = true)) =
    ⨆ (b : γ) (_ : b ∈ some (Option.get (decode₂ γ n) (_ : Option.isSome (decode₂ γ n) = true))), s b
[PROOFSTEP]
simp [ext_iff, -Option.some_get]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝² : T2Space α
inst✝¹ : Countable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
R : α → α → Prop
m_iSup : ∀ (s : ℕ → β), R (m (⨆ (i : ℕ), s i)) (∑' (i : ℕ), m (s i))
s : γ → β
⊢ R (m (⨆ (b : γ), s b)) (∑' (b : γ), m (s b))
[PROOFSTEP]
cases nonempty_encodable γ
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝² : T2Space α
inst✝¹ : Countable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
R : α → α → Prop
m_iSup : ∀ (s : ℕ → β), R (m (⨆ (i : ℕ), s i)) (∑' (i : ℕ), m (s i))
s : γ → β
val✝ : Encodable γ
⊢ R (m (⨆ (b : γ), s b)) (∑' (b : γ), m (s b))
[PROOFSTEP]
rw [← iSup_decode₂, ← tsum_iSup_decode₂ _ m0 s]
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝² : T2Space α
inst✝¹ : Countable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
R : α → α → Prop
m_iSup : ∀ (s : ℕ → β), R (m (⨆ (i : ℕ), s i)) (∑' (i : ℕ), m (s i))
s : γ → β
val✝ : Encodable γ
⊢ R (m (⨆ (i : ℕ) (b : γ) (_ : b ∈ decode₂ γ i), s b)) (∑' (i : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b))
[PROOFSTEP]
exact m_iSup _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝² : T2Space α
inst✝¹ : Countable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
R : α → α → Prop
m_iSup : ∀ (s : ℕ → β), R (m (⨆ (i : ℕ), s i)) (∑' (i : ℕ), m (s i))
s : δ → β
t : Finset δ
⊢ R (m (⨆ (d : δ) (_ : d ∈ t), s d)) (∑ d in t, m (s d))
[PROOFSTEP]
rw [iSup_subtype', ← Finset.tsum_subtype]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝² : T2Space α
inst✝¹ : Countable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
R : α → α → Prop
m_iSup : ∀ (s : ℕ → β), R (m (⨆ (i : ℕ), s i)) (∑' (i : ℕ), m (s i))
s : δ → β
t : Finset δ
⊢ R (m (⨆ (x : { d // d ∈ t }), s ↑x)) (∑' (x : { x // x ∈ t }), m (s ↑x))
[PROOFSTEP]
exact rel_iSup_tsum m m0 R m_iSup _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝² : T2Space α
inst✝¹ : Countable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
R : α → α → Prop
m_iSup : ∀ (s : ℕ → β), R (m (⨆ (i : ℕ), s i)) (∑' (i : ℕ), m (s i))
s₁ s₂ : β
⊢ R (m (s₁ ⊔ s₂)) (m s₁ + m s₂)
[PROOFSTEP]
convert rel_iSup_tsum m m0 R m_iSup fun b => cond b s₁ s₂
[GOAL]
case h.e'_1.h.e'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝² : T2Space α
inst✝¹ : Countable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
R : α → α → Prop
m_iSup : ∀ (s : ℕ → β), R (m (⨆ (i : ℕ), s i)) (∑' (i : ℕ), m (s i))
s₁ s₂ : β
⊢ s₁ ⊔ s₂ = ⨆ (b : Bool), bif b then s₁ else s₂
[PROOFSTEP]
simp only [iSup_bool_eq, cond]
[GOAL]
case h.e'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
f g : β → α
a a₁ a₂ : α
inst✝² : T2Space α
inst✝¹ : Countable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
R : α → α → Prop
m_iSup : ∀ (s : ℕ → β), R (m (⨆ (i : ℕ), s i)) (∑' (i : ℕ), m (s i))
s₁ s₂ : β
⊢ m s₁ + m s₂ = ∑' (b : Bool), m (bif b then s₁ else s₂)
[PROOFSTEP]
rw [tsum_fintype, Fintype.sum_bool, cond, cond]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
h : HasSum f a
⊢ HasSum (fun b => -f b) (-a)
[PROOFSTEP]
simpa only using h.map (-AddMonoidHom.id α) continuous_neg
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
hf : Summable fun b => -f b
⊢ Summable f
[PROOFSTEP]
simpa only [neg_neg] using hf.neg
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
hf : HasSum f a₁
hg : HasSum g a₂
⊢ HasSum (fun b => f b - g b) (a₁ - a₂)
[PROOFSTEP]
simp only [sub_eq_add_neg]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
hf : HasSum f a₁
hg : HasSum g a₂
⊢ HasSum (fun b => f b + -g b) (a₁ + -a₂)
[PROOFSTEP]
exact hf.add hg.neg
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
hg : Summable g
hfg : Summable fun b => f b - g b
⊢ Summable f
[PROOFSTEP]
simpa only [sub_add_cancel] using hfg.add hg
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
hfg : Summable fun b => f b - g b
hf : Summable f
⊢ Summable fun b => g b - f b
[PROOFSTEP]
simpa only [neg_sub] using hfg.neg
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f g : β → α
a✝ a₁ a₂ : α
hf : HasSum f a₁
b : β
inst✝ : DecidableEq β
a : α
⊢ HasSum (Function.update f b a) (a - f b + a₁)
[PROOFSTEP]
convert (hasSum_ite_eq b (a - f b)).add hf
[GOAL]
case h.e'_5.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f g : β → α
a✝ a₁ a₂ : α
hf : HasSum f a₁
b : β
inst✝ : DecidableEq β
a : α
x✝ : β
⊢ Function.update f b a x✝ = (if x✝ = b then a - f b else 0) + f x✝
[PROOFSTEP]
rename_i b'
[GOAL]
case h.e'_5.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f g : β → α
a✝ a₁ a₂ : α
hf : HasSum f a₁
b : β
inst✝ : DecidableEq β
a : α
b' : β
⊢ Function.update f b a b' = (if b' = b then a - f b else 0) + f b'
[PROOFSTEP]
by_cases h : b' = b
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f g : β → α
a✝ a₁ a₂ : α
hf : HasSum f a₁
b : β
inst✝ : DecidableEq β
a : α
b' : β
h : b' = b
⊢ Function.update f b a b' = (if b' = b then a - f b else 0) + f b'
[PROOFSTEP]
rw [h, update_same]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f g : β → α
a✝ a₁ a₂ : α
hf : HasSum f a₁
b : β
inst✝ : DecidableEq β
a : α
b' : β
h : b' = b
⊢ a = (if b = b then a - f b else 0) + f b
[PROOFSTEP]
simp [eq_self_iff_true, if_true, sub_add_cancel]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f g : β → α
a✝ a₁ a₂ : α
hf : HasSum f a₁
b : β
inst✝ : DecidableEq β
a : α
b' : β
h : ¬b' = b
⊢ Function.update f b a b' = (if b' = b then a - f b else 0) + f b'
[PROOFSTEP]
simp only [h, update_noteq, if_false, Ne.def, zero_add, not_false_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
s : Set β
hf : HasSum (f ∘ Subtype.val) a₁
⊢ HasSum (f ∘ Subtype.val) a₂ ↔ HasSum f (a₁ + a₂)
[PROOFSTEP]
refine' ⟨fun h => hf.add_compl h, fun h => _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
s : Set β
hf : HasSum (f ∘ Subtype.val) a₁
h : HasSum f (a₁ + a₂)
⊢ HasSum (f ∘ Subtype.val) a₂
[PROOFSTEP]
rw [hasSum_subtype_iff_indicator] at hf ⊢
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
s : Set β
hf : HasSum (Set.indicator s f) a₁
h : HasSum f (a₁ + a₂)
⊢ HasSum (Set.indicator sᶜ f) a₂
[PROOFSTEP]
rw [Set.indicator_compl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
s : Set β
hf : HasSum (Set.indicator s f) a₁
h : HasSum f (a₁ + a₂)
⊢ HasSum (f - Set.indicator s f) a₂
[PROOFSTEP]
simpa only [add_sub_cancel'] using h.sub hf
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
s : Set β
hf : HasSum (f ∘ Subtype.val) a₁
⊢ HasSum f (a₁ + (a₂ - a₁)) ↔ HasSum f a₂
[PROOFSTEP]
rw [add_sub_cancel'_right]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
s : Finset β
⊢ HasSum f (∑ b in s, f b + a) ↔ HasSum f (a + ∑ i in s, f i)
[PROOFSTEP]
rw [add_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
inst✝ : DecidableEq β
hf : HasSum f a
b : β
⊢ HasSum (fun n => if n = b then 0 else f n) (a - f b)
[PROOFSTEP]
convert hf.update b 0 using 1
[GOAL]
case h.e'_5
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
inst✝ : DecidableEq β
hf : HasSum f a
b : β
⊢ (fun n => if n = b then 0 else f n) = update f b 0
[PROOFSTEP]
ext n
[GOAL]
case h.e'_5.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
inst✝ : DecidableEq β
hf : HasSum f a
b n : β
⊢ (if n = b then 0 else f n) = update f b 0 n
[PROOFSTEP]
rw [Function.update_apply]
[GOAL]
case h.e'_6
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
inst✝ : DecidableEq β
hf : HasSum f a
b : β
⊢ a - f b = 0 - f b + a
[PROOFSTEP]
rw [sub_add_eq_add_sub, zero_add]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
inst✝ : T2Space α
⊢ ∑' (b : β), -f b = -∑' (b : β), f b
[PROOFSTEP]
by_cases hf : Summable f
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
inst✝ : T2Space α
hf : Summable f
⊢ ∑' (b : β), -f b = -∑' (b : β), f b
[PROOFSTEP]
exact hf.hasSum.neg.tsum_eq
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
inst✝ : T2Space α
hf : ¬Summable f
⊢ ∑' (b : β), -f b = -∑' (b : β), f b
[PROOFSTEP]
simp [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable (mt Summable.of_neg hf)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommGroup α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
inst✝¹ : T2Space α
inst✝ : DecidableEq β
hf : Summable f
b : β
⊢ ∑' (n : β), f n = f b + ∑' (n : β), if n = b then 0 else f n
[PROOFSTEP]
rw [(hasSum_ite_sub_hasSum hf.hasSum b).tsum_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommGroup α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
inst✝¹ : T2Space α
inst✝ : DecidableEq β
hf : Summable f
b : β
⊢ ∑' (n : β), f n = f b + (∑' (b : β), f b - f b)
[PROOFSTEP]
exact (add_sub_cancel'_right _ _).symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g : β → α
a✝ a₁ a₂ : α
f : ℕ → α
k : ℕ
a : α
⊢ HasSum (fun n => f (n + k)) a ↔ HasSum f (a + ∑ i in range k, f i)
[PROOFSTEP]
refine' Iff.trans _ (range k).hasSum_compl_iff
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g : β → α
a✝ a₁ a₂ : α
f : ℕ → α
k : ℕ
a : α
⊢ HasSum (fun n => f (n + k)) a ↔ HasSum (fun x => f ↑x) a
[PROOFSTEP]
rw [← (notMemRangeEquiv k).symm.hasSum_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g : β → α
a✝ a₁ a₂ : α
f : ℕ → α
k : ℕ
a : α
⊢ HasSum (fun n => f (n + k)) a ↔ HasSum ((fun x => f ↑x) ∘ ↑(notMemRangeEquiv k).symm) a
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g : β → α
a✝ a₁ a₂ : α
f : ℕ → α
k : ℕ
a : α
⊢ HasSum (fun n => f (n + k)) (a - ∑ i in range k, f i) ↔ HasSum f a
[PROOFSTEP]
simp [hasSum_nat_add_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : AddCommGroup α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalAddGroup α
f✝ g : β → α
a✝ a₁ a₂ : α
M : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousAdd M
f : ℕ → M
k : ℕ
a : M
h : HasSum (fun n => f (n + k)) a
⊢ HasSum f (∑ i in range k, f i + a)
[PROOFSTEP]
refine ((range k).hasSum f).add_compl ?_
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : AddCommGroup α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalAddGroup α
f✝ g : β → α
a✝ a₁ a₂ : α
M : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousAdd M
f : ℕ → M
k : ℕ
a : M
h : HasSum (fun n => f (n + k)) a
⊢ HasSum (f ∘ Subtype.val) a
[PROOFSTEP]
rwa [← (notMemRangeEquiv k).symm.hasSum_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : AddCommGroup α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalAddGroup α
f✝ g : β → α
a a₁ a₂ : α
M : Type u_5
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousAdd M
inst✝ : T2Space M
f : ℕ → M
hf : Summable fun n => f (n + 1)
⊢ ∑' (b : ℕ), f b = f 0 + ∑' (b : ℕ), f (b + 1)
[PROOFSTEP]
simpa only [sum_range_one] using (sum_add_tsum_nat_add' hf).symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f✝ g : β → α
a a₁ a₂ : α
inst✝ : T2Space α
f : ℕ → α
⊢ Tendsto (fun i => ∑' (k : ℕ), f (k + i)) atTop (𝓝 0)
[PROOFSTEP]
by_cases hf : Summable f
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f✝ g : β → α
a a₁ a₂ : α
inst✝ : T2Space α
f : ℕ → α
hf : Summable f
⊢ Tendsto (fun i => ∑' (k : ℕ), f (k + i)) atTop (𝓝 0)
[PROOFSTEP]
have h₀ : (fun i => ∑' i, f i - ∑ j in range i, f j) = fun i => ∑' k : ℕ, f (k + i) :=
  by
  ext1 i
  rw [sub_eq_iff_eq_add, add_comm, sum_add_tsum_nat_add i hf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f✝ g : β → α
a a₁ a₂ : α
inst✝ : T2Space α
f : ℕ → α
hf : Summable f
⊢ (fun i => ∑' (i : ℕ), f i - ∑ j in range i, f j) = fun i => ∑' (k : ℕ), f (k + i)
[PROOFSTEP]
ext1 i
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f✝ g : β → α
a a₁ a₂ : α
inst✝ : T2Space α
f : ℕ → α
hf : Summable f
i : ℕ
⊢ ∑' (i : ℕ), f i - ∑ j in range i, f j = ∑' (k : ℕ), f (k + i)
[PROOFSTEP]
rw [sub_eq_iff_eq_add, add_comm, sum_add_tsum_nat_add i hf]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f✝ g : β → α
a a₁ a₂ : α
inst✝ : T2Space α
f : ℕ → α
hf : Summable f
h₀ : (fun i => ∑' (i : ℕ), f i - ∑ j in range i, f j) = fun i => ∑' (k : ℕ), f (k + i)
⊢ Tendsto (fun i => ∑' (k : ℕ), f (k + i)) atTop (𝓝 0)
[PROOFSTEP]
have h₁ : Tendsto (fun _ : ℕ => ∑' i, f i) atTop (𝓝 (∑' i, f i)) := tendsto_const_nhds
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f✝ g : β → α
a a₁ a₂ : α
inst✝ : T2Space α
f : ℕ → α
hf : Summable f
h₀ : (fun i => ∑' (i : ℕ), f i - ∑ j in range i, f j) = fun i => ∑' (k : ℕ), f (k + i)
h₁ : Tendsto (fun x => ∑' (i : ℕ), f i) atTop (𝓝 (∑' (i : ℕ), f i))
⊢ Tendsto (fun i => ∑' (k : ℕ), f (k + i)) atTop (𝓝 0)
[PROOFSTEP]
simpa only [h₀, sub_self] using Tendsto.sub h₁ hf.hasSum.tendsto_sum_nat
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f✝ g : β → α
a a₁ a₂ : α
inst✝ : T2Space α
f : ℕ → α
hf : ¬Summable f
⊢ Tendsto (fun i => ∑' (k : ℕ), f (k + i)) atTop (𝓝 0)
[PROOFSTEP]
convert tendsto_const_nhds (α := α) (β := ℕ) (a := 0) (f := atTop)
[GOAL]
case h.e'_3.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f✝ g : β → α
a a₁ a₂ : α
inst✝ : T2Space α
f : ℕ → α
hf : ¬Summable f
x✝ : ℕ
⊢ ∑' (k : ℕ), f (k + x✝) = 0
[PROOFSTEP]
rename_i i
[GOAL]
case h.e'_3.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f✝ g : β → α
a a₁ a₂ : α
inst✝ : T2Space α
f : ℕ → α
hf : ¬Summable f
i : ℕ
⊢ ∑' (k : ℕ), f (k + i) = 0
[PROOFSTEP]
rw [← summable_nat_add_iff i] at hf 
[GOAL]
case h.e'_3.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f✝ g : β → α
a a₁ a₂ : α
inst✝ : T2Space α
f : ℕ → α
i : ℕ
hf : ¬Summable fun n => f (n + i)
⊢ ∑' (k : ℕ), f (k + i) = 0
[PROOFSTEP]
exact tsum_eq_zero_of_not_summable hf
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g✝ : β → α
a a₁ a₂ b : α
f g : ℕ → α
hf : HasSum f a
hg : HasSum g b
⊢ HasSum (Int.rec f g) (a + b)
[PROOFSTEP]
have h₁ : Injective ((↑) : ℕ → ℤ) := @Int.ofNat.inj
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g✝ : β → α
a a₁ a₂ b : α
f g : ℕ → α
hf : HasSum f a
hg : HasSum g b
h₁ : Injective Nat.cast
⊢ HasSum (Int.rec f g) (a + b)
[PROOFSTEP]
have h₂ : Injective Int.negSucc := @Int.negSucc.inj
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g✝ : β → α
a a₁ a₂ b : α
f g : ℕ → α
hf : HasSum f a
hg : HasSum g b
h₁ : Injective Nat.cast
h₂ : Injective Int.negSucc
⊢ HasSum (Int.rec f g) (a + b)
[PROOFSTEP]
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) _
    exacts [Or.inl ⟨_, rfl⟩, Or.inr ⟨_, rfl⟩]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g✝ : β → α
a a₁ a₂ b : α
f g : ℕ → α
hf : HasSum f a
hg : HasSum g b
h₁ : Injective Nat.cast
h₂ : Injective Int.negSucc
⊢ IsCompl (Set.range Nat.cast) (Set.range Int.negSucc)
[PROOFSTEP]
constructor
[GOAL]
case disjoint
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g✝ : β → α
a a₁ a₂ b : α
f g : ℕ → α
hf : HasSum f a
hg : HasSum g b
h₁ : Injective Nat.cast
h₂ : Injective Int.negSucc
⊢ Disjoint (Set.range Nat.cast) (Set.range Int.negSucc)
[PROOFSTEP]
rw [disjoint_iff_inf_le]
[GOAL]
case disjoint
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g✝ : β → α
a a₁ a₂ b : α
f g : ℕ → α
hf : HasSum f a
hg : HasSum g b
h₁ : Injective Nat.cast
h₂ : Injective Int.negSucc
⊢ Set.range Nat.cast ⊓ Set.range Int.negSucc ≤ ⊥
[PROOFSTEP]
rintro _ ⟨⟨i, rfl⟩, ⟨j, ⟨⟩⟩⟩
[GOAL]
case codisjoint
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g✝ : β → α
a a₁ a₂ b : α
f g : ℕ → α
hf : HasSum f a
hg : HasSum g b
h₁ : Injective Nat.cast
h₂ : Injective Int.negSucc
⊢ Codisjoint (Set.range Nat.cast) (Set.range Int.negSucc)
[PROOFSTEP]
rw [codisjoint_iff_le_sup]
[GOAL]
case codisjoint
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g✝ : β → α
a a₁ a₂ b : α
f g : ℕ → α
hf : HasSum f a
hg : HasSum g b
h₁ : Injective Nat.cast
h₂ : Injective Int.negSucc
⊢ ⊤ ≤ Set.range Nat.cast ⊔ Set.range Int.negSucc
[PROOFSTEP]
rintro (i | j) _
[GOAL]
case codisjoint.ofNat
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g✝ : β → α
a a₁ a₂ b : α
f g : ℕ → α
hf : HasSum f a
hg : HasSum g b
h₁ : Injective Nat.cast
h₂ : Injective Int.negSucc
i : ℕ
a✝ : Int.ofNat i ∈ ⊤
⊢ Int.ofNat i ∈ Set.range Nat.cast ⊔ Set.range Int.negSucc
case codisjoint.negSucc
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g✝ : β → α
a a₁ a₂ b : α
f g : ℕ → α
hf : HasSum f a
hg : HasSum g b
h₁ : Injective Nat.cast
h₂ : Injective Int.negSucc
j : ℕ
a✝ : Int.negSucc j ∈ ⊤
⊢ Int.negSucc j ∈ Set.range Nat.cast ⊔ Set.range Int.negSucc
[PROOFSTEP]
exacts [Or.inl ⟨_, rfl⟩, Or.inr ⟨_, rfl⟩]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g✝ : β → α
a a₁ a₂ b : α
f g : ℕ → α
hf : HasSum f a
hg : HasSum g b
h₁ : Injective Nat.cast
h₂ : Injective Int.negSucc
this : IsCompl (Set.range Nat.cast) (Set.range Int.negSucc)
⊢ HasSum (Int.rec f g) (a + b)
[PROOFSTEP]
exact HasSum.add_isCompl this (h₁.hasSum_range_iff.mpr hf) (h₂.hasSum_range_iff.mpr hg)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
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)
[PROOFSTEP]
simp_rw [← Int.negSucc_coe] at hneg 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
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)
[PROOFSTEP]
convert hnonneg.int_rec hneg using 1
[GOAL]
case h.e'_5
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
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)
[PROOFSTEP]
ext (i | j)
[GOAL]
case h.e'_5.h.ofNat
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
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
i : ℕ
⊢ f (Int.ofNat i) = Int.rec (fun n => f ↑n) (fun n => f (Int.negSucc n)) (Int.ofNat i)
[PROOFSTEP]
rfl
[GOAL]
case h.e'_5.h.negSucc
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
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
j : ℕ
⊢ f (Int.negSucc j) = Int.rec (fun n => f ↑n) (fun n => f (Int.negSucc n)) (Int.negSucc j)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g : β → α
a a₁ a₂ b : α
f : ℤ → α
hpos : HasSum (fun n => f (↑n + 1)) a
hneg : HasSum (fun n => f (-↑(Nat.succ n))) b
⊢ ∀ (g : ℕ → α), HasSum (fun k => g (k + 1)) a → HasSum g (a + g 0)
[PROOFSTEP]
intro g hg
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g✝ : β → α
a a₁ a₂ b : α
f : ℤ → α
hpos : HasSum (fun n => f (↑n + 1)) a
hneg : HasSum (fun n => f (-↑(Nat.succ n))) b
g : ℕ → α
hg : HasSum (fun k => g (k + 1)) a
⊢ HasSum g (a + g 0)
[PROOFSTEP]
simpa using (hasSum_nat_add_iff _).mp hg
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_5
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousAdd α
a : α
f : ℤ → α
hf : HasSum f a
⊢ HasSum (fun n => f ↑n + f (-↑n)) (a + f 0)
[PROOFSTEP]
apply (hf.add (hasSum_ite_eq (0 : ℤ) (f 0))).hasSum_of_sum_eq fun u => ?_
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_5
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))
[PROOFSTEP]
refine' ⟨u.image Int.natAbs, fun v' hv' => _⟩
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_5
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))
[PROOFSTEP]
let u1 := v'.image fun x : ℕ => (x : ℤ)
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_5
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))
[PROOFSTEP]
let u2 := v'.image fun x : ℕ => -(x : ℤ)
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_5
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))
[PROOFSTEP]
have A : u ⊆ u1 ∪ u2 := by
  intro x hx
  simp only [mem_union, mem_image, exists_prop]
  rcases le_total 0 x with (h'x | h'x)
  · left
    refine' ⟨Int.natAbs x, hv' _, _⟩
    · simp only [mem_image, exists_prop]
      exact ⟨x, hx, rfl⟩
    · simp only [h'x, Int.coe_natAbs, abs_eq_self]
  · right
    refine' ⟨Int.natAbs x, hv' _, _⟩
    · simp only [mem_image, exists_prop]
      exact ⟨x, hx, rfl⟩
    · simp only [abs_of_nonpos h'x, Int.coe_natAbs, neg_neg]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_5
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
[PROOFSTEP]
intro x hx
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_5
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
[PROOFSTEP]
simp only [mem_union, mem_image, exists_prop]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_5
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
[PROOFSTEP]
rcases le_total 0 x with (h'x | h'x)
[GOAL]
case inl
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_5
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
[PROOFSTEP]
left
[GOAL]
case inl.h
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_5
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
[PROOFSTEP]
refine' ⟨Int.natAbs x, hv' _, _⟩
[GOAL]
case inl.h.refine'_1
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_5
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
[PROOFSTEP]
simp only [mem_image, exists_prop]
[GOAL]
case inl.h.refine'_1
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_5
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
[PROOFSTEP]
exact ⟨x, hx, rfl⟩
[GOAL]
case inl.h.refine'_2
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_5
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
[PROOFSTEP]
simp only [h'x, Int.coe_natAbs, abs_eq_self]
[GOAL]
case inr
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_5
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
[PROOFSTEP]
right
[GOAL]
case inr.h
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_5
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
[PROOFSTEP]
refine' ⟨Int.natAbs x, hv' _, _⟩
[GOAL]
case inr.h.refine'_1
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_5
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
[PROOFSTEP]
simp only [mem_image, exists_prop]
[GOAL]
case inr.h.refine'_1
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_5
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
[PROOFSTEP]
exact ⟨x, hx, rfl⟩
[GOAL]
case inr.h.refine'_2
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_5
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
[PROOFSTEP]
simp only [abs_of_nonpos h'x, Int.coe_natAbs, neg_neg]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_5
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))
[PROOFSTEP]
refine' ⟨u1 ∪ u2, A, _⟩
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_5
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))
[PROOFSTEP]
calc
  (∑ x in u1 ∪ u2, (f x + ite (x = 0) (f 0) 0)) = (∑ x in u1 ∪ u2, f x) + ∑ x in u1 ∩ u2, f x :=
    by
    rw [sum_add_distrib]
    congr 1
    refine' (sum_subset_zero_on_sdiff inter_subset_union _ _).symm
    · intro x hx
      suffices x ≠ 0 by simp only [this, if_false]
      rintro rfl
      simp at hx 
    · intro x hx
      simp only [mem_inter, mem_image, exists_prop] at hx 
      have : x = 0 := by
        apply le_antisymm
        · rcases hx.2 with ⟨a, _, rfl⟩
          simp only [Right.neg_nonpos_iff, Nat.cast_nonneg]
        · rcases hx.1 with ⟨a, _, rfl⟩
          simp only [Nat.cast_nonneg]
      simp only [this, eq_self_iff_true, if_true]
  _ = (∑ x in u1, f x) + ∑ x in u2, f x := sum_union_inter
  _ = (∑ b in v', f b) + ∑ b in v', f (-b) := by simp
  _ = ∑ b in v', (f b + f (-b)) := sum_add_distrib.symm
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_5
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
[PROOFSTEP]
rw [sum_add_distrib]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_5
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
[PROOFSTEP]
congr 1
[GOAL]
case e_a
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_5
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
[PROOFSTEP]
refine' (sum_subset_zero_on_sdiff inter_subset_union _ _).symm
[GOAL]
case e_a.refine'_1
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_5
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
[PROOFSTEP]
intro x hx
[GOAL]
case e_a.refine'_1
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_5
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
[PROOFSTEP]
suffices x ≠ 0 by simp only [this, if_false]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_5
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
[PROOFSTEP]
simp only [this, if_false]
[GOAL]
case e_a.refine'_1
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_5
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
[PROOFSTEP]
rintro rfl
[GOAL]
case e_a.refine'_1
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_5
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
[PROOFSTEP]
simp at hx 
[GOAL]
case e_a.refine'_2
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_5
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
[PROOFSTEP]
intro x hx
[GOAL]
case e_a.refine'_2
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_5
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
[PROOFSTEP]
simp only [mem_inter, mem_image, exists_prop] at hx 
[GOAL]
case e_a.refine'_2
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_5
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
[PROOFSTEP]
have : x = 0 := by
  apply le_antisymm
  · rcases hx.2 with ⟨a, _, rfl⟩
    simp only [Right.neg_nonpos_iff, Nat.cast_nonneg]
  · rcases hx.1 with ⟨a, _, rfl⟩
    simp only [Nat.cast_nonneg]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_5
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
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_5
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
[PROOFSTEP]
rcases hx.2 with ⟨a, _, rfl⟩
[GOAL]
case a.intro.intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝¹ a₁ a₂ : α✝
α : Type u_5
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
[PROOFSTEP]
simp only [Right.neg_nonpos_iff, Nat.cast_nonneg]
[GOAL]
case a
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_5
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
[PROOFSTEP]
rcases hx.1 with ⟨a, _, rfl⟩
[GOAL]
case a.intro.intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝¹ a₁ a₂ : α✝
α : Type u_5
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
[PROOFSTEP]
simp only [Nat.cast_nonneg]
[GOAL]
case e_a.refine'_2
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_5
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
[PROOFSTEP]
simp only [this, eq_self_iff_true, if_true]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : AddCommGroup α✝
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalAddGroup α✝
f✝ g : β → α✝
a✝ a₁ a₂ : α✝
α : Type u_5
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)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
⊢ (CauchySeq fun s => ∑ b in s, f b) ↔ ∀ (e : Set α), e ∈ 𝓝 0 → ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
[PROOFSTEP]
simp only [CauchySeq, cauchy_map_iff, and_iff_right atTop_neBot, prod_atTop_atTop_eq, uniformity_eq_comap_nhds_zero α,
  tendsto_comap_iff, (· ∘ ·), atTop_neBot, true_and]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
⊢ Tendsto (fun x => ∑ b in x.snd, f b - ∑ b in x.fst, f b) atTop (𝓝 0) ↔
    ∀ (e : Set α), e ∈ 𝓝 0 → ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
[PROOFSTEP]
rw [tendsto_atTop']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
⊢ (∀ (s : Set α), s ∈ 𝓝 0 → ∃ a, ∀ (b : Finset β × Finset β), b ≥ a → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ s) ↔
    ∀ (e : Set α), e ∈ 𝓝 0 → ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
⊢ (∀ (s : Set α), s ∈ 𝓝 0 → ∃ a, ∀ (b : Finset β × Finset β), b ≥ a → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ s) →
    ∀ (e : Set α), e ∈ 𝓝 0 → ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
[PROOFSTEP]
intro h e he
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
h : ∀ (s : Set α), s ∈ 𝓝 0 → ∃ a, ∀ (b : Finset β × Finset β), b ≥ a → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ s
e : Set α
he : e ∈ 𝓝 0
⊢ ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
[PROOFSTEP]
obtain ⟨⟨s₁, s₂⟩, h⟩ := h e he
[GOAL]
case mp.intro.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
h✝ : ∀ (s : Set α), s ∈ 𝓝 0 → ∃ a, ∀ (b : Finset β × Finset β), b ≥ a → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ s
e : Set α
he : e ∈ 𝓝 0
s₁ s₂ : Finset β
h : ∀ (b : Finset β × Finset β), b ≥ (s₁, s₂) → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ e
⊢ ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
[PROOFSTEP]
use s₁ ∪ s₂
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
h✝ : ∀ (s : Set α), s ∈ 𝓝 0 → ∃ a, ∀ (b : Finset β × Finset β), b ≥ a → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ s
e : Set α
he : e ∈ 𝓝 0
s₁ s₂ : Finset β
h : ∀ (b : Finset β × Finset β), b ≥ (s₁, s₂) → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ e
⊢ ∀ (t : Finset β), Disjoint t (s₁ ∪ s₂) → ∑ b in t, f b ∈ e
[PROOFSTEP]
intro t ht
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
h✝ : ∀ (s : Set α), s ∈ 𝓝 0 → ∃ a, ∀ (b : Finset β × Finset β), b ≥ a → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ s
e : Set α
he : e ∈ 𝓝 0
s₁ s₂ : Finset β
h : ∀ (b : Finset β × Finset β), b ≥ (s₁, s₂) → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ e
t : Finset β
ht : Disjoint t (s₁ ∪ s₂)
⊢ ∑ b in t, f b ∈ e
[PROOFSTEP]
specialize h (s₁ ∪ s₂, s₁ ∪ s₂ ∪ t) ⟨le_sup_left, le_sup_of_le_left le_sup_right⟩
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
h✝ : ∀ (s : Set α), s ∈ 𝓝 0 → ∃ a, ∀ (b : Finset β × Finset β), b ≥ a → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ s
e : Set α
he : e ∈ 𝓝 0
s₁ s₂ t : Finset β
ht : Disjoint t (s₁ ∪ s₂)
h : ∑ b in (s₁ ∪ s₂, s₁ ∪ s₂ ∪ t).snd, f b - ∑ b in (s₁ ∪ s₂, s₁ ∪ s₂ ∪ t).fst, f b ∈ e
⊢ ∑ b in t, f b ∈ e
[PROOFSTEP]
simpa only [Finset.sum_union ht.symm, add_sub_cancel'] using h
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
⊢ (∀ (e : Set α), e ∈ 𝓝 0 → ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e) →
    ∀ (s : Set α), s ∈ 𝓝 0 → ∃ a, ∀ (b : Finset β × Finset β), b ≥ a → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ s
[PROOFSTEP]
rintro h e he
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
h : ∀ (e : Set α), e ∈ 𝓝 0 → ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
e : Set α
he : e ∈ 𝓝 0
⊢ ∃ a, ∀ (b : Finset β × Finset β), b ≥ a → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ e
[PROOFSTEP]
rcases exists_nhds_half_neg he with ⟨d, hd, hde⟩
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
h : ∀ (e : Set α), e ∈ 𝓝 0 → ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
e : Set α
he : e ∈ 𝓝 0
d : Set α
hd : d ∈ 𝓝 0
hde : ∀ (v : α), v ∈ d → ∀ (w : α), w ∈ d → v - w ∈ e
⊢ ∃ a, ∀ (b : Finset β × Finset β), b ≥ a → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ e
[PROOFSTEP]
rcases h d hd with ⟨s, h⟩
[GOAL]
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
h✝ : ∀ (e : Set α), e ∈ 𝓝 0 → ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
e : Set α
he : e ∈ 𝓝 0
d : Set α
hd : d ∈ 𝓝 0
hde : ∀ (v : α), v ∈ d → ∀ (w : α), w ∈ d → v - w ∈ e
s : Finset β
h : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ d
⊢ ∃ a, ∀ (b : Finset β × Finset β), b ≥ a → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ e
[PROOFSTEP]
use(s, s)
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
h✝ : ∀ (e : Set α), e ∈ 𝓝 0 → ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
e : Set α
he : e ∈ 𝓝 0
d : Set α
hd : d ∈ 𝓝 0
hde : ∀ (v : α), v ∈ d → ∀ (w : α), w ∈ d → v - w ∈ e
s : Finset β
h : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ d
⊢ ∀ (b : Finset β × Finset β), b ≥ (s, s) → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ e
[PROOFSTEP]
rintro ⟨t₁, t₂⟩ ⟨ht₁, ht₂⟩
[GOAL]
case h.mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
h✝ : ∀ (e : Set α), e ∈ 𝓝 0 → ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
e : Set α
he : e ∈ 𝓝 0
d : Set α
hd : d ∈ 𝓝 0
hde : ∀ (v : α), v ∈ d → ∀ (w : α), w ∈ d → v - w ∈ e
s : Finset β
h : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ d
t₁ t₂ : Finset β
ht₁ : (s, s).fst ≤ (t₁, t₂).fst
ht₂ : (s, s).snd ≤ (t₁, t₂).snd
⊢ ∑ b in (t₁, t₂).snd, f b - ∑ b in (t₁, t₂).fst, f b ∈ e
[PROOFSTEP]
have : ((∑ b in t₂, f b) - ∑ b in t₁, f b) = (∑ b in t₂ \ s, f b) - ∑ b in t₁ \ s, f b := by
  rw [← Finset.sum_sdiff ht₁, ← Finset.sum_sdiff ht₂, add_sub_add_right_eq_sub]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
h✝ : ∀ (e : Set α), e ∈ 𝓝 0 → ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
e : Set α
he : e ∈ 𝓝 0
d : Set α
hd : d ∈ 𝓝 0
hde : ∀ (v : α), v ∈ d → ∀ (w : α), w ∈ d → v - w ∈ e
s : Finset β
h : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ d
t₁ t₂ : Finset β
ht₁ : (s, s).fst ≤ (t₁, t₂).fst
ht₂ : (s, s).snd ≤ (t₁, t₂).snd
⊢ ∑ b in t₂, f b - ∑ b in t₁, f b = ∑ b in t₂ \ s, f b - ∑ b in t₁ \ s, f b
[PROOFSTEP]
rw [← Finset.sum_sdiff ht₁, ← Finset.sum_sdiff ht₂, add_sub_add_right_eq_sub]
[GOAL]
case h.mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
h✝ : ∀ (e : Set α), e ∈ 𝓝 0 → ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
e : Set α
he : e ∈ 𝓝 0
d : Set α
hd : d ∈ 𝓝 0
hde : ∀ (v : α), v ∈ d → ∀ (w : α), w ∈ d → v - w ∈ e
s : Finset β
h : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ d
t₁ t₂ : Finset β
ht₁ : (s, s).fst ≤ (t₁, t₂).fst
ht₂ : (s, s).snd ≤ (t₁, t₂).snd
this : ∑ b in t₂, f b - ∑ b in t₁, f b = ∑ b in t₂ \ s, f b - ∑ b in t₁ \ s, f b
⊢ ∑ b in (t₁, t₂).snd, f b - ∑ b in (t₁, t₂).fst, f b ∈ e
[PROOFSTEP]
simp only [this]
[GOAL]
case h.mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
h✝ : ∀ (e : Set α), e ∈ 𝓝 0 → ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
e : Set α
he : e ∈ 𝓝 0
d : Set α
hd : d ∈ 𝓝 0
hde : ∀ (v : α), v ∈ d → ∀ (w : α), w ∈ d → v - w ∈ e
s : Finset β
h : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ d
t₁ t₂ : Finset β
ht₁ : (s, s).fst ≤ (t₁, t₂).fst
ht₂ : (s, s).snd ≤ (t₁, t₂).snd
this : ∑ b in t₂, f b - ∑ b in t₁, f b = ∑ b in t₂ \ s, f b - ∑ b in t₁ \ s, f b
⊢ ∑ b in t₂ \ s, f b - ∑ b in t₁ \ s, f b ∈ e
[PROOFSTEP]
exact hde _ (h _ Finset.sdiff_disjoint) _ (h _ Finset.sdiff_disjoint)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a a₁ a₂ : α
f : β → α
⊢ Tendsto (fun s => ∑' (b : { x // ¬x ∈ s }), f ↑b) atTop (𝓝 0)
[PROOFSTEP]
by_cases H : Summable f
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a a₁ a₂ : α
f : β → α
H : Summable f
⊢ Tendsto (fun s => ∑' (b : { x // ¬x ∈ s }), f ↑b) atTop (𝓝 0)
[PROOFSTEP]
intro e he
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a a₁ a₂ : α
f : β → α
H : Summable f
e : Set α
he : e ∈ 𝓝 0
⊢ e ∈ Filter.map (fun s => ∑' (b : { x // ¬x ∈ s }), f ↑b) atTop
[PROOFSTEP]
rcases exists_mem_nhds_isClosed_subset he with ⟨o, ho, o_closed, oe⟩
[GOAL]
case pos.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a a₁ a₂ : α
f : β → α
H : Summable f
e : Set α
he : e ∈ 𝓝 0
o : Set α
ho : o ∈ 𝓝 0
o_closed : IsClosed o
oe : o ⊆ e
⊢ e ∈ Filter.map (fun s => ∑' (b : { x // ¬x ∈ s }), f ↑b) atTop
[PROOFSTEP]
simp only [le_eq_subset, Set.mem_preimage, mem_atTop_sets, Filter.mem_map, ge_iff_le]
[GOAL]
case pos.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a a₁ a₂ : α
f : β → α
H : Summable f
e : Set α
he : e ∈ 𝓝 0
o : Set α
ho : o ∈ 𝓝 0
o_closed : IsClosed o
oe : o ⊆ e
⊢ ∃ a, ∀ (b : Finset β), a ⊆ b → ∑' (b_1 : { x // ¬x ∈ b }), f ↑b_1 ∈ e
[PROOFSTEP]
obtain ⟨s, hs⟩ : ∃ s : Finset β, ∀ t : Finset β, Disjoint t s → (∑ b : β in t, f b) ∈ o :=
  cauchySeq_finset_iff_vanishing.1 (Tendsto.cauchySeq H.hasSum) o ho
[GOAL]
case pos.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a a₁ a₂ : α
f : β → α
H : Summable f
e : Set α
he : e ∈ 𝓝 0
o : Set α
ho : o ∈ 𝓝 0
o_closed : IsClosed o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ o
⊢ ∃ a, ∀ (b : Finset β), a ⊆ b → ∑' (b_1 : { x // ¬x ∈ b }), f ↑b_1 ∈ e
[PROOFSTEP]
refine' ⟨s, fun a sa => oe _⟩
[GOAL]
case pos.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a✝ a₁ a₂ : α
f : β → α
H : Summable f
e : Set α
he : e ∈ 𝓝 0
o : Set α
ho : o ∈ 𝓝 0
o_closed : IsClosed o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ o
a : Finset β
sa : s ⊆ a
⊢ ∑' (b : { x // ¬x ∈ a }), f ↑b ∈ o
[PROOFSTEP]
have A : Summable fun b : { x // x ∉ a } => f b := a.summable_compl_iff.2 H
[GOAL]
case pos.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a✝ a₁ a₂ : α
f : β → α
H : Summable f
e : Set α
he : e ∈ 𝓝 0
o : Set α
ho : o ∈ 𝓝 0
o_closed : IsClosed o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ o
a : Finset β
sa : s ⊆ a
A : Summable fun b => f ↑b
⊢ ∑' (b : { x // ¬x ∈ a }), f ↑b ∈ o
[PROOFSTEP]
refine' IsClosed.mem_of_tendsto o_closed A.hasSum (eventually_of_forall fun b => _)
[GOAL]
case pos.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a✝ a₁ a₂ : α
f : β → α
H : Summable f
e : Set α
he : e ∈ 𝓝 0
o : Set α
ho : o ∈ 𝓝 0
o_closed : IsClosed o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ o
a : Finset β
sa : s ⊆ a
A : Summable fun b => f ↑b
b : Finset { x // ¬x ∈ a }
⊢ ∑ b in b, (fun b => f ↑b) b ∈ o
[PROOFSTEP]
have : Disjoint (Finset.image (fun i : { x // x ∉ a } => (i : β)) b) s :=
  by
  refine' disjoint_left.2 fun i hi his => _
  rcases mem_image.1 hi with ⟨i', _, rfl⟩
  exact i'.2 (sa his)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a✝ a₁ a₂ : α
f : β → α
H : Summable f
e : Set α
he : e ∈ 𝓝 0
o : Set α
ho : o ∈ 𝓝 0
o_closed : IsClosed o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ o
a : Finset β
sa : s ⊆ a
A : Summable fun b => f ↑b
b : Finset { x // ¬x ∈ a }
⊢ Disjoint (image (fun i => ↑i) b) s
[PROOFSTEP]
refine' disjoint_left.2 fun i hi his => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a✝ a₁ a₂ : α
f : β → α
H : Summable f
e : Set α
he : e ∈ 𝓝 0
o : Set α
ho : o ∈ 𝓝 0
o_closed : IsClosed o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ o
a : Finset β
sa : s ⊆ a
A : Summable fun b => f ↑b
b : Finset { x // ¬x ∈ a }
i : β
hi : i ∈ image (fun i => ↑i) b
his : i ∈ s
⊢ False
[PROOFSTEP]
rcases mem_image.1 hi with ⟨i', _, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a✝ a₁ a₂ : α
f : β → α
H : Summable f
e : Set α
he : e ∈ 𝓝 0
o : Set α
ho : o ∈ 𝓝 0
o_closed : IsClosed o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ o
a : Finset β
sa : s ⊆ a
A : Summable fun b => f ↑b
b : Finset { x // ¬x ∈ a }
i' : { x // ¬x ∈ a }
left✝ : i' ∈ b
hi : ↑i' ∈ image (fun i => ↑i) b
his : ↑i' ∈ s
⊢ False
[PROOFSTEP]
exact i'.2 (sa his)
[GOAL]
case pos.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a✝ a₁ a₂ : α
f : β → α
H : Summable f
e : Set α
he : e ∈ 𝓝 0
o : Set α
ho : o ∈ 𝓝 0
o_closed : IsClosed o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ o
a : Finset β
sa : s ⊆ a
A : Summable fun b => f ↑b
b : Finset { x // ¬x ∈ a }
this : Disjoint (image (fun i => ↑i) b) s
⊢ ∑ b in b, (fun b => f ↑b) b ∈ o
[PROOFSTEP]
convert hs _ this using 1
[GOAL]
case h.e'_4
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a✝ a₁ a₂ : α
f : β → α
H : Summable f
e : Set α
he : e ∈ 𝓝 0
o : Set α
ho : o ∈ 𝓝 0
o_closed : IsClosed o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ o
a : Finset β
sa : s ⊆ a
A : Summable fun b => f ↑b
b : Finset { x // ¬x ∈ a }
this : Disjoint (image (fun i => ↑i) b) s
⊢ ∑ b in b, (fun b => f ↑b) b = ∑ b in image (fun i => ↑i) b, f b
[PROOFSTEP]
rw [sum_image]
[GOAL]
case h.e'_4
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a✝ a₁ a₂ : α
f : β → α
H : Summable f
e : Set α
he : e ∈ 𝓝 0
o : Set α
ho : o ∈ 𝓝 0
o_closed : IsClosed o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ o
a : Finset β
sa : s ⊆ a
A : Summable fun b => f ↑b
b : Finset { x // ¬x ∈ a }
this : Disjoint (image (fun i => ↑i) b) s
⊢ ∀ (x : { x // ¬x ∈ a }), x ∈ b → ∀ (y : { x // ¬x ∈ a }), y ∈ b → ↑x = ↑y → x = y
[PROOFSTEP]
intro i _ j _ hij
[GOAL]
case h.e'_4
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a✝² a₁ a₂ : α
f : β → α
H : Summable f
e : Set α
he : e ∈ 𝓝 0
o : Set α
ho : o ∈ 𝓝 0
o_closed : IsClosed o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ o
a : Finset β
sa : s ⊆ a
A : Summable fun b => f ↑b
b : Finset { x // ¬x ∈ a }
this : Disjoint (image (fun i => ↑i) b) s
i : { x // ¬x ∈ a }
a✝¹ : i ∈ b
j : { x // ¬x ∈ a }
a✝ : j ∈ b
hij : ↑i = ↑j
⊢ i = j
[PROOFSTEP]
exact Subtype.ext hij
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a a₁ a₂ : α
f : β → α
H : ¬Summable f
⊢ Tendsto (fun s => ∑' (b : { x // ¬x ∈ s }), f ↑b) atTop (𝓝 0)
[PROOFSTEP]
convert tendsto_const_nhds (α := α) (β := Finset β) (f := atTop) (a := 0)
[GOAL]
case h.e'_3.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a a₁ a₂ : α
f : β → α
H : ¬Summable f
x✝ : Finset β
⊢ ∑' (b : { x // ¬x ∈ x✝ }), f ↑b = 0
[PROOFSTEP]
apply tsum_eq_zero_of_not_summable
[GOAL]
case h.e'_3.h.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a a₁ a₂ : α
f : β → α
H : ¬Summable f
x✝ : Finset β
⊢ ¬Summable fun b => f ↑b
[PROOFSTEP]
rwa [Finset.summable_compl_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommGroup α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
inst✝ : CompleteSpace α
⊢ Summable f ↔ ∀ (e : Set α), e ∈ 𝓝 0 → ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
[PROOFSTEP]
rw [summable_iff_cauchySeq_finset, cauchySeq_finset_iff_vanishing]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommGroup α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
inst✝ : CompleteSpace α
hf : Summable f
h : ∀ (b : β), g b = 0 ∨ g b = f b
e : Set α
he : e ∈ 𝓝 0
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
t : Finset β
ht : Disjoint t s
⊢ ∑ b in filter (fun b => g b = f b) t, g b = ∑ b in t, g b
[PROOFSTEP]
{ refine' Finset.sum_subset (Finset.filter_subset _ _) _
  intro b hbt hb
  simp only [Finset.mem_filter, and_iff_right hbt] at hb 
  exact (h b).resolve_right hb
}
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommGroup α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
inst✝ : CompleteSpace α
hf : Summable f
h : ∀ (b : β), g b = 0 ∨ g b = f b
e : Set α
he : e ∈ 𝓝 0
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
t : Finset β
ht : Disjoint t s
⊢ ∑ b in filter (fun b => g b = f b) t, g b = ∑ b in t, g b
[PROOFSTEP]
refine' Finset.sum_subset (Finset.filter_subset _ _) _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommGroup α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
inst✝ : CompleteSpace α
hf : Summable f
h : ∀ (b : β), g b = 0 ∨ g b = f b
e : Set α
he : e ∈ 𝓝 0
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
t : Finset β
ht : Disjoint t s
⊢ ∀ (x : β), x ∈ t → ¬x ∈ filter (fun b => g b = f b) t → g x = 0
[PROOFSTEP]
intro b hbt hb
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommGroup α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
inst✝ : CompleteSpace α
hf : Summable f
h : ∀ (b : β), g b = 0 ∨ g b = f b
e : Set α
he : e ∈ 𝓝 0
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
t : Finset β
ht : Disjoint t s
b : β
hbt : b ∈ t
hb : ¬b ∈ filter (fun b => g b = f b) t
⊢ g b = 0
[PROOFSTEP]
simp only [Finset.mem_filter, and_iff_right hbt] at hb 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommGroup α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
inst✝ : CompleteSpace α
hf : Summable f
h : ∀ (b : β), g b = 0 ∨ g b = f b
e : Set α
he : e ∈ 𝓝 0
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
t : Finset β
ht : Disjoint t s
b : β
hbt : b ∈ t
hb : ¬g b = f b
⊢ g b = 0
[PROOFSTEP]
exact (h b).resolve_right hb
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommGroup α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
inst✝ : CompleteSpace α
i : γ → β
hf : Summable f
hi : Injective i
⊢ Summable (f ∘ i)
[PROOFSTEP]
simpa only [Set.indicator_range_comp] using
  (hi.summable_iff (fun x hx => Set.indicator_of_not_mem hx _)).2 (hf.indicator (Set.range i))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommGroup α
inst✝³ : UniformSpace α
inst✝² : UniformAddGroup α
f✝ g : β → α
a a₁ a₂ : α
inst✝¹ : CompleteSpace α
inst✝ : T2Space α
f : β → α
hf : Summable f
s : Finset β
⊢ ∑ x in s, f x + ∑' (x : { x // ¬x ∈ s }), f ↑x = ∑' (x : β), f x
[PROOFSTEP]
rw [← tsum_subtype_add_tsum_subtype_compl hf s]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommGroup α
inst✝³ : UniformSpace α
inst✝² : UniformAddGroup α
f✝ g : β → α
a a₁ a₂ : α
inst✝¹ : CompleteSpace α
inst✝ : T2Space α
f : β → α
hf : Summable f
s : Finset β
⊢ ∑ x in s, f x + ∑' (x : { x // ¬x ∈ s }), f ↑x = ∑' (x : ↑↑s), f ↑x + ∑' (x : ↑(↑s)ᶜ), f ↑x
[PROOFSTEP]
simp only [Finset.tsum_subtype', add_right_inj]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommGroup α
inst✝³ : UniformSpace α
inst✝² : UniformAddGroup α
f✝ g : β → α
a a₁ a₂ : α
inst✝¹ : CompleteSpace α
inst✝ : T2Space α
f : β → α
hf : Summable f
s : Finset β
⊢ ∑' (x : { x // ¬x ∈ s }), f ↑x = ∑' (x : ↑(↑s)ᶜ), f ↑x
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝² : TopologicalSpace G
inst✝¹ : AddCommGroup G
inst✝ : TopologicalAddGroup G
f : α → G
hf : Summable f
e : Set G
he : e ∈ 𝓝 0
⊢ ∃ s, ∀ (t : Finset α), Disjoint t s → ∑ k in t, f k ∈ e
[PROOFSTEP]
letI : UniformSpace G := TopologicalAddGroup.toUniformSpace G
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝² : TopologicalSpace G
inst✝¹ : AddCommGroup G
inst✝ : TopologicalAddGroup G
f : α → G
hf : Summable f
e : Set G
he : e ∈ 𝓝 0
this : UniformSpace G := TopologicalAddGroup.toUniformSpace G
⊢ ∃ s, ∀ (t : Finset α), Disjoint t s → ∑ k in t, f k ∈ e
[PROOFSTEP]
letI : UniformAddGroup G := comm_topologicalAddGroup_is_uniform
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝² : TopologicalSpace G
inst✝¹ : AddCommGroup G
inst✝ : TopologicalAddGroup G
f : α → G
hf : Summable f
e : Set G
he : e ∈ 𝓝 0
this✝ : UniformSpace G := TopologicalAddGroup.toUniformSpace G
this : UniformAddGroup G := comm_topologicalAddGroup_is_uniform
⊢ ∃ s, ∀ (t : Finset α), Disjoint t s → ∑ k in t, f k ∈ e
[PROOFSTEP]
rcases hf with ⟨y, hy⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝² : TopologicalSpace G
inst✝¹ : AddCommGroup G
inst✝ : TopologicalAddGroup G
f : α → G
e : Set G
he : e ∈ 𝓝 0
this✝ : UniformSpace G := TopologicalAddGroup.toUniformSpace G
this : UniformAddGroup G := comm_topologicalAddGroup_is_uniform
y : G
hy : HasSum f y
⊢ ∃ s, ∀ (t : Finset α), Disjoint t s → ∑ k in t, f k ∈ e
[PROOFSTEP]
exact cauchySeq_finset_iff_vanishing.1 hy.cauchySeq e he
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝² : TopologicalSpace G
inst✝¹ : AddCommGroup G
inst✝ : TopologicalAddGroup G
f : α → G
hf : Summable f
⊢ Tendsto f cofinite (𝓝 0)
[PROOFSTEP]
intro e he
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝² : TopologicalSpace G
inst✝¹ : AddCommGroup G
inst✝ : TopologicalAddGroup G
f : α → G
hf : Summable f
e : Set G
he : e ∈ 𝓝 0
⊢ e ∈ Filter.map f cofinite
[PROOFSTEP]
rw [Filter.mem_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝² : TopologicalSpace G
inst✝¹ : AddCommGroup G
inst✝ : TopologicalAddGroup G
f : α → G
hf : Summable f
e : Set G
he : e ∈ 𝓝 0
⊢ f ⁻¹' e ∈ cofinite
[PROOFSTEP]
rcases hf.vanishing he with ⟨s, hs⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝² : TopologicalSpace G
inst✝¹ : AddCommGroup G
inst✝ : TopologicalAddGroup G
f : α → G
hf : Summable f
e : Set G
he : e ∈ 𝓝 0
s : Finset α
hs : ∀ (t : Finset α), Disjoint t s → ∑ k in t, f k ∈ e
⊢ f ⁻¹' e ∈ cofinite
[PROOFSTEP]
refine' s.eventually_cofinite_nmem.mono fun x hx => _
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝² : TopologicalSpace G
inst✝¹ : AddCommGroup G
inst✝ : TopologicalAddGroup G
f : α → G
hf : Summable f
e : Set G
he : e ∈ 𝓝 0
s : Finset α
hs : ∀ (t : Finset α), Disjoint t s → ∑ k in t, f k ∈ e
x : α
hx : ¬x ∈ s
⊢ f x ∈ e
[PROOFSTEP]
simpa using hs { x } (disjoint_singleton_left.2 hx)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝² : TopologicalSpace G
inst✝¹ : AddCommGroup G
inst✝ : TopologicalAddGroup G
f✝ : α → G
f : ℕ → G
hf : Summable f
⊢ Tendsto f atTop (𝓝 0)
[PROOFSTEP]
rw [← Nat.cofinite_eq_atTop]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝² : TopologicalSpace G
inst✝¹ : AddCommGroup G
inst✝ : TopologicalAddGroup G
f✝ : α → G
f : ℕ → G
hf : Summable f
⊢ Tendsto f cofinite (𝓝 0)
[PROOFSTEP]
exact hf.tendsto_cofinite_zero
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝⁴ : TopologicalSpace G
inst✝³ : AddCommGroup G
inst✝² : TopologicalAddGroup G
f : α → G
inst✝¹ : TopologicalSpace.FirstCountableTopology G
inst✝ : T1Space G
hf : Summable f
⊢ Set.Countable (support f)
[PROOFSTEP]
simpa only [sInter_sets_nhds] using hf.tendsto_cofinite_zero.countable_compl_preimage_sInter_sets
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : AddCommMonoid γ
inst✝ : TopologicalSpace γ
f : β → α
g : β → γ
a : α
b : γ
hf : HasSum f a
hg : HasSum g b
⊢ HasSum (fun x => (f x, g x)) (a, b)
[PROOFSTEP]
simp [HasSum, ← prod_mk_sum, Filter.Tendsto.prod_mk_nhds hf hg]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
π : α → Type u_6
inst✝¹ : (x : α) → AddCommMonoid (π x)
inst✝ : (x : α) → TopologicalSpace (π x)
f : ι → (x : α) → π x
g : (x : α) → π x
⊢ HasSum f g ↔ ∀ (x : α), HasSum (fun i => f i x) (g x)
[PROOFSTEP]
simp only [HasSum, tendsto_pi_nhds, sum_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
π : α → Type u_6
inst✝¹ : (x : α) → AddCommMonoid (π x)
inst✝ : (x : α) → TopologicalSpace (π x)
f : ι → (x : α) → π x
⊢ Summable f ↔ ∀ (x : α), Summable fun i => f i x
[PROOFSTEP]
simp only [Summable, Pi.hasSum, skolem]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
a : α
inst✝ : T2Space α
⊢ ∑' (x : β), op (f x) = op (∑' (x : β), f x)
[PROOFSTEP]
by_cases h : Summable f
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
a : α
inst✝ : T2Space α
h : Summable f
⊢ ∑' (x : β), op (f x) = op (∑' (x : β), f x)
[PROOFSTEP]
exact h.hasSum.op.tsum_eq
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
a : α
inst✝ : T2Space α
h : ¬Summable f
⊢ ∑' (x : β), op (f x) = op (∑' (x : β), f x)
[PROOFSTEP]
have ho := summable_op.not.mpr h
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
a : α
inst✝ : T2Space α
h : ¬Summable f
ho : ¬Summable fun a => op (f a)
⊢ ∑' (x : β), op (f x) = op (∑' (x : β), f x)
[PROOFSTEP]
rw [tsum_eq_zero_of_not_summable h, tsum_eq_zero_of_not_summable ho, MulOpposite.op_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : StarAddMonoid α
inst✝ : ContinuousStar α
f : β → α
a : α
h : HasSum f a
⊢ HasSum (fun b => Star.star (f b)) (Star.star a)
[PROOFSTEP]
simpa only using h.map (starAddEquiv : α ≃+ α) continuous_star
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : StarAddMonoid α
inst✝ : ContinuousStar α
f : β → α
a : α
hf : Summable fun b => Star.star (f b)
⊢ Summable f
[PROOFSTEP]
simpa only [star_star] using hf.star
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : StarAddMonoid α
inst✝¹ : ContinuousStar α
f : β → α
a : α
inst✝ : T2Space α
⊢ star (∑' (b : β), f b) = ∑' (b : β), star (f b)
[PROOFSTEP]
by_cases hf : Summable f
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : StarAddMonoid α
inst✝¹ : ContinuousStar α
f : β → α
a : α
inst✝ : T2Space α
hf : Summable f
⊢ star (∑' (b : β), f b) = ∑' (b : β), star (f b)
[PROOFSTEP]
exact hf.hasSum.star.tsum_eq.symm
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : StarAddMonoid α
inst✝¹ : ContinuousStar α
f : β → α
a : α
inst✝ : T2Space α
hf : ¬Summable f
⊢ star (∑' (b : β), f b) = ∑' (b : β), star (f b)
[PROOFSTEP]
rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable (mt Summable.ofStar hf), star_zero]
