chore: Remove simp from Option.elim, replace with individal simp lemmas

[BoltonBailey]

This PR removes the simp attribute from Option.elim and adds it to two related simp lemmas, Option.elim_none and Option.elim_some.

This PR comes from some discussion here about simps! feeling too aggressive in unfolding this lemma.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0a1a855ba80e51515570439f3d73d3d9414ac053 --onto 1cf71e54cf268e87cf5c43c830d953f5c88e6c39. (2024-06-19 21:29:43)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase bc047b8530f76f75c4456192b3ca24ad28c85420 --onto 1cf71e54cf268e87cf5c43c830d953f5c88e6c39. (2024-06-19 21:51:47)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 84e46162b5d25581039cd575c40bc6bd347f0853 --onto 357b52928f905bfb85a3496e411cf12fa20e730c. (2024-06-21 15:09:43)
• 💥 Mathlib branch lean-pr-testing-4504 build failed against this PR. (2024-06-21 17:40:27) View Log
• 💥 Mathlib branch lean-pr-testing-4504 build failed against this PR. (2024-06-21 18:07:16) View Log
• 💥 Mathlib branch lean-pr-testing-4504 build failed against this PR. (2024-06-21 18:42:01) View Log
• ✅ Mathlib branch lean-pr-testing-4504 has successfully built against this PR. (2024-06-21 19:44:02) View Log

[BoltonBailey]

This rebase command from the bot does not seem to affect the PR in any way. I am not really sure what to do to be able to see if and how this breaks mathlib.

[leodemoura]

@BoltonBailey Have tried to squash your commits before executing the command? Another option is to use

git reset --hard origin/nightly-with-mathlib
git cherry-pick 1c29870c1aa
git cherry-pick 4554124b873

[BoltonBailey]

origin, which in this case is my fork of this repo, does not have a nightly-with-mathlib branch, so I don't think that will work. I could try the "squash"ing option, but it seems like it would require me to learn something called "interactive rebasing".

[semorrison]

origin, which in this case is my fork of this repo, does not have a nightly-with-mathlib branch, so I don't think that will work. I could try the "squash"ing option, but it seems like it would require me to learn something called "interactive rebasing".

Replace origin with the name of the upstream referring to this repository?