fix

Author: YaelDillies

Mathlib/LinearAlgebra/Basis/Defs.lean

@@ -483,7 +483,8 @@ theorem reindexFinsetRange_repr_self (i : ι) :
 @[simp]
 theorem reindexFinsetRange_repr (x : M) (i : ι)
     (h := Finset.mem_image_of_mem b (Finset.mem_univ i)) :
-    b.reindexFinsetRange.repr x ⟨b i, h⟩ = b.repr x i := by simp [reindexFinsetRange]
+    b.reindexFinsetRange.repr x ⟨b i, h⟩ = b.repr x i := by
+  rw [reindexFinsetRange, repr_reindex, Finsupp.mapDomain_equiv_apply]; simp
 
 end Fintype