mathlib

796f2675 - refactor(category_theory/lifting_properties): refactor lifting properties using comm_sq (#15765)

refactor(category_theory/lifting_properties): refactor lifting properties using comm_sq (#15765) Co-authored-by: Markus Himmel <markus@himmel-villmar.de> Co-authored-by: kkytola <kalle.kytola@aalto.fi> Co-authored-by: Tyler Raven Billingsley <trbillin@gmail.com> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: damiano <adomani@gmail.com> Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com> Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com> Co-authored-by: negiizhao <egresf@gmail.com> Co-authored-by: Andrew Yang <the.erd.one@gmail.com> Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com> Co-authored-by: tb65536 <tb65536@uw.edu> Co-authored-by: Kexing Ying <kexing.ying19@imperial.ac.uk> Co-authored-by: Rémy Degenne <Remydegenne@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>