chore(topology/uniform_space/basic): golf a proof (#13289)
chore(topology/uniform_space/basic): golf a proof (#13289)

Rewrite a proof using tactic mode and golf it.





leanprover-community/mathlib,leanprover-community/mathlib