Commit 2025-02-19 08:59 9d75f595
View on Github →feat: add Homeomorph.sumCongr_{refl,symm,trans} (#22041)
These lemmas seem to be missing, compared to other comparable constructions.
While at it, move the corresponding lemmas for Equiv next to their definition.