Commit 2025-03-12 20:18 bb749e53
View on Github →chore: upstream OptionT lemmas to batteries (#22859)
This PR has the corresponding changes for leanprover-community/batteries#1152
Some statements there were changed to be in terms of Option.elimM instead of a match, resulting in the tweaks to proofs here.