chore(algebra/module/injective): golf some proofs (#15534)
chore(algebra/module/injective): golf some proofs (#15534)




Co-authored-by: Yury G. Kudryashov <2c59405d0ec2e119a1c3d2318bdb4a6ce50051ae@urkud.name>

leanprover-community/mathlib,leanprover-community/mathlib