no goals
ι : Type u_3
ι' : Type ?u.207260
R : Type u_2
R₂ : Type ?u.207266
K : Type ?u.207269
M : Type u_1
M' : Type ?u.207275
M'' : Type ?u.207278
V : Type u
V' : Type ?u.207283
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
R₁ : Type ?u.207395
inst✝⁴ : Semiring R₁
σ : R →+* R₁
σ' : R₁ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
M₁ : Type ?u.207599
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
x y : M
⊢ x = y ↔ ∀ (i : ι), ↑(↑b.repr x) i = ↑(↑b.repr y) i
simp only [← FunLike.ext_iff, EmbeddingLike.apply_eq_iff_eq]