chore: add nomatch tactic (#3294)

src/Init/Tactics.lean

@@ -857,6 +857,12 @@ empty pattern match, closing the goal if the introduced pattern is impossible.
 -/
 macro "nofun" : tactic => `(tactic| exact nofun)
 
+/--
+The tactic `nomatch h` is shorthand for `exact nomatch h`.
+-/
+macro "nomatch " es:term,+ : tactic =>
+  `(tactic| exact nomatch $es:term,*)
+
 end Tactic
 
 namespace Attr

tests/lean/run/nomatch_tac.lean

@@ -0,0 +1,5 @@
+example (h : Empty) : False := by
+  nomatch h
+
+example (x : Nat) (f : Nat → Fin n) (h : n = 0 ∧ True) : False := by
+  nomatch f x, h.1