no goals
𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
F : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
G : Type u_3
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace 𝕜 G
R : Type ?u.242967
𝕜₂ : Type ?u.242970
𝕜' : Type ?u.242973
inst✝⁶ : NontriviallyNormedField 𝕜'
inst✝⁵ : NontriviallyNormedField 𝕜₂
M : Type ?u.242982
inst✝⁴ : TopologicalSpace M
σ₁₂ : 𝕜 →+* 𝕜₂
G' : Type ?u.243329
inst✝³ : NormedAddCommGroup G'
inst✝² : NormedSpace 𝕜₂ G'
inst✝¹ : NormedSpace 𝕜' G'
inst✝ : SMulCommClass 𝕜₂ 𝕜' G'
f : E →L[𝕜] F →L[𝕜] G
c : 𝕜
x : E
y : F
⊢ ↑(↑f (c • x)) y = c • ↑(↑f x) y
rw [f.map_smul, smul_apply]