From 5f02e6300c12ef4c6f7424b8f3fb0cdbe5242f24 Mon Sep 17 00:00:00 2001
From: adomani <adomani@gmail.com>
Date: Thu, 4 Apr 2024 17:38:44 +0200
Subject: [PATCH] Ignore `use!` and `congrm`.  Add test file

---
 Mathlib/Tactic/TerminalRefineLinter.lean | 10 ++++-----
 test/TerminalRefineLinter.lean           | 28 ++++++++++++++++++++++++
 2 files changed, 32 insertions(+), 6 deletions(-)
 create mode 100644 test/TerminalRefineLinter.lean

diff --git a/Mathlib/Tactic/TerminalRefineLinter.lean b/Mathlib/Tactic/TerminalRefineLinter.lean
index cd24c6904d261..09f88d0ff95c2 100644
--- a/Mathlib/Tactic/TerminalRefineLinter.lean
+++ b/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
diff --git a/test/TerminalRefineLinter.lean b/test/TerminalRefineLinter.lean
new file mode 100644
index 0000000000000..1fadb3fd59e66
--- /dev/null
+++ b/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