Commit 2025-11-06 15:01 6f0cdf6e

feat(SetLike): add exists_not_mem_of_ne_top lemma (#30946) Adds a bridging lemma for SetLike structures: if s ≠ ⊤ and the top element coerces to the universal set, then there exists an element not in s. This generalizes a pattern that was specific to AffineSubspace and makes it available for all SetLike structures (submodules, subalgebras, etc.) where ⊤ = univ. Extracted from #30854 per reviewer feedback: https://github.com/leanprover-community/mathlib4/pull/30854#discussion_r2462326156