mathlib

b6d10283 - chore(topology/sequences): golf a few proofs (#14081)