Commit 2022-03-15 11:10 eefa4257

perf(analysis/convec/topology): remove topological_add_group.path_connected instance (#12675) The linter was right in #10011 and topological_add_group.path_connected should not be an instance, because it creates enormous TC subproblems (turn on pp.all to get an idea of what's going on). Apparently the instance isn't even used in mathlib.