exclude one lemma from exact?

Stream: general

[Filippo A. E. Nuccio]

I am preparing a class and I would like to run exact? but preventing it to find a very specific lemma (namely nsmul_add_nsmul_eq_zero) so that I can explain some other feature. The problem is that the files I am importing all import Mathlib.Algebra.GroupPower.Basic, where the above lemma is defined, so I cannot get rid of it by simply avoiding a certain import. Is there a way to achieve this?

[Johan Commelin]

cc @Scott Morrison

[Kim Morrison]

You could put a check in exact? for that specific lemma?

[Kim Morrison]

I can't think of a way to do this without modifying exact?

[Filippo A. E. Nuccio]

What do you mean by a "check in exact?"?

[Eric Rodriguez]

I think Scott means editing the tactic itself

[Filippo A. E. Nuccio]

OK, I'll give it a try. Thanks!