case refine'_1
ι : Type u_2
κ : Type ?u.35269
α : Type u_1
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
hf : ∀ (i : ι), 0 ≤ f i
hf' : HasSum f 0
⊢ f = 0

case refine'_2
ι : Type u_2
κ : Type ?u.35269
α : Type u_1
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
hf : ∀ (i : ι), 0 ≤ f i
⊢ f = 0 → HasSum f 0
ι : Type u_2
κ : Type ?u.35269
α : Type u_1
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
hf : ∀ (i : ι), 0 ≤ f i
⊢ HasSum f 0 ↔ f = 0
refine' ⟨fun hf' => _, _⟩
case refine'_1.h
ι : Type u_2
κ : Type ?u.35269
α : Type u_1
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
hf : ∀ (i : ι), 0 ≤ f i
hf' : HasSum f 0
i : ι
⊢ f i = OfNat.ofNat 0 i
case refine'_1
ι : Type u_2
κ : Type ?u.35269
α : Type u_1
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
hf : ∀ (i : ι), 0 ≤ f i
hf' : HasSum f 0
⊢ f = 0
ext i
no goals
case refine'_1.h
ι : Type u_2
κ : Type ?u.35269
α : Type u_1
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
hf : ∀ (i : ι), 0 ≤ f i
hf' : HasSum f 0
i : ι
⊢ f i = OfNat.ofNat 0 i
exact (hf i).antisymm' (le_hasSum hf' _ fun j _ => hf j)
case refine'_2
ι : Type u_2
κ : Type ?u.35269
α : Type u_1
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
g : ι → α
a a₁ a₂ : α
hf : ∀ (i : ι), 0 ≤ OfNat.ofNat 0 i
⊢ HasSum 0 0
case refine'_2
ι : Type u_2
κ : Type ?u.35269
α : Type u_1
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
hf : ∀ (i : ι), 0 ≤ f i
⊢ f = 0 → HasSum f 0
rintro rfl
no goals
case refine'_2
ι : Type u_2
κ : Type ?u.35269
α : Type u_1
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
g : ι → α
a a₁ a₂ : α
hf : ∀ (i : ι), 0 ≤ OfNat.ofNat 0 i
⊢ HasSum 0 0
exact hasSum_zero