rw [hz.symm.symm]
case h.a
f g : ℂ → ℂ
z✝ z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f 0 z₀
R : ℝ
hR : R > 0
hf : ∀ ⦃y : ℂ⦄, dist y z₀ < R → f y = 0
r : ℝ
hr : r ∈ Set.Ioo 0 R
z : ℂ
hz : z ∈ sphere z₀ r
⊢ dist z z₀ < R
case h.a
f g : ℂ → ℂ
z✝ z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f 0 z₀
R : ℝ
hR : R > 0
hf : ∀ ⦃y : ℂ⦄, dist y z₀ < R → f y = 0
r : ℝ
hr : r ∈ Set.Ioo 0 R
z : ℂ
hz : z ∈ sphere z₀ r
⊢ r < R