mathlib3

6a852793 - fix(tactic/doc_commands): do not construct json by hand (#4501)

fix(tactic/doc_commands): do not construct json by hand (#4501) Fixes three lines going over the 100 character limit. The first one was a hand-rolled JSON serializer, I took the liberty to migrate it to the new `json` API.