∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {R₁ R₂ : ℝ} {f : ℂ → E} {c z₀ : ℂ}
  [StrictConvexSpace ℝ E],
  DifferentiableOn ℂ f (Metric.ball c R₁) →
    Set.MapsTo f (Metric.ball c R₁) (Metric.closedBall (f c) R₂) →
      z₀ ∈ Metric.ball c R₁ →
        ‖dslope f c z₀‖ = R₂ / R₁ → Set.EqOn f (fun z => f c + (z - c) • dslope f c z₀) (Metric.ball c R₁)