Use closeMainGoalUsing in Pratt tactic

[dhsorens]

Context

CompPoly/Fields/PrattCertificate.lean includes a TODO inside the pratt tactic:

use closeMainGoalUsing

Proposed work

• Replace the current closing step with closeMainGoalUsing.
• Keep tactic behavior unchanged for existing uses.

Acceptance criteria

• The TODO is removed and the tactic still proves the same goals.
• proofs and/or tests to show correctness as needed