Tests for the polyrith tactic

Stream: mathlib4

[Eric Wieser]

We have 700 lines of tests for the polyrith tactic... but they're all commented out, because they were never ported!

More specifically, the refactor to Polyrith that took place when porting removed docs3#polyrith.process_output which is the interface that the tests needed in order to bypass the sage server.

Is porting these tests on anyone's radar?