diff --git a/src/Init/Omega/Coeffs.lean b/src/Init/Omega/Coeffs.lean
index f880ba2e3a..ba1ca48e2c 100644
--- a/src/Init/Omega/Coeffs.lean
+++ b/src/Init/Omega/Coeffs.lean
@@ -20,7 +20,7 @@ There is an equivalent file setting up `Coeffs` as a type synonym for `AssocList
 currently in a private branch.
 Not all the theorems about the algebraic operations on that representation have been proved yet.
 When they are ready, we can replace the implementation in `omega` simply by importing
-`Std.Tactic.Omega.Coeffs.IntDict` instead of `Std.Tactic.Omega.Coeffs.IntList`.
+`Init.Omega.IntDict` instead of `Init.Omega.IntList`.
 
 For small problems, the sparse representation is actually slightly slower,
 so it is not urgent to make this replacement.
diff --git a/src/Init/Omega/Int.lean b/src/Init/Omega/Int.lean
index 347fdc7dd9..65b0aeb8a7 100644
--- a/src/Init/Omega/Int.lean
+++ b/src/Init/Omega/Int.lean
@@ -12,7 +12,7 @@ import Init.Data.Nat.Lemmas
 # Lemmas about `Nat`, `Int`, and `Fin` needed internally by `omega`.
 
 These statements are useful for constructing proof expressions,
-but unlikely to be widely useful, so are inside the `Std.Tactic.Omega` namespace.
+but unlikely to be widely useful, so are inside the `Lean.Omega` namespace.
 
 If you do find a use for them, please move them into the appropriate file and namespace!
 -/
diff --git a/src/Init/Omega/Logic.lean b/src/Init/Omega/Logic.lean
index 5963cf3469..7fc051918a 100644
--- a/src/Init/Omega/Logic.lean
+++ b/src/Init/Omega/Logic.lean
@@ -9,7 +9,7 @@ import Init.PropLemmas
 # Specializations of basic logic lemmas
 
 These are useful for `omega` while constructing proofs, but not considered generally useful
-so are hidden in the `Std.Tactic.Omega` namespace.
+so are hidden in the `Lean.Omega` namespace.
 
 If you find yourself needing them elsewhere, please move them first to another file.
 -/
diff --git a/src/Lean/Elab/Tactic/Omega/Frontend.lean b/src/Lean/Elab/Tactic/Omega/Frontend.lean
index 0c78d70947..734aed0306 100644
--- a/src/Lean/Elab/Tactic/Omega/Frontend.lean
+++ b/src/Lean/Elab/Tactic/Omega/Frontend.lean
@@ -598,7 +598,7 @@ def omegaTactic (cfg : OmegaConfig) : TacticM Unit := do
 
 /-- The `omega` tactic, for resolving integer and natural linear arithmetic problems. This
 `TacticM Unit` frontend with default configuration can be used as an Aesop rule, for example via
-the tactic call `aesop (add 50% tactic Std.Tactic.Omega.omegaDefault)`. -/
+the tactic call `aesop (add 50% tactic Lean.Omega.omegaDefault)`. -/
 def omegaDefault : TacticM Unit := omegaTactic {}
 
 @[builtin_tactic Lean.Parser.Tactic.omega]