have := eventuallyEq_of_mem (mem_atBot (-3/2)) fun σ' h ↦ ha σ' σ h σlt
a : ℝ → ℂ
σ : ℝ
σlt : σ ≤ -3 / 2
ha : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → a σ' = a σ''
ha' : Tendsto a atBot (𝓝 0)
⊢ a σ = 0
a : ℝ → ℂ
σ : ℝ
σlt : σ ≤ -3 / 2
ha : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → a σ' = a σ''
ha' : Tendsto a atBot (𝓝 0)
this : (fun σ' => a σ') =ᶠ[atBot] fun σ' => a σ
⊢ a σ = 0