by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)
differential-calculusproofwiki
Let \mapjx,\mapkx be real functions defined on the open interval I. Let ξ∈I be a point in I at which both j and k are differentiable. Define the real function f on I by \mapfx=⎩⎨⎧\mapkx\mapjx0:\mapkx=0:otherwise Then, if \mapkξ=0, f is differentiable at ξ, and furthermore \mapf′ξ=\paren\mapkξ2\mapj′ξ\mapkξ−\mapjξ\mapk′ξ It follows from the definition of derivative that if j and k are both differentiable on the interval I, then ∀x∈I:\mapkx=0⟹\mapf′x=\paren\mapkx2\mapj′x\mapkx−\mapjx\mapk′x
import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.Calculus.Deriv.Basic
theorem Quotient_Rule_for_Derivatives (f g : ℝ → ℝ) (x : ℝ) (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) (hgx : g x ≠ 0) : HasDerivAt (fun x => f x / g x) ((deriv f x * g x - f x * deriv g x) / g x ^ 2) x := by sorry