mathlib

e14e87ae - chore(category_theory/filtered): slightly golf two proofs (#10368)