`[ ... ] tactics produce output in other files

[fpvandoorn]

A tactic `[ t ] used in a tactic definition my_tac at line L column C in file X that is used in file Y produces output (a server message) at line L column C of file Y (independent of where the tactic my_tac was used in file Y).

See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Extension.20showing.20goal.20for.20a.20separate.20lemma for more information and a less cryptic description.

[bryangingechen]

Another example: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/buggy.20infoview.3F