no goals
K : Type u_2
E : Type u_1
inst✝⁴ : IsROrC K
inst✝³ : AddCommGroup E
inst✝² : Module K E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ K E
r : ℝ
x : E
⊢ r • x = ↑r • x
rw [IsROrC.ofReal_alg, smul_one_smul]