by_cases h : U = ∅
z z₀ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
⊢ _root_.has_logs U
case pos
z z₀ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h : U = ∅
⊢ _root_.has_logs U

case neg
z z₀ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h : ¬U = ∅
⊢ _root_.has_logs U