I don't see turning in piles of Lean as bad-faith somehow. They were first, and they did prove the result (assuming no hidden exploit deep in the middle). The thing they produced is just different, and both giant raw proofs and distilled human-understandable proofs are valuable. Before we couldn't make giant raw proofs, so we didn't need to understand their place. Now we can. It makes sense to just incorporate that into what "math" is (at least until the machines are smarter and can make elegant proofs from the start).