Commit 2024-06-05 11:47 230f6fe6

View on Github →

chore: deprecate redundant lattice lemmas (#13513) There were tagged with the ematch attribute in lean 3, but this no longer exists.

Estimated changes

deleted theorem inf_le_left'
deleted theorem inf_le_right'
deleted theorem le_sup_left'
deleted theorem le_sup_right'