Commit 2026-05-04 15:38 b53544c1

View on Github →

chore: tag (almost) all mono lemmas as @[gcongr] (#38793) The few exceptions are the lemmas about Set and Finset which would make gcongr use ≤ instead of ⊆, and measure_mono_ae which feels like a bigger than I want to undertake here, as well as a few lemmas that gcongr doesn't want to eat. From AddCombi

Estimated changes

modified theorem Finset.dens_mono
modified theorem Finset.dens_strictMono
modified theorem NNReal.coe_mono
modified theorem CircleDeg1Lift.mono
modified theorem HomogeneousIdeal.comap_mono
modified theorem nhdsKer_mono