mathlib3
feat(tactic/interactive): move `rotate` into interactive namespace
#1272
Merged
Merged