mathlib3

ccdf1d27 - feat(category_theory/limits): prod.lift_comp_comp (#2968)