mathlib

3f772d42 - chore(category_theory/sites/compatible_plus): speed up ι_plus_comp_iso_hom (#16379)

chore(category_theory/sites/compatible_plus): speed up ι_plus_comp_iso_hom (#16379) This failed when experimenting with `-T90000`; just squeezing the `simp`s seems to help a fair bit.