rintro f hfz hf
z z₀ : ℂ
U : Set ℂ
h : has_logs U
⊢ _root_.has_sqrt U
z z₀ : ℂ
U : Set ℂ
h : has_logs U
f : ℂ → ℂ
hfz : ∀ z ∈ U, f z ≠ 0
hf : DifferentiableOn ℂ f U
⊢ ∃ g, DifferentiableOn ℂ g U ∧ EqOn f (g ^ 2) U