Which is exactly why you want a Lean proof in the first place!
NL proofs rely on not-entirely-correct prior art, and contain countless holes both big and small. When formalizing human NL proofs it is probably very normal that the Lean proofs doesn't quite follow the NL proof.
NL proofs rely on not-entirely-correct prior art, and contain countless holes both big and small. When formalizing human NL proofs it is probably very normal that the Lean proofs doesn't quite follow the NL proof.