𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝⁹ : NontriviallyNormedField 𝕜'
inst✝⁸ : NormedAlgebra 𝕜 𝕜'
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜' E
inst✝⁴ : IsScalarTower 𝕜 𝕜' E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
f : E → F
f' : E →L[𝕜'] F
s : Set E
x : E
g' : E →L[𝕜] F
h : HasFDerivWithinAt f (restrictScalars 𝕜 f') s x
H : restrictScalars 𝕜 f' = g'
⊢ HasFDerivWithinAt f f' s x
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝⁹ : NontriviallyNormedField 𝕜'
inst✝⁸ : NormedAlgebra 𝕜 𝕜'
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜' E
inst✝⁴ : IsScalarTower 𝕜 𝕜' E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
f : E → F
f' : E →L[𝕜'] F
s : Set E
x : E
g' : E →L[𝕜] F
h : HasFDerivWithinAt f g' s x
H : restrictScalars 𝕜 f' = g'
⊢ HasFDerivWithinAt f f' s x
rw [← H] at h
no goals
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝⁹ : NontriviallyNormedField 𝕜'
inst✝⁸ : NormedAlgebra 𝕜 𝕜'
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜' E
inst✝⁴ : IsScalarTower 𝕜 𝕜' E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
f : E → F
f' : E →L[𝕜'] F
s : Set E
x : E
g' : E →L[𝕜] F
h : HasFDerivWithinAt f (restrictScalars 𝕜 f') s x
H : restrictScalars 𝕜 f' = g'
⊢ HasFDerivWithinAt f f' s x
exact h