mathlib

5fc18b5e - fix(tactic/polyrith): remove unnecessary 1* from polyrith output (#15292)

fix(tactic/polyrith): remove unnecessary 1* from polyrith output (#15292) Some `polyrith` certificates were printing with a superfluous `1*` in front. Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>