diff --git a/src/Lean/Elab/Tactic/ShowTerm.lean b/src/Lean/Elab/Tactic/ShowTerm.lean
index 94ef9c2c13..ebb65875ab 100644
--- a/src/Lean/Elab/Tactic/ShowTerm.lean
+++ b/src/Lean/Elab/Tactic/ShowTerm.lean
@@ -7,7 +7,7 @@ prelude
 import Lean.Elab.ElabRules
 import Lean.Meta.Tactic.TryThis
 
-namespace Std.Tactic
+namespace Lean.Elab.Tactic.ShowTerm
 open Lean Elab Term Tactic Meta.Tactic.TryThis Parser.Tactic
 
 @[builtin_tactic showTerm] def evalShowTerm : Tactic := fun stx =>
@@ -26,3 +26,5 @@ open Lean Elab Term Tactic Meta.Tactic.TryThis Parser.Tactic
     addTermSuggestion tk (← instantiateMVars e).headBeta (origSpan? := ← getRef)
     pure e
   | _, _ => throwUnsupportedSyntax
+
+end Lean.Elab.Tactic.ShowTerm
diff --git a/src/Lean/Elab/Tactic/Simpa.lean b/src/Lean/Elab/Tactic/Simpa.lean
index 79d441460d..3e8cf1e459 100644
--- a/src/Lean/Elab/Tactic/Simpa.lean
+++ b/src/Lean/Elab/Tactic/Simpa.lean
@@ -18,7 +18,7 @@ register_option linter.unnecessarySimpa : Bool := {
   descr := "enable the 'unnecessary simpa' linter"
 }
 
-namespace Std.Tactic.Simpa
+namespace Lean.Elab.Tactic.Simpa
 
 open Lean Parser.Tactic Elab Meta Term Tactic Simp Linter
 
@@ -86,3 +86,5 @@ deriving instance Repr for UseImplicitLambdaResult
           | _ => unreachable!
         TryThis.addSuggestion tk stx (origSpan? := ← getRef)
     | _ => throwUnsupportedSyntax
+
+end Lean.Elab.Tactic.Simpa