diff --git a/src/Init/Conv.lean b/src/Init/Conv.lean
index 58751741ba..d0707b1969 100644
--- a/src/Init/Conv.lean
+++ b/src/Init/Conv.lean
@@ -30,7 +30,6 @@ syntax (name := change) "change " term : conv
 syntax (name := delta) "delta " ident : conv
 syntax (name := pattern) "pattern " term : conv
 syntax (name := rewrite) "rewrite " (config)? rwRuleSeq : conv
-syntax (name := erewrite) "erewrite " rwRuleSeq : conv
 syntax (name := simp) "simp " ("(" &"config" " := " term ")")? (&"only ")? ("[" (simpStar <|> simpErase <|> simpLemma),* "]")? : conv
 syntax (name := simpMatch) "simpMatch " : conv
 
@@ -43,8 +42,9 @@ syntax (name := paren) "(" convSeq ")" : conv
 
 /-- `· conv` focuses on the main conv goal and tries to solve it using `s` -/
 macro dot:("·" <|> ".") s:convSeq : conv => `({%$dot ($s:convSeq) })
-macro "rw " s:rwRuleSeq : conv => `(rewrite $s:rwRuleSeq)
-macro "erw " s:rwRuleSeq : conv => `(erewrite $s:rwRuleSeq)
+macro "rw " c:(config)? s:rwRuleSeq : conv =>
+  let c? := if c.isNone then none else some c[0]
+  `(conv| rewrite $[$c?:config]? $s:rwRuleSeq)
 macro "args" : conv => `(congr)
 macro "left" : conv => `(lhs)
 macro "right" : conv => `(rhs)
diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean
index 1a044207f8..ae5237ad67 100644
--- a/src/Lean/Server/FileWorker/RequestHandling.lean
+++ b/src/Lean/Server/FileWorker/RequestHandling.lean
@@ -59,7 +59,7 @@ partial def handleHover (p : HoverParams)
 
 inductive GoToKind
   | declaration | definition | type
-  deriving DecidableEq
+  deriving BEq
 
 open Elab GoToKind in
 partial def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams)
@@ -112,7 +112,7 @@ partial def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams)
         if let some (ci, i) := t.hoverableInfoAt? hoverPos then
           if let Info.ofTermInfo ti := i then
             let mut expr := ti.expr
-            if kind = type then
+            if kind == type then
               expr ← ci.runMetaM i.lctx do
                 Expr.getAppFn (← Meta.instantiateMVars (← Meta.inferType expr))
             match expr with
@@ -120,7 +120,7 @@ partial def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams)
             | Expr.fvar id .. => return ← ci.runMetaM i.lctx <| locationLinksFromBinder t i id
             | _ => pure ()
           if let Info.ofFieldInfo fi := i then
-            if kind = type then
+            if kind == type then
               let expr ← ci.runMetaM i.lctx do
                 Meta.instantiateMVars (← Meta.inferType fi.val)
               if let some n := expr.getAppFn.constName? then
@@ -129,9 +129,9 @@ partial def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams)
               return ← ci.runMetaM i.lctx <| locationLinksFromDecl i fi.projName
           -- If other go-tos fail, we try to show the elaborator or parser
           if let some ei := i.toElabInfo? then
-            if kind = declaration ∧ ci.env.contains ei.stx.getKind then
+            if kind == declaration && ci.env.contains ei.stx.getKind then
               return ← ci.runMetaM i.lctx <| locationLinksFromDecl i ei.stx.getKind
-            if kind = definition ∧ ci.env.contains ei.elaborator then
+            if kind == definition && ci.env.contains ei.elaborator then
               return ← ci.runMetaM i.lctx <| locationLinksFromDecl i ei.elaborator
       return #[]