no goals
ι : Type u_1
ι' : Type ?u.694515
R : Type u_2
R₂ : Type ?u.694521
K : Type ?u.694524
M : Type u_3
M' : Type ?u.694530
M'' : Type ?u.694533
V : Type u
V' : Type ?u.694538
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Fintype ι
b v : Basis ι R M
⊢ ofEquivFun (equivFun v) = v
classical
  ext j
  simp only [Basis.equivFun_symm_apply, Basis.coe_ofEquivFun]
  simp_rw [Function.update_apply, ite_smul]
  simp only [Finset.mem_univ, if_true, Pi.zero_apply, one_smul, Finset.sum_ite_eq', zero_smul]
case a
ι : Type u_1
ι' : Type ?u.694515
R : Type u_2
R₂ : Type ?u.694521
K : Type ?u.694524
M : Type u_3
M' : Type ?u.694530
M'' : Type ?u.694533
V : Type u
V' : Type ?u.694538
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Fintype ι
b v : Basis ι R M
j : ι
⊢ ↑(ofEquivFun (equivFun v)) j = ↑v j
ι : Type u_1
ι' : Type ?u.694515
R : Type u_2
R₂ : Type ?u.694521
K : Type ?u.694524
M : Type u_3
M' : Type ?u.694530
M'' : Type ?u.694533
V : Type u
V' : Type ?u.694538
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Fintype ι
b v : Basis ι R M
⊢ ofEquivFun (equivFun v) = v
ext j
case a
ι : Type u_1
ι' : Type ?u.694515
R : Type u_2
R₂ : Type ?u.694521
K : Type ?u.694524
M : Type u_3
M' : Type ?u.694530
M'' : Type ?u.694533
V : Type u
V' : Type ?u.694538
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Fintype ι
b v : Basis ι R M
j : ι
⊢ ∑ x : ι, update 0 j 1 x • ↑v x = ↑v j
case a
ι : Type u_1
ι' : Type ?u.694515
R : Type u_2
R₂ : Type ?u.694521
K : Type ?u.694524
M : Type u_3
M' : Type ?u.694530
M'' : Type ?u.694533
V : Type u
V' : Type ?u.694538
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Fintype ι
b v : Basis ι R M
j : ι
⊢ ↑(ofEquivFun (equivFun v)) j = ↑v j
simp only [Basis.equivFun_symm_apply, Basis.coe_ofEquivFun]
case a
ι : Type u_1
ι' : Type ?u.694515
R : Type u_2
R₂ : Type ?u.694521
K : Type ?u.694524
M : Type u_3
M' : Type ?u.694530
M'' : Type ?u.694533
V : Type u
V' : Type ?u.694538
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Fintype ι
b v : Basis ι R M
j : ι
⊢ (∑ x : ι, if x = j then 1 • ↑v x else OfNat.ofNat 0 x • ↑v x) = ↑v j
case a
ι : Type u_1
ι' : Type ?u.694515
R : Type u_2
R₂ : Type ?u.694521
K : Type ?u.694524
M : Type u_3
M' : Type ?u.694530
M'' : Type ?u.694533
V : Type u
V' : Type ?u.694538
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Fintype ι
b v : Basis ι R M
j : ι
⊢ ∑ x : ι, update 0 j 1 x • ↑v x = ↑v j
simp_rw [Function.update_apply, ite_smul]
no goals
case a
ι : Type u_1
ι' : Type ?u.694515
R : Type u_2
R₂ : Type ?u.694521
K : Type ?u.694524
M : Type u_3
M' : Type ?u.694530
M'' : Type ?u.694533
V : Type u
V' : Type ?u.694538
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Fintype ι
b v : Basis ι R M
j : ι
⊢ (∑ x : ι, if x = j then 1 • ↑v x else OfNat.ofNat 0 x • ↑v x) = ↑v j
simp only [Finset.mem_univ, if_true, Pi.zero_apply, one_smul, Finset.sum_ite_eq', zero_smul]