Commit 2026-05-10 00:45 93049402

feat(Order/ConditionallyCompleteLattice/Indexed): ciSup_mono' for ConditionallyCompleteLattice (#38854) Usually a primed version of a sup/inf theorem is like the unprimed version but for ConditionallyCompleteLinearOrderBot which can remove Nonempty assumptions. ciSup_mono' is different from its unprimed version and it's missing ConditionallyCompleteLattice versions. We add these and rename ciSup_mono' to ciSup_mono_of_forall_exists'.