no goals
ι : Type u_4
ι' : Type u_1
R : Type u_2
R₂ : Type ?u.362162
K : Type ?u.362165
M : Type u_3
M' : Type ?u.362171
M'' : Type ?u.362174
V : Type u
V' : Type ?u.362179
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 : ι ≃ ι'
⊢ ∀ (x_1 : ι'), ↑(↑(reindex b e).repr x) x_1 = ↑(Finsupp.mapDomain (↑e) (↑b.repr x)) x_1
simp [repr_reindex_apply]