refine' ENat.Tendsto.const_mul tendsto_id (Or.inl _)
case neg
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s : Set α
n : ℕ∞
ι : Sort u_4
c : ℕ∞
f : ι → ℕ∞
hf : ¬∀ (i : ι), f i = 0
⊢ ContinuousAt (fun x => c * id x) (⨆ i, f i)
case neg
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s : Set α
n : ℕ∞
ι : Sort u_4
c : ℕ∞
f : ι → ℕ∞
hf : ¬∀ (i : ι), f i = 0
⊢ id (⨆ i, f i) ≠ 0