Commit 2023-05-28 17:25 b7597898

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 https://github.com/leanprover-community/mathlib4/pull/4036#issuecomment-1550297061 , 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.