simp [innerSL_smul_apply, id_smul_apply]
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
φ : 𝓢(ℝ, F)
x : ℝ
⊢ ((innerSL_smul φ) x) 1 = (id_smul φ) x
no goals