have h : ∀ (f : R → K) x, fderiv R f x 1 = deriv f x := by simp[deriv]
K : Type u_2
inst✝¹¹ : RCLike K
X : Type ?u.170248
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace K X
Y : Type ?u.170390
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace K Y
Z : Type ?u.170525
inst✝⁶ : NormedAddCommGroup Z
inst✝⁵ : NormedSpace K Z
ι : Type ?u.170660
inst✝⁴ : Fintype ι
E : ι → Type ?u.170668
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace K (E i)
R : Type u_1
inst✝¹ : NontriviallyNormedField R
inst✝ : NormedAlgebra R K
x : R
f g : R → K
hf : DifferentiableAt R f x
hg : DifferentiableAt R g x
hx : g x ≠ 0
⊢ fderiv R (fun x => f x / g x) x =
    let k := f x;
    let k' := g x;
    fun dx =>L[R] ((fderiv R f x) dx * k' - k * (fderiv R g x) dx) / k' ^ 2
K : Type u_2
inst✝¹¹ : RCLike K
X : Type ?u.170248
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace K X
Y : Type ?u.170390
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace K Y
Z : Type ?u.170525
inst✝⁶ : NormedAddCommGroup Z
inst✝⁵ : NormedSpace K Z
ι : Type ?u.170660
inst✝⁴ : Fintype ι
E : ι → Type ?u.170668
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace K (E i)
R : Type u_1
inst✝¹ : NontriviallyNormedField R
inst✝ : NormedAlgebra R K
x : R
f g : R → K
hf : DifferentiableAt R f x
hg : DifferentiableAt R g x
hx : g x ≠ 0
h : ∀ (f : R → K) (x : R), (fderiv R f x) 1 = deriv f x
⊢ fderiv R (fun x => f x / g x) x =
    let k := f x;
    let k' := g x;
    fun dx =>L[R] ((fderiv R f x) dx * k' - k * (fderiv R g x) dx) / k' ^ 2