[bckgrndrdtn]

You are conflating:

(i) accepting that a piece of code is a valid Lean proof (ii) merging a valid Lean proof into Mathlib.

Valid Lean proofs need maintenance. Mathlib is a living blob of code. People care about how fast the proofs typecheck. Many other properties of code play a role.

Not everything that is true is worthy of immediately including in the Encyclopaedia Brittanica.

[murderfs]

So add it as an axiom with a comment pointing to the proof. If you don't trust the proof because you don't personally understand it, why are you using a proof assistant in the first place?