case h
k : Type u_3
inst✝⁴ : CommRing k
R : Type u_1
inst✝³ : Ring R
inst✝² : Algebra k R
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module k M
ι : Type u_2
b : Basis ι k M
r : R
m : M
a✝ : ι
⊢ ↑(↑(basisAux R b) (r ⊗ₜ[k] m)) a✝ =
    ↑(r • Finsupp.mapRange ↑(algebraMap k R) (_ : ↑(algebraMap k R) 0 = 0) (↑b.repr m)) a✝
k : Type u_3
inst✝⁴ : CommRing k
R : Type u_1
inst✝³ : Ring R
inst✝² : Algebra k R
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module k M
ι : Type u_2
b : Basis ι k M
r : R
m : M
⊢ ↑(basisAux R b) (r ⊗ₜ[k] m) = r • Finsupp.mapRange ↑(algebraMap k R) (_ : ↑(algebraMap k R) 0 = 0) (↑b.repr m)
ext
no goals
case h
k : Type u_3
inst✝⁴ : CommRing k
R : Type u_1
inst✝³ : Ring R
inst✝² : Algebra k R
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module k M
ι : Type u_2
b : Basis ι k M
r : R
m : M
a✝ : ι
⊢ ↑(↑(basisAux R b) (r ⊗ₜ[k] m)) a✝ =
    ↑(r • Finsupp.mapRange ↑(algebraMap k R) (_ : ↑(algebraMap k R) 0 = 0) (↑b.repr m)) a✝
simp [basisAux, ← Algebra.commutes, Algebra.smul_def]