refine ⟨λ z => exp (l z / 2), differentiable_exp.comp_differentiableOn (hl.div_const _), λ z hz => ?_⟩
case intro.intro
z z₀ : ℂ
U : Set ℂ
h : has_logs U
f : ℂ → ℂ
hfz : ∀ z ∈ U, f z ≠ 0
hf : DifferentiableOn ℂ f U
l : ℂ → ℂ
hl : DifferentiableOn ℂ l U
hlf : EqOn f (cexp ∘ l) U
⊢ ∃ g, DifferentiableOn ℂ g U ∧ EqOn f (g ^ 2) U
case intro.intro
z✝ z₀ : ℂ
U : Set ℂ
h : has_logs U
f : ℂ → ℂ
hfz : ∀ z ∈ U, f z ≠ 0
hf : DifferentiableOn ℂ f U
l : ℂ → ℂ
hl : DifferentiableOn ℂ l U
hlf : EqOn f (cexp ∘ l) U
z : ℂ
hz : z ∈ U
⊢ f z = ((fun z => cexp (l z / 2)) ^ 2) z