∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (f g : Module.Basis ι R M),
  (fun b i => b.repr.symm fun₀ | i => 1) f = (fun b i => b.repr.symm fun₀ | i => 1) g → ↑f.repr.symm = ↑g.repr.symm