have h := @fderiv.comp ℝ _ _ _ _ _ _ _ _ _ _ x w φ sorry (hx w)
case h.h.a
R : Type ?u.22279
inst✝¹⁸ : RealScalar R
W : Type u_1
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type ?u.22774
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.23013
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type ?u.23252
inst✝¹ : MeasurableSpace α
β : Type ?u.23258
inst✝ : MeasurableSpace β
x : W → X
hx : Differentiable ℝ x
w dw : W
φ : X → ℝ
⊢ (fderiv ℝ (fun x' => φ (x x')) w) dw = (fderiv ℝ φ (x w)) ((fderiv ℝ x w) dw)
case h.h.a
R : Type ?u.22279
inst✝¹⁸ : RealScalar R
W : Type u_1
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type ?u.22774
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.23013
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type ?u.23252
inst✝¹ : MeasurableSpace α
β : Type ?u.23258
inst✝ : MeasurableSpace β
x : W → X
hx : Differentiable ℝ x
w dw : W
φ : X → ℝ
h : fderiv ℝ (φ ∘ x) w = ContinuousLinearMap.comp (fderiv ℝ φ (x w)) (fderiv ℝ x w)
⊢ (fderiv ℝ (fun x' => φ (x x')) w) dw = (fderiv ℝ φ (x w)) ((fderiv ℝ x w) dw)