Proof irrelevance is not respected in statements

With challenge

theorem foo_aux : 3 < 5 := show 2 + 1 < 5 by simp

theorem foo : ⟨3, foo_aux⟩ = (3 : Fin 5) := sorry

and solution

@[simp] theorem two_add_one : 2 + 1 = 3 := (rfl)

theorem foo_aux : 3 < 5 := show 2 + 1 < 5 by simp

theorem foo : ⟨3, foo_aux⟩ = (3 : Fin 5) := sorry

the solution is rejected because the simp proof has changed, with

Exporting #[foo, foo_aux, 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: Const does not match between challenge and target 'foo_aux'

Start by reproducing the challenge and solution from the issue, then compare how the exported declarations are checked when the proof of foo_aux differs. Trace the handling of proof-valued statements around the reported “Const does not match” failure. Done means the solution is accepted despite the changed simp proof, while ordinary mismatches remain rejected.