no goals
M✝ : Type ?u.89956
N : Type ?u.89959
P : Type ?u.89962
α : Type u_1
M : Type u_2
inst✝² : MulOneClass M
inst✝¹ : SMul α M
inst✝ : IsScalarTower α M M
c : Con M
a : α
w x : M
h : ↑c w x
⊢ ↑c (a • w) (a • x)
simpa only [smul_one_mul] using c.mul (c.refl' (a • (1 : M) : M)) h