docs(tactic/interactive): Add tag debugging and doc mwe for `extr…

…act_goal` (#3708)

Requested by @kbuzzard on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Being.20stuck.20-.3E.20MWE/near/206124861).

x-ref: leanprover-community/leanprover-community.github.io#105 



Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>

src/tactic/interactive.lean

@@ -1045,7 +1045,8 @@ do ls ← local_context,
    partition_vars' (name_set.of_list $ ls.map expr.local_uniq_name) ls [] []
 
 /--
-Format the current goal as a stand-alone example. Useful for testing tactic.
+Format the current goal as a stand-alone example. Useful for testing tactics
+or creating [minimal working examples](https://leanprover-community.github.io/mwe.html).
 
 * `extract_goal`: formats the statement as an `example` declaration
 * `extract_goal my_decl`: formats the statement as a `lemma` or `def` declaration
@@ -1153,7 +1154,7 @@ add_tactic_doc
 { name       := "extract_goal",
   category   := doc_category.tactic,
   decl_names := [`tactic.interactive.extract_goal],
-  tags       := ["goal management", "proof extraction"] }
+  tags       := ["goal management", "proof extraction", "debugging"] }
 
 /--
 `inhabit α` tries to derive a `nonempty α` instance and then upgrades this