Comparator generates different instance names for problem and solution files

With this challenge in challenge.lean:

instance : Inhabited Nat := ⟨37⟩

theorem target : default = 37 := sorry

and this solution.lean

instance : Inhabited Nat := ⟨37⟩

theorem target : default = 37 := rfl

comparator fails with

Exporting #[target, propext, Quot.sound, Classical.choice, Nat.add, Nat.sub, Nat.mul, Nat.pow, Nat.gcd, Nat.div, Nat.mod, Nat.beq, Nat.ble, Nat.land, Nat.lor, Nat.xor, Nat.shiftLeft, Nat.shiftRight, String.ofList] from Challenge
Building Solution
Build completed successfully (3 jobs).
Exporting #[target, propext, Quot.sound, Classical.choice, Nat.add, Nat.sub, Nat.mul, Nat.pow, Nat.gcd, Nat.div, Nat.mod, Nat.beq, Nat.ble, Nat.land, Nat.lor, Nat.xor, Nat.shiftLeft, Nat.shiftRight, String.ofList] from Solution
uncaught exception: Challenge and solution theorem statement do not match: 'target'

presumably because one has type

@default _ instInhabitedNat_challenge = 37

and the other has type

@default _ instInhabitedNat_solution = 37

Reproduce the mismatch using the challenge.lean and solution.lean snippets from the report, then trace the comparator's theorem-statement comparison after the Challenge and Solution builds. The fix is done when equivalent local Inhabited Nat instances no longer make the target statements differ.