obtain ⟨z₀, hz₀⟩ := nonempty_iff_ne_empty.2 h
z z₀ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h : ¬U = ∅
⊢ _root_.has_logs U
case intro
z z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
⊢ _root_.has_logs U