R : Type u_2
inst✝² : Ring R
P : Type u_3
inst✝¹ : AddCommGroup P
inst✝ : Module R P
ι : Type u_1
b : Basis ι R P
⊢ Function.LeftInverse ↑(Finsupp.total P P R id) ↑(↑(Basis.constr b ℕ) fun i => Finsupp.single (↑b i) 1)
R : Type u_2
inst✝² : Ring R
P : Type u_3
inst✝¹ : AddCommGroup P
inst✝ : Module R P
ι : Type u_1
b : Basis ι R P
⊢ Projective R P
use b.constr ℕ fun i => Finsupp.single (b i) (1 : R)
R : Type u_2
inst✝² : Ring R
P : Type u_3
inst✝¹ : AddCommGroup P
inst✝ : Module R P
ι : Type u_1
b : Basis ι R P
m : P
⊢ ↑(Finsupp.total P P R id) (↑(↑(Basis.constr b ℕ) fun i => Finsupp.single (↑b i) 1) m) = m
R : Type u_2
inst✝² : Ring R
P : Type u_3
inst✝¹ : AddCommGroup P
inst✝ : Module R P
ι : Type u_1
b : Basis ι R P
⊢ Function.LeftInverse ↑(Finsupp.total P P R id) ↑(↑(Basis.constr b ℕ) fun i => Finsupp.single (↑b i) 1)
intro m
R : Type u_2
inst✝² : Ring R
P : Type u_3
inst✝¹ : AddCommGroup P
inst✝ : Module R P
ι : Type u_1
b : Basis ι R P
m : P
⊢ (sum (↑b.repr m) fun i d => d • ↑b i) = m
R : Type u_2
inst✝² : Ring R
P : Type u_3
inst✝¹ : AddCommGroup P
inst✝ : Module R P
ι : Type u_1
b : Basis ι R P
m : P
⊢ ↑(Finsupp.total P P R id) (↑(↑(Basis.constr b ℕ) fun i => Finsupp.single (↑b i) 1) m) = m
simp only [b.constr_apply, mul_one, id.def, Finsupp.smul_single', Finsupp.total_single,
  LinearMap.map_finsupp_sum]
no goals
R : Type u_2
inst✝² : Ring R
P : Type u_3
inst✝¹ : AddCommGroup P
inst✝ : Module R P
ι : Type u_1
b : Basis ι R P
m : P
⊢ (sum (↑b.repr m) fun i d => d • ↑b i) = m
exact b.total_repr m