have := eventuallyEq_of_mem (mem_atTop σ) fun σ' h ↦ ha σ' σ (σpos.trans_le h) σpos
a : ℝ → ℂ
σ : ℝ
σpos : 0 < σ
ha : ∀ (σ' σ'' : ℝ), 0 < σ' → 0 < σ'' → a σ' = a σ''
ha' : Tendsto a atTop (𝓝 0)
⊢ a σ = 0
a : ℝ → ℂ
σ : ℝ
σpos : 0 < σ
ha : ∀ (σ' σ'' : ℝ), 0 < σ' → 0 < σ'' → a σ' = a σ''
ha' : Tendsto a atTop (𝓝 0)
this : (fun σ' => a σ') =ᶠ[atTop] fun σ' => a σ
⊢ a σ = 0