mathlib

6ad27998 - chore(analysis/locally_convex/weak_dual): golf using `seminorm.comp` (#14699)