no goals
R : Type u_1
inst✝⁶ : Semiring R
P : Type u_2
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M : Type ?u.2418
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type ?u.2448
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
⊢ Projective R P ↔ ∃ s, comp (Finsupp.total P P R id) s = LinearMap.id
simp_rw [projective_def, FunLike.ext_iff, Function.LeftInverse, comp_apply, id_apply]