rintro f hf hfz
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
case intro
z z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
⊢ ∃ g, DifferentiableOn ℂ g U ∧ EqOn f (cexp ∘ g) U