exact λ z hz => eq_of_div_eq_one (h hz)
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 : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h✝ : ℂ → ℂ := f / cexp ∘ g
h3 : DifferentiableOn ℂ g U
e4 : DifferentiableOn ℂ (cexp ∘ g) U
e1 : DifferentiableOn ℂ h✝ U
h : EqOn h✝ (fun x => 1) U
⊢ EqOn f (cexp ∘ g) U
no goals