∀ {R : Type u_1} [inst : CommSemiring R] {P : Type u_9} {Q : Type u_10} [inst_1 : AddCommMonoid P]
  [inst_2 : AddCommMonoid Q] [inst_3 : Module R P] [inst_4 : Module R Q] (p : Submodule R P) (q : Submodule R Q),
  TensorProduct.mapIncl p q = TensorProduct.map p.subtype q.subtype