no goals
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
r : R
a : (⨂[R]^n) M
⊢ ↑(cast R M (_ : 0 + n = n)) (GradedMonoid.GMul.mul (↑algebraMap₀ r) a) = r • a
rw [gMul_eq_coe_linearMap, algebraMap₀_eq_smul_one, LinearMap.map_smul₂,
  LinearEquiv.map_smul, ← gMul_eq_coe_linearMap, one_mul]