Commit 2025-08-06 17:32 5bc55886

chore(Order/Filter/Basic): write lemmas in point-free style (#27184) This PR writes the congruence lemmas about filtered equality and about asymptotic equivalence in a point-free style. This is so that they can then be tagged with @[gcongr]. Some of the old versions have been kept with a fun_ name. And apparently the import size has decreased as a bonus :)