feat: allow numeric literals to be coerced to option type

[robsimmons]

This PR allows adds new instances for the OfNat and OfScientific typeclass that allow numeric literals to be treated as having Option type.

This change fixes an apparent asymmetry between numerals and other Lean expressions. Thanks to the optionCoe typeclass, an expression that synthesizes the type α can be coerced to Option α. However, a numeral like 5 or 4.2e3 does not synthesize the type Nat or Float because it expands to e.g. OfNat.ofNat (α := _) (nat_lit 5), and typeclass inference will fail to find an instance that lets α be an Option type.

Comparing this with the behavior of String makes the apparent asymmetry particularly egregious, because string literals don't get a similar typeclass wrapper.

def s : String := "4"
example : Option String := s
example : Option String := ("3" : String)
example : Option String := "3"

def n : Nat := 4
example : Option Nat := n
example : Option Nat := (3 : Nat)
example : Option Nat := 3 -- Fails currently, succeeds under this PR

def d : Float := 4.
example : Option Float := d
example : Option Float := (3. : Float)
example : Option Float := 3. -- Fails currently, succeeds under this PR

Despite these instances not being coercions, the effect is quite similar to the optionCoe typeclass that defines the coercion α → Option α, so by putting them in Init.Data.Option.Core we ensure that these instances are similarly banned inside Init and Std.

https://live.lean-lang.org/#codez=CYUwZgBAzhBcEGUAuAnAlgOwOZwLwQCIAWAgKBAA8BDAWwAcAbEOCAeTqTQHsNFVMcsfFHLV6TFu048+6bHggAKAgGYCLZHKwBKUbUbN4U7r00CFqsqVCRe8AHJUkConvGG2HExEfOhEDDcDSS8ZXwVFFRZfXUp9CSNQ3nD/KIBaNIgAMSo0BhgAYwBXFBQQDCQGAE8AGmgigoKQEGAYIoxQFAgkAAs0GAAFACVSa3AIYBYshi4nFwA6IITPaV5p2b98YCWPYxl1uf9I+amZp1ixYMTV7LPNiBUTjOzc/Ihi0vLK2vrG5taIO1Ot0+oMhkA

[leanprover-community-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 6d5efd79b9d751a487c4b3049e283fc412b0179e --onto ac0b82933f6eac9914011ca2caf38d0e4e991160. You can force Mathlib CI using the force-mathlib-ci label. (2025-09-27 05:11:37)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5d3df7b5f45fa4781edd56c9b8869c49f89b820c --onto 0b2193c7715a55246d0596a4db548c1b5b81562a. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-03 18:02:44)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 6d5efd79b9d751a487c4b3049e283fc412b0179e --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-09-27 05:11:39)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 5d3df7b5f45fa4781edd56c9b8869c49f89b820c --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-03 18:02:46)

[robsimmons]

Making this a real PR, though there's no urgency of merging it until @kim-em is back in town and caught up.