Post #1365988

@tao Oh, I had Tactic, I just mistyped in my reply. And it turns out that the import Canonical was throwing such a spanner in the works that the error message was attached to the line import Mathlib.Tactic , which worked on its own... 🤦‍♂️