case h.h
ι : Type u_3
ι' : Type ?u.700635
R : Type u_1
R₂ : Type ?u.700641
K : Type ?u.700644
M : Type u_2
M' : Type ?u.700650
M'' : Type ?u.700653
V : Type u
V' : Type ?u.700658
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Fintype ι
b : Basis ι R M
e : M ≃ₗ[R] ι → R
j : M
x✝ : ι
⊢ ↑(equivFun (ofEquivFun e)) j x✝ = ↑e j x✝
ι : Type u_3
ι' : Type ?u.700635
R : Type u_1
R₂ : Type ?u.700641
K : Type ?u.700644
M : Type u_2
M' : Type ?u.700650
M'' : Type ?u.700653
V : Type u
V' : Type ?u.700658
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Fintype ι
b : Basis ι R M
e : M ≃ₗ[R] ι → R
⊢ equivFun (ofEquivFun e) = e
ext j
no goals
case h.h
ι : Type u_3
ι' : Type ?u.700635
R : Type u_1
R₂ : Type ?u.700641
K : Type ?u.700644
M : Type u_2
M' : Type ?u.700650
M'' : Type ?u.700653
V : Type u
V' : Type ?u.700658
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Fintype ι
b : Basis ι R M
e : M ≃ₗ[R] ι → R
j : M
x✝ : ι
⊢ ↑(equivFun (ofEquivFun e)) j x✝ = ↑e j x✝
simp_rw [Basis.equivFun_apply, Basis.ofEquivFun_repr_apply]