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 (_ : n + 0 = n)) (GradedMonoid.GMul.mul a (↑algebraMap₀ r)) = r • a
rw [gMul_eq_coe_linearMap, algebraMap₀_eq_smul_one, LinearMap.map_smul,
  LinearEquiv.map_smul, ← gMul_eq_coe_linearMap, mul_one]