fix: prefer original module in const2ModIdx (#4652)

When a definition is redeclared, the original code would clobber the
value of `const2ModIdx` every time, meaning that a constant would be
attributed to a module which occurs later than the modules for constants
referencing this one. Preferring the original module ensures that these
module indexes are dependency-ordered. This originally came up as a bug
in `shake`, which assumes this property, see
[Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/check.20for.20unused.20imports.20doesn't.20stop/near/449139309).

src/Lean/Environment.lean

@@ -868,9 +868,9 @@ def finalizeImport (s : ImportState) (imports : Array Import) (opts : Options) (
           -- Recall that the map has not been modified when `cinfoPrev? = some _`.
           unless equivInfo cinfoPrev cinfo do
             throwAlreadyImported s const2ModIdx modIdx cname
-      const2ModIdx := const2ModIdx.insert cname modIdx
+      const2ModIdx := const2ModIdx.insertIfNew cname modIdx |>.1
     for cname in mod.extraConstNames do
-      const2ModIdx := const2ModIdx.insert cname modIdx
+      const2ModIdx := const2ModIdx.insertIfNew cname modIdx |>.1
   let constants : ConstMap := SMap.fromHashMap constantMap false
   let exts ← mkInitialExtensionStates
   let mut env : Environment := {