no goals
α : Type u_1
β : Type u_2
γ : Type ?u.304545
δ : Type ?u.304548
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
hz : IsClosed {0}
⊢ (∑' (x : β), 0) = 0
classical
  rw [tsum_def, dif_pos summable_zero]
  suffices ∀ x : α, HasSum (fun _ : β => (0 : α)) x → x = 0 by
    exact this _ (Classical.choose_spec _)
  intro x hx
  contrapose! hx
  simp only [HasSum, tendsto_nhds, Finset.sum_const_zero, Filter.mem_atTop_sets, ge_iff_le,
    Finset.le_eq_subset, Set.mem_preimage, not_forall, not_exists, exists_prop, exists_and_right]
  refine ⟨{0}ᶜ, ⟨isOpen_compl_iff.mpr hz, by simpa [hx] using fun x ↦ ⟨x, subset_refl _⟩⟩⟩
α : Type u_1
β : Type u_2
γ : Type ?u.304545
δ : Type ?u.304548
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
hz : IsClosed {0}
⊢ Classical.choose (_ : Summable fun x => 0) = 0
α : Type u_1
β : Type u_2
γ : Type ?u.304545
δ : Type ?u.304548
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
hz : IsClosed {0}
⊢ (∑' (x : β), 0) = 0
rw [tsum_def, dif_pos summable_zero]
α : Type u_1
β : Type u_2
γ : Type ?u.304545
δ : Type ?u.304548
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
hz : IsClosed {0}
⊢ ∀ (x : α), HasSum (fun x => 0) x → x = 0
α : Type u_1
β : Type u_2
γ : Type ?u.304545
δ : Type ?u.304548
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
hz : IsClosed {0}
⊢ Classical.choose (_ : Summable fun x => 0) = 0
suffices ∀ x : α, HasSum (fun _ : β => (0 : α)) x → x = 0 by
  exact this _ (Classical.choose_spec _)
α : Type u_1
β : Type u_2
γ : Type ?u.304545
δ : Type ?u.304548
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
hz : IsClosed {0}
x : α
hx : HasSum (fun x => 0) x
⊢ x = 0
α : Type u_1
β : Type u_2
γ : Type ?u.304545
δ : Type ?u.304548
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
hz : IsClosed {0}
⊢ ∀ (x : α), HasSum (fun x => 0) x → x = 0
intro x hx
α : Type u_1
β : Type u_2
γ : Type ?u.304545
δ : Type ?u.304548
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
hz : IsClosed {0}
x : α
hx : x ≠ 0
⊢ ¬HasSum (fun x => 0) x
α : Type u_1
β : Type u_2
γ : Type ?u.304545
δ : Type ?u.304548
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
hz : IsClosed {0}
x : α
hx : HasSum (fun x => 0) x
⊢ x = 0
contrapose! hx
α : Type u_1
β : Type u_2
γ : Type ?u.304545
δ : Type ?u.304548
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
hz : IsClosed {0}
x : α
hx : x ≠ 0
⊢ ∃ x_1, IsOpen x_1 ∧ x ∈ x_1 ∧ ∀ (x : Finset β), (∃ x_2, x ⊆ x_2) ∧ ¬0 ∈ x_1
α : Type u_1
β : Type u_2
γ : Type ?u.304545
δ : Type ?u.304548
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
hz : IsClosed {0}
x : α
hx : x ≠ 0
⊢ ¬HasSum (fun x => 0) x
simp only [HasSum, tendsto_nhds, Finset.sum_const_zero, Filter.mem_atTop_sets, ge_iff_le,
  Finset.le_eq_subset, Set.mem_preimage, not_forall, not_exists, exists_prop, exists_and_right]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.304545
δ : Type ?u.304548
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
hz : IsClosed {0}
x : α
hx : x ≠ 0
⊢ ∃ x_1, IsOpen x_1 ∧ x ∈ x_1 ∧ ∀ (x : Finset β), (∃ x_2, x ⊆ x_2) ∧ ¬0 ∈ x_1
refine ⟨{0}ᶜ, ⟨isOpen_compl_iff.mpr hz, by simpa [hx] using fun x ↦ ⟨x, subset_refl _⟩⟩⟩
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.304545
δ : Type ?u.304548
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
hz : IsClosed {0}
this : ∀ (x : α), HasSum (fun x => 0) x → x = 0
⊢ Classical.choose (_ : Summable fun x => 0) = 0
exact this _ (Classical.choose_spec _)
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.304545
δ : Type ?u.304548
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
hz : IsClosed {0}
x : α
hx : x ≠ 0
⊢ x ∈ {0}ᶜ ∧ ∀ (x : Finset β), (∃ x_1, x ⊆ x_1) ∧ ¬0 ∈ {0}ᶜ
simpa [hx] using fun x ↦ ⟨x, subset_refl _⟩