Commit 2025-03-16 22:23 77aee407

View on Github →

chore(Data/Option): replace bad simp lemma elim_none_some (#22985) The previous simp lemma is tried at every lambda term, which is bad. #mathlib4 > bad simp discrimination tree keys @ 💬

Estimated changes

modified theorem Option.elim_none_some
added theorem Option.elim'_none_some