feat: check_compositions, a tactic for diagnosing defeq problems in category theory (#21357)
check_compositions