Theorem: zeroTendstoDiff (PrimeNumberTheoremAnd/PerronFormula.lean)

State before:
L₁ L₂ : ℂ
f : ℝ → ℂ
h : ∀ᶠ (T : ℝ) in atTop, f T = 0
h' : Tendsto f atTop (𝓝 (L₂ - L₁))
⊢ L₁ = L₂
Tactic:
rw [← zero_add L₁, ← @eq_sub_iff_add_eq]
State after:
L₁ L₂ : ℂ
f : ℝ → ℂ
h : ∀ᶠ (T : ℝ) in atTop, f T = 0
h' : Tendsto f atTop (𝓝 (L₂ - L₁))
⊢ 0 = L₂ - L₁

State before:
L₁ L₂ : ℂ
f : ℝ → ℂ
h : ∀ᶠ (T : ℝ) in atTop, f T = 0
h' : Tendsto f atTop (𝓝 (L₂ - L₁))
⊢ 0 = L₂ - L₁
Tactic:
exact tendsto_nhds_unique (EventuallyEq.tendsto h) h'
State after:
no goals