diff --git a/Mathlib/Tactic/DeclarationNames.lean b/Mathlib/Tactic/DeclarationNames.lean
index c9cb53158e7bc..66e4f41d90495 100644
--- a/Mathlib/Tactic/DeclarationNames.lean
+++ b/Mathlib/Tactic/DeclarationNames.lean
@@ -6,7 +6,9 @@ Authors: Damiano Testa, Moritz Firsching
 
 import Lean.DeclarationRange
 import Lean.ResolveName
--- transitively imported in Mathlib.Init
+-- Import this linter explicitly to ensure that
+-- this file has a valid copyright header and module docstring.
+import Mathlib.Tactic.Linter.Header
 
 /-!
 This file contains functions that are used by multiple linters.
diff --git a/Mathlib/Tactic/Finiteness/Attr.lean b/Mathlib/Tactic/Finiteness/Attr.lean
index 93264ceb6d54e..aaa1585fc18fc 100644
--- a/Mathlib/Tactic/Finiteness/Attr.lean
+++ b/Mathlib/Tactic/Finiteness/Attr.lean
@@ -4,6 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
 import Aesop
+-- Import this linter explicitly to ensure that
+-- this file has a valid copyright header and module docstring.
+import Mathlib.Tactic.Linter.Header
 
 /-! # Finiteness tactic attribute -/