Theorem: limitOfConstantLeft (PrimeNumberTheoremAnd/PerronFormula.lean)

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

State before:
a : ℝ → ℂ
σ : ℝ
σlt : σ ≤ -3 / 2
ha : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → a σ' = a σ''
ha' : Tendsto a atBot (𝓝 0)
this : (fun σ' => a σ') =ᶠ[atBot] fun σ' => a σ
⊢ a σ = 0
Tactic:
exact tendsto_const_nhds_iff.mp (ha'.congr' this)
State after:
no goals