rw [Pi.pow_apply, h, zero_pow two_ne_zero] at this
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
e1 : U ∈ 𝓝 z₀
e2 : AnalyticAt ℂ g z₀
f_eq_comp : ∀ᶠ (x : ℂ) in 𝓝 z₀, f x = (g ^ 2) x
e3 : deriv (fun z => g z) z₀ = deriv (fun z => f z) z₀ / (↑2 * g z₀ ^ (2 - 1))
h : g z₀ = 0
this : f z₀ = (g ^ 2) z₀
⊢ False
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
e1 : U ∈ 𝓝 z₀
e2 : AnalyticAt ℂ g z₀
f_eq_comp : ∀ᶠ (x : ℂ) in 𝓝 z₀, f x = (g ^ 2) x
e3 : deriv (fun z => g z) z₀ = deriv (fun z => f z) z₀ / (↑2 * g z₀ ^ (2 - 1))
h : g z₀ = 0
this : f z₀ = 0
⊢ False