diff --git a/src/Init/Conv.lean b/src/Init/Conv.lean
index 919a592e3d..1a15193cc0 100644
--- a/src/Init/Conv.lean
+++ b/src/Init/Conv.lean
@@ -31,7 +31,7 @@ syntax (name := delta) "delta " ident : conv
 syntax (name := pattern) "pattern " term : conv
 syntax (name := rewrite) "rewrite " (config)? rwRuleSeq : conv
 syntax (name := simp) "simp " (config)? (discharger)? (&"only ")? ("[" (simpStar <|> simpErase <|> simpLemma),* "]")? : conv
-syntax (name := simpMatch) "simpMatch " : conv
+syntax (name := simpMatch) "simp_match " : conv
 
 /-- Execute the given tactic block without converting `conv` goal into a regular goal -/
 syntax (name := nestedTacticCore) "tactic'" " => " tacticSeq : conv
@@ -59,7 +59,7 @@ macro_rules
 
 macro "skip" : conv => `(tactic => rfl)
 macro "done" : conv => `(tactic' => done)
-macro "traceState" : conv => `(tactic' => traceState)
+macro "trace_state" : conv => `(tactic' => trace_state)
 macro "apply " e:term : conv => `(tactic => apply $e)
 
 end Lean.Parser.Tactic.Conv
diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 89984c1ea6..41debea0e1 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -934,7 +934,7 @@ protected abbrev recOnSubsingleton₂
   intro a; apply s
   induction q₂ using Quot.recOnSubsingleton
   intro a; apply s
-  inferInstance
+  infer_instance
 
 end
 end Quotient
diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index bd41e6ae31..bf3e1bc542 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -282,9 +282,9 @@ syntax (name := case) "case " (ident <|> "_") (ident <|> "_")* " => " tacticSeq
 macro "next " args:(ident <|> "_")* " => " tac:tacticSeq : tactic => `(tactic| case _ $(args.getArgs)* => $tac)
 
 /-- `allGoals tac` runs `tac` on each goal, concatenating the resulting goals, if any. -/
-syntax (name := allGoals) "allGoals " tacticSeq : tactic
+syntax (name := allGoals) "all_goals " tacticSeq : tactic
 /-- `anyGoals tac` applies the tactic `tac` to every goal, and succeeds if at least one application succeeds.  -/
-syntax (name := anyGoals) "anyGoals " tacticSeq : tactic
+syntax (name := anyGoals) "any_goals " tacticSeq : tactic
 /--
 `focus tac` focuses on the main goal, suppressing all other goals, and runs `tac` on it.
 Usually `· tac`, which enforces that the goal is closed by `tac`, should be preferred. -/
@@ -293,19 +293,19 @@ syntax (name := focus) "focus " tacticSeq : tactic
 syntax (name := skip) "skip" : tactic
 /-- `done` succeeds iff there are no remaining goals. -/
 syntax (name := done) "done" : tactic
-syntax (name := traceState) "traceState" : tactic
-syntax (name := failIfSuccess) "failIfSuccess " tacticSeq : tactic
+syntax (name := traceState) "trace_state" : tactic
+syntax (name := failIfSuccess) "fail_if_success " tacticSeq : tactic
 syntax (name := paren) "(" tacticSeq ")" : tactic
-syntax (name := withReducible) "withReducible " tacticSeq : tactic
-syntax (name := withReducibleAndInstances) "withReducibleAndInstances " tacticSeq : tactic
+syntax (name := withReducible) "with_reducible " tacticSeq : tactic
+syntax (name := withReducibleAndInstances) "with_reducible_and_instances " tacticSeq : tactic
 /-- `first | tac | ...` runs each `tac` until one succeeds, or else fails. -/
 syntax (name := first) "first " withPosition((group(colGe "|" tacticSeq))+) : tactic
-syntax (name := rotateLeft) "rotateLeft" (num)? : tactic
-syntax (name := rotateRight) "rotateRight" (num)? : tactic
+syntax (name := rotateLeft) "rotate_left" (num)? : tactic
+syntax (name := rotateRight) "rotate_right" (num)? : tactic
 /-- `try tac` runs `tac` and succeeds even if `tac` failed. -/
 macro "try " t:tacticSeq : tactic => `(first | $t | skip)
 /-- `tac <;> tac'` runs `tac` on the main goal and `tac'` on each produced goal, concatenating all goals produced by `tac'`. -/
-macro:1 x:tactic " <;> " y:tactic:0 : tactic => `(tactic| focus ($x:tactic; allGoals $y:tactic))
+macro:1 x:tactic " <;> " y:tactic:0 : tactic => `(tactic| focus ($x:tactic; all_goals $y:tactic))
 
 /-- `· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. -/
 macro dot:("·" <|> ".") ts:tacticSeq : tactic => `(tactic| {%$dot ($ts:tacticSeq) })
@@ -316,7 +316,7 @@ macro "rfl" : tactic => `(exact rfl)
 macro "admit" : tactic => `(exact sorry)
 /-- The `sorry` tactic isnxo a shorthand for `exact sorry`. -/
 macro "sorry" : tactic => `(exact sorry)
-macro "inferInstance" : tactic => `(exact inferInstance)
+macro "infer_instance" : tactic => `(exact inferInstance)
 
 /-- Optional configuration option for tactics -/
 syntax config := atomic("(" &"config") " := " term ")"
@@ -343,7 +343,7 @@ def rwWithRfl (kind : SyntaxNodeKind) (atom : String) (stx : Syntax) : MacroM Sy
   -- Replace `]` token with one without position information in the expanded tactic
   let seq   := seq.setArg 2 (mkAtom "]")
   let tac   := stx.setKind kind |>.setArg 0 (mkAtomFrom stx atom) |>.setArg 2 seq
-  `(tactic| $tac; try (withReducible rfl%$rbrak))
+  `(tactic| $tac; try (with_reducible rfl%$rbrak))
 
 @[macro rwSeq] def expandRwSeq : Macro :=
   rwWithRfl ``Lean.Parser.Tactic.rewriteSeq "rewrite"
@@ -369,23 +369,23 @@ syntax (name := delta) "delta " ident (location)? : tactic
 
 -- Auxiliary macro for lifting have/suffices/let/...
 -- It makes sure the "continuation" `?_` is the main goal after refining
-macro "refineLift " e:term : tactic => `(focus (refine noImplicitLambda% $e; rotateRight))
+macro "refine_lift " e:term : tactic => `(focus (refine noImplicitLambda% $e; rotate_right))
 
-macro "have " d:haveDecl : tactic => `(refineLift have $d:haveDecl; ?_)
+macro "have " d:haveDecl : tactic => `(refine_lift have $d:haveDecl; ?_)
 /- We use a priority > default, to avoid ambiguity with previous `have` notation -/
 macro (priority := high) "have" x:ident " := " p:term : tactic => `(have $x:ident : _ := $p)
-macro "suffices " d:sufficesDecl : tactic => `(refineLift suffices $d:sufficesDecl; ?_)
-macro "let " d:letDecl : tactic => `(refineLift let $d:letDecl; ?_)
-macro "show " e:term : tactic => `(refineLift show $e:term from ?_)
+macro "suffices " d:sufficesDecl : tactic => `(refine_lift suffices $d:sufficesDecl; ?_)
+macro "let " d:letDecl : tactic => `(refine_lift let $d:letDecl; ?_)
+macro "show " e:term : tactic => `(refine_lift show $e:term from ?_)
 syntax (name := letrec) withPosition(atomic(group("let " &"rec ")) letRecDecls) : tactic
 macro_rules
-  | `(tactic| let rec $d:letRecDecls) => `(tactic| refineLift let rec $d:letRecDecls; ?_)
+  | `(tactic| let rec $d:letRecDecls) => `(tactic| refine_lift let rec $d:letRecDecls; ?_)
 
 -- Similar to `refineLift`, but using `refine'`
-macro "refineLift' " e:term : tactic => `(focus (refine' noImplicitLambda% $e; rotateRight))
-macro "have' " d:haveDecl : tactic => `(refineLift' have $d:haveDecl; ?_)
+macro "refine_lift' " e:term : tactic => `(focus (refine' noImplicitLambda% $e; rotate_right))
+macro "have' " d:haveDecl : tactic => `(refine_lift' have $d:haveDecl; ?_)
 macro (priority := high) "have'" x:ident " := " p:term : tactic => `(have' $x:ident : _ := $p)
-macro "let' " d:letDecl : tactic => `(refineLift' let $d:letDecl; ?_)
+macro "let' " d:letDecl : tactic => `(refine_lift' let $d:letDecl; ?_)
 
 syntax inductionAlt  := "| " (group("@"? ident) <|> "_") (ident <|> "_")* " => " (hole <|> syntheticHole <|> tacticSeq)
 syntax inductionAlts := "with " (tactic)? withPosition( (colGe inductionAlt)+)
@@ -402,8 +402,8 @@ syntax (name := cases) "cases " casesTarget,+ (" using " ident)? (inductionAlts)
 
 syntax (name := existsIntro) "exists " term : tactic
 
-/-- `renameI x_1 ... x_n` renames the last `n` inaccessible names using the given names. -/
-syntax (name := renameI) "renameI " (colGt (ident <|> "_"))+ : tactic
+/-- `rename_i x_1 ... x_n` renames the last `n` inaccessible names using the given names. -/
+syntax (name := renameI) "rename_i " (colGt (ident <|> "_"))+ : tactic
 
 syntax "repeat " tacticSeq : tactic
 macro_rules
diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean
index 0decab00c0..8cce19e4b6 100644
--- a/src/Lean/Elab/Tactic/BuiltinTactic.lean
+++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean
@@ -269,7 +269,7 @@ def renameInaccessibles (mvarId : MVarId) (hs : Array Syntax) : TacticM MVarId :
   | _ => throwUnsupportedSyntax
 
 @[builtinTactic «renameI»] def evalRenameInaccessibles : Tactic
-  | stx@`(tactic| renameI $hs*) => do replaceMainGoal [← renameInaccessibles (← getMainGoal) hs]
+  | stx@`(tactic| rename_i $hs*) => do replaceMainGoal [← renameInaccessibles (← getMainGoal) hs]
   | _ => throwUnsupportedSyntax
 
 @[builtinTactic «first»] partial def evalFirst : Tactic := fun stx => do
diff --git a/src/Lean/Elab/Tactic/Conv/Basic.lean b/src/Lean/Elab/Tactic/Conv/Basic.lean
index 93114db7df..1c6e5873ed 100644
--- a/src/Lean/Elab/Tactic/Conv/Basic.lean
+++ b/src/Lean/Elab/Tactic/Conv/Basic.lean
@@ -88,7 +88,7 @@ def changeLhs (lhs' : Expr) : TacticM Unit := do
     -- save state before/after entering focus on `{`
     withInfoContext (pure ()) initInfo
     evalManyTacticOptSemi stx[1]
-    evalTactic (← `(tactic| allGoals (try rfl)))
+    evalTactic (← `(tactic| all_goals (try rfl)))
 
 @[builtinTactic Lean.Parser.Tactic.Conv.nestedConv] def evalNestedConv : Tactic := fun stx => do
   evalConvSeqBracketed stx[0]