fix: out-line instance equality proofs in norm_num (#4048)

This applies a similar technique as was used for the `ofScientific` norm_num extension to the core field operations. This ensures that lean doesn't try to prove `Add.add (inst := inst1) 1234 56 = Add.add (inst := inst2) 1234 56` by evaluating the addition itself, and instead tries to prove the instances equal and let norm_num do the adding. Reported at #4036 (comment) , although I can't find a test case that doesn't involve the base norm_num implementation because all the core operations on nat are already overridden.

Author: digama0