feat(CategoryTheory): lemmas about descOfIsLeftKanExtension
for pointwise left Kan extensions (+dual)
#17383
+43
−0