refactor(tactic/polyrith): use the autogenerated json parser (#15429)
refactor(tactic/polyrith): use the autogenerated json parser (#15429)

This acts as a nice demonstration of how to use `@[derive non_null_json_serializable]`





leanprover-community/mathlib,leanprover-community/mathlib