obtain ⟨lf, hlf1, hlf2⟩ := hp (deriv f / f) ((hf.deriv hU).div hf hfz)
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
case intro.intro.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
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
⊢ ∃ g, DifferentiableOn ℂ g U ∧ EqOn f (cexp ∘ g) U