refine (hG (1 + t * I) (by simp)).tendsto.comp <| tendsto_nhdsWithin_iff.mpr ⟨?_, ?_⟩
case neg.intro.intro.intro.h_lim.hp.h.h
n : ℕ
A a b c d u x y t✝ σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
t : ℝ
⊢ Tendsto (fun k => G (↑k + ↑t * I)) (𝓝[>] 1) (𝓝 (G (1 + ↑t * I)))
case neg.intro.intro.intro.h_lim.hp.h.h.refine_1
n : ℕ
A a b c d u x y t✝ σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
t : ℝ
⊢ Tendsto (fun k => ↑k + ↑t * I) (𝓝[>] 1) (𝓝 (1 + ↑t * I))

case neg.intro.intro.intro.h_lim.hp.h.h.refine_2
n : ℕ
A a b c d u x y t✝ σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
t : ℝ
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 1, ↑n + ↑t * I ∈ {s | 1 ≤ s.re}