obtain ⟨c, U, hU, V, hV, h⟩ := this
this : ∃ c, ∀ᶠ (x : ℝ) in 𝓝[>] 1, ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
case intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)