Commit 2025-01-21 01:06 cb161584

feat: tag csInf_insert and csSup_insert @[simp] (#20883) This makes the @[simp] attributes for complete and conditionally complete lattices consistent, so that sSup {a,b,c,d,...} is simplified to to a ⊔ b ⊔ c ⊔ d ⊔ ... in all cases (and similarly for sInf).