case neg =>
  obtain ⟨z₀, hz₀⟩ := nonempty_iff_ne_empty.2 h
  rintro f hf hfz
  obtain ⟨lf, hlf1, hlf2⟩ := hp (deriv f / f) ((hf.deriv hU).div hf hfz)
  let g : ℂ → ℂ := λ z => lf z + (log (f z₀) - lf z₀)
  set h : ℂ → ℂ := f / (exp ∘ g)
  have h3 : DifferentiableOn ℂ g U := hlf1.add (differentiableOn_const _)
  have e4 : DifferentiableOn ℂ (exp ∘ g) U := differentiable_exp.comp_differentiableOn h3
  have e1 : DifferentiableOn ℂ h U := hf.div e4 (λ z _ => exp_ne_zero _)
  refine ⟨g, h3, ?_⟩
  suffices h : EqOn h (λ _ => 1) U
    by exact λ z hz => eq_of_div_eq_one (h hz)
  have : 1 = h z₀ := by unfold_let ; simp [exp_log, hfz z₀ hz₀]
  rw [this]
  refine EqOn_of_deriv_eq_zero hU hU' e1 (λ z hz => ?_) hz₀
  have f0 : U ∈ 𝓝 z := hU.mem_nhds hz
  dsimp
  unfold_let
  rw [Pi.div_def, deriv_div (hf.differentiableAt f0) (e4.differentiableAt f0) (exp_ne_zero _)]
  rw [deriv.scomp z differentiableAt_exp (h3.differentiableAt f0)]
  have e5 : deriv g z = deriv lf z := by unfold_let ; simp
  field_simp [exp_ne_zero, hlf2 hz, hfz z hz, e5]
  ring
z z₀ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h : ¬U = ∅
⊢ _root_.has_logs U
no goals