∀ {𝕜 : Type u_1} {V : Type u_2} {V' : Type u_3} {W : Type u_4} {W' : Type u_5} [inst : NontriviallyNormedField 𝕜]
  {σ σ' : 𝕜 →+* 𝕜} [inst_1 : NormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : NormedAddCommGroup V']
  [inst_4 : NormedSpace 𝕜 V'] [inst_5 : NormedAddCommGroup W] [inst_6 : NormedSpace 𝕜 W]
  [inst_7 : NormedAddCommGroup W'] [inst_8 : NormedSpace 𝕜 W'] [RingHomIsometric σ] [inst_10 : RingHomInvPair σ σ']
  (L : W →SL[σ] W') (R : V' →SL[σ'] V) {f : V → W} {z : V'} {f' : V →L[𝕜] W},
  HasFDerivAt f f' (R z) → HasFDerivAt (⇑L ∘ f ∘ ⇑R) (L.comp (f'.comp R)) z