no goals
ι : Type u_4
ι' : Type u_2
R : Type u_3
R₂ : Type ?u.344299
K : Type ?u.344302
M : Type u_1
M' : Type ?u.344308
M'' : Type ?u.344311
V : Type u
V' : Type ?u.344316
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b b₁ : Basis ι R M
i : ι
c : R
x : M
b' : Basis ι' R M'
e : ι ≃ ι'
i' : ι'
⊢ ↑(LinearEquiv.symm (LinearEquiv.trans b.repr (Finsupp.domLCongr e))) (Finsupp.single i' 1) =
    ↑(LinearEquiv.symm b.repr) (Finsupp.single (↑e.symm i') 1)
rw [LinearEquiv.symm_trans_apply, Finsupp.domLCongr_symm, Finsupp.domLCongr_single]