Ignore use! and congrm. Add test file

Mathlib/Tactic/TerminalRefineLinter.lean

@@ -30,13 +30,11 @@ def refine? : Syntax → Bool
   | .node _ ``Lean.Parser.Tactic.refine _  => true
   | _ => false
 
-/-- `refine? stx` detects whether the input syntax `stx` is `refine` or `refine'`. -/
-def last : Syntax → Syntax
-  | .node _ ``Lean.Parser.Tactic.tacticSeq1Indented #[.node _ `null args] => args.back
-  | _ => .missing
-
 /-- `SyntaxNodeKinds` that "contain" a `refine` and that the linter should ignore. -/
-abbrev ignore : HashSet SyntaxNodeKind := HashSet.empty.insert `Mathlib.Tactic.useSyntax
+abbrev ignore : HashSet SyntaxNodeKind := HashSet.empty
+  |>.insert `Mathlib.Tactic.useSyntax
+  |>.insert `Mathlib.Tactic.«tacticUse!___,,»
+  |>.insert `Mathlib.Tactic.congrM
 
 /-- `refine_tree t` returns all terminal usages of `refine/refine'` in the input infotree. -/
 partial

test/TerminalRefineLinter.lean

@@ -0,0 +1,28 @@
+import Mathlib.Tactic.Use
+import Mathlib.Tactic.Congrm
+import Mathlib.Tactic.TerminalRefineLinter
+
+#guard_msgs in
+example : Nat := by
+  use 0
+
+#guard_msgs in
+example : Nat := by
+  use! 0
+
+#guard_msgs in
+example : 0 = 0 := by
+  congrm(_)
+
+set_option linter.terminalRefine false in
+set_option linter.terminalRefine true in
+/--
+warning: Please, use `exact` instead of `refine'`! [linter.terminalRefine]
+---
+warning: Please, use `exact` instead of `refine`! [linter.terminalRefine]
+-/
+#guard_msgs in
+example : 0 = 0 ∧ 0 = 0 := by
+  constructor
+  refine' rfl
+  refine rfl