helping grind understand scientific notation

Stream: mathlib4

[Kim Morrison]

Mathlib.Data.Rat.Cast.OfScientific provides the typeclass that lets grind understanding scientific notation in characteristic zero fields (in particular, in the reals!). This would be useful in files such as

• Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean
• Mathlib/Analysis/SpecialFunctions/Elliptic/Weierstrass.lean
  which use scientific notation to write explicit constants. (In particular here, I'm resolving the final cases where grind can't do everything that linarith can.)

However Mathlib.Data.Rat.Cast.OfScientific has awkward imports that aren't brought together anywhere early in the library, so I'm finding it hard to put this necessary import somewhere that people will actually find it easily.

If anyone were interested in adopting this problem, that would be lovely.

(More concisely, the request is: "make sure instance {K : Type*} [_root_.Field K] [CharZero K] : LawfulOfScientific K, currently defined in Mathlib.Data.Rat.Cast.OfScientific is available earlier, and certainly available by Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean and Mathlib/Analysis/SpecialFunctions/Elliptic/Weierstrass.lean without needing explicit imports there".)

[Kim Morrison]

Pinging @Bhavik Mehta as I think he's been tripped up by this in past. :-)