mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

chore: deprecate bad lemmas about WithTop/WithBot

Open eric-wieser opened this issue 1 month ago • 0 comments

This file seems to frequently confuse WithBot.some and Option.some, and some of the lemmas are strange as a result.

By teaching cases not to introduce Option.some, we no longer need these weird lemmas.

Open in Gitpod

eric-wieser avatar May 22 '24 22:05 eric-wieser