Theorem: limitOfConstant (PrimeNumberTheoremAnd/PerronFormula.lean)

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

State before:
a : ℝ → ℂ
σ : ℝ
σpos : 0 < σ
ha : ∀ (σ' σ'' : ℝ), 0 < σ' → 0 < σ'' → a σ' = a σ''
ha' : Tendsto a atTop (𝓝 0)
this : (fun σ' => a σ') =ᶠ[atTop] fun σ' => a σ
⊢ a σ = 0
Tactic:
exact tendsto_const_nhds_iff.mp (ha'.congr' this)
State after:
no goals