Commit 2026-01-17 10:43 2cdef43f

feat(CategoryTheory/ComposableArrows): isIso_iff (#33879) We introduce lemmas characterizing isomorphisms in ComposableArrows C n for small numbers n. We add autoparams (by cat_disch) for certain parameters. We also make definitions like mk₂ abbreviations (instead of using the simp attribute), as it will allow to have mk₂ in the LHS/RHS of simp lemmas in the formalization of spectral sequences #33842.