diff --git a/tests/lean/beginEndAsMacro.lean b/tests/lean/beginEndAsMacro.lean
index 6138979716..1a0053bc6d 100644
--- a/tests/lean/beginEndAsMacro.lean
+++ b/tests/lean/beginEndAsMacro.lean
@@ -7,12 +7,12 @@ macro "begin " ts:tactic,*,? "end"%i : term => do
 
 theorem ex1 (x : Nat) : x + 0 = 0 + x :=
   begin
-    rw Nat.zero_add,
-    rw Nat.add_zero,
+    rw [Nat.zero_add],
+    rw [Nat.add_zero],
   end
 /- ANCHOR_END: doc -/
 
 theorem ex2 (x : Nat) : x + 0 = 0 + x :=
   begin
-    rw Nat.zero_add
+    rw [Nat.zero_add]
   end  -- error should be shown here
diff --git a/tests/lean/interactive/plainGoal.lean.expected.out b/tests/lean/interactive/plainGoal.lean.expected.out
index 9bbab69e4a..6692bf71b0 100644
--- a/tests/lean/interactive/plainGoal.lean.expected.out
+++ b/tests/lean/interactive/plainGoal.lean.expected.out
@@ -46,8 +46,8 @@
  "goals": ["n m : Nat\nh1 : n = m\nh2 : m = 0\n⊢ 0 = m"]}
 {"textDocument": {"uri": "file://plainGoal.lean"},
  "position": {"line": 25, "character": 13}}
-{"rendered": "```lean\nn m : Nat\nh1 : n = m\nh2 : m = 0\n⊢ 0 = 0\n```",
- "goals": ["n m : Nat\nh1 : n = m\nh2 : m = 0\n⊢ 0 = 0"]}
+{"rendered": "```lean\nn m : Nat\nh1 : n = m\nh2 : m = 0\n⊢ 0 = n\n```",
+ "goals": ["n m : Nat\nh1 : n = m\nh2 : m = 0\n⊢ 0 = n"]}
 {"textDocument": {"uri": "file://plainGoal.lean"},
  "position": {"line": 32, "character": 3}}
 {"rendered": "```lean\ncase zero\n⊢ 0 + Nat.zero = Nat.zero\n```",
diff --git a/tests/lean/isDefEqOffsetBug.lean b/tests/lean/isDefEqOffsetBug.lean
index d03230dc24..5a6a0f200d 100644
--- a/tests/lean/isDefEqOffsetBug.lean
+++ b/tests/lean/isDefEqOffsetBug.lean
@@ -19,9 +19,9 @@ theorem negZero [AddGroup α] : -(0 : α) = 0 := by
 
 theorem subZero [AddGroup α] {a : α} : a + -(0 : α) = a := by
   rw [← addZero (a := a)]
-  rw addAssoc
-  rw negZero
-  rw addZero
+  rw [addAssoc]
+  rw [negZero]
+  rw [addZero]
 
 theorem shouldFail [AddGroup α] : ((0 : α) + 0) = 0 :=
   rfl -- Error
diff --git a/tests/lean/run/270.lean b/tests/lean/run/270.lean
index 12ff3e314b..6d6b122b6d 100644
--- a/tests/lean/run/270.lean
+++ b/tests/lean/run/270.lean
@@ -8,8 +8,8 @@ theorem addComm3 [CommAddSemigroup α] {a b c : α} : a + b + c = a + c + b := b
     have h : b + c = c + b := addComm;
     have h' := congrArg (a + .) h;
     simp at h';
-    rw ←addAssoc at h';
-    rw ←addAssoc (a := a) at h';
+    rw [←addAssoc] at h';
+    rw [←addAssoc (a := a)] at h';
     exact h';
 }
 
@@ -22,8 +22,8 @@ theorem addComm5 [CommAddSemigroup α] {a b c : α} : a + b + c = a + c + b := b
     have h : b + c = c + b := addComm;
     have h' := congrArg (a + .) h;
     simp at h';
-    rw ←addAssoc at h';
-    rw ←@addAssoc (a := a) at h';
+    rw [←addAssoc] at h';
+    rw [←@addAssoc (a := a)] at h';
     exact h';
 }
 
@@ -31,7 +31,7 @@ theorem addComm6 [CommAddSemigroup α] {a b c : α} : a + b + c = a + c + b := b
     have h : b + c = c + b := addComm;
     have h' := congrArg (a + .) h;
     simp at h';
-    rw ←addAssoc at h';
-    rw ←addAssoc at h';
+    rw [←addAssoc] at h';
+    rw [←addAssoc] at h';
     exact h';
 }
diff --git a/tests/lean/run/KyleAlg.lean b/tests/lean/run/KyleAlg.lean
index b5ff7472ce..3fa5330d0b 100644
--- a/tests/lean/run/KyleAlg.lean
+++ b/tests/lean/run/KyleAlg.lean
@@ -138,16 +138,16 @@ theorem subZero [AddGroup α] {a : α} : a + -(0 : α) = a := by
     rw [←addZero (a := a), addAssoc, negZero, addZero]
 
 theorem negNeg [AddGroup α] {a : α} : -(-a) = a := by {
-    rw ←addZero (a := - -a);
-    rw ←negAdd (a := a);
-    rw ←addAssoc;
-    rw negAdd;
-    rw zeroAdd;
+    rw [←addZero (a := - -a)];
+    rw [←negAdd (a := a)];
+    rw [←addAssoc];
+    rw [negAdd];
+    rw [zeroAdd];
 }
 
 theorem addNeg [AddGroup α] {a : α} : a + -a = 0 := by {
-    have h : - -a + -a = 0 := by { rw negAdd };
-    rw negNeg at h;
+    have h : - -a + -a = 0 := by { rw [negAdd] };
+    rw [negNeg] at h;
     exact h
 }
 
@@ -162,14 +162,14 @@ theorem addIdemIffZero [AddGroup α] {a : α} : a + a = a ↔ a = 0 := by
     focus
         intro h
         subst a
-        rw addZero
+        rw [addZero]
 
 instance [Ring α] : ZeroMul α := by {
     apply ZeroMul.mk;
     intro a;
     have h : 0 * a + 0 * a = 0 * a := by { rw [←rightDistrib, addZero] };
-    rw addIdemIffZero (a := 0 * a) at h;
-    rw h;
+    rw [addIdemIffZero (a := 0 * a)] at h;
+    rw [h];
 }
 
 example [Ring α] : Semiring α := inferInstance
diff --git a/tests/lean/run/allGoals.lean b/tests/lean/run/allGoals.lean
index 886fadf7f9..cb848e9615 100644
--- a/tests/lean/run/allGoals.lean
+++ b/tests/lean/run/allGoals.lean
@@ -39,7 +39,7 @@ theorem Weekday.nextOfPrevious'' (d : Weekday) : previous (next d) = d ∧ next
   apply And.intro <;> cases d <;> rfl
 
 open Lean.Parser.Tactic in
-macro "rwd " x:term : tactic => `(rw $x:term; done)
+macro "rwd " x:term : tactic => `(rw [$x:term]; done)
 
 theorem ex (a b c : α) (h₁ : a = b) (h₂ : a = c) : b = a ∧ c = a := by
   apply And.intro <;> first rwd h₁ | rwd h₂
@@ -50,12 +50,12 @@ theorem idEq (a : α) : id a = a :=
 theorem Weekday.test (d : Weekday) : next (previous d) = id d := by
   cases d
   traceState
-  allGoals rw idEq
+  allGoals rw [idEq]
   traceState
   allGoals rfl
 
 theorem Weekday.test2 (d : Weekday) : next (previous d) = id d := by
-  cases d <;> rw idEq
+  cases d <;> rw [idEq]
   traceState
   allGoals rfl
 
diff --git a/tests/lean/run/casesUsing.lean b/tests/lean/run/casesUsing.lean
index 1162d48bf6..caddc13e1c 100644
--- a/tests/lean/run/casesUsing.lean
+++ b/tests/lean/run/casesUsing.lean
@@ -30,7 +30,7 @@ axiom Nat.parityElim (motive : Nat → Sort u)
   : motive n
 
 theorem time2Eq (n : Nat) : 2*n = n + n := by
-  rw Nat.mul_comm
+  rw [Nat.mul_comm]
   show (0 + n) + n = n+n
   simp
 
@@ -39,11 +39,11 @@ theorem ex3 (n : Nat) : Exists (fun m => n = m + m ∨ n = m + m + 1) := by
   | even i =>
     apply Exists.intro i
     apply Or.inl
-    rw time2Eq
+    rw [time2Eq]
   | odd i =>
     apply Exists.intro i
     apply Or.inr
-    rw time2Eq
+    rw [time2Eq]
 
 open Nat in
 theorem ex3b (n : Nat) : Exists (fun m => n = m + m ∨ n = m + m + 1) := by
@@ -51,11 +51,11 @@ theorem ex3b (n : Nat) : Exists (fun m => n = m + m ∨ n = m + m + 1) := by
   | even i =>
     apply Exists.intro i
     apply Or.inl
-    rw time2Eq
+    rw [time2Eq]
   | odd i =>
     apply Exists.intro i
     apply Or.inr
-    rw time2Eq
+    rw [time2Eq]
 
 def ex4 {α} (xs : List α) (h : xs = [] → False) : α := by
   cases he:xs with
@@ -152,4 +152,4 @@ theorem ex17 (n : Nat) : 0 + n = n := by
   case zero => rfl
   case succ m ih =>
     show Nat.succ (0 + m) = Nat.succ m
-    rw ih
+    rw [ih]
diff --git a/tests/lean/run/decClassical.lean b/tests/lean/run/decClassical.lean
index fa3aa9780c..821ad9caaa 100644
--- a/tests/lean/run/decClassical.lean
+++ b/tests/lean/run/decClassical.lean
@@ -5,7 +5,7 @@ theorem ex : if (fun x => x + 1) = (fun x => x + 2) then False else True := by
     intro h
     have 1 = 2 from congrFun h 0
     contradiction
-  rw ifNeg this
+  rw [ifNeg this]
   exact True.intro
 
 def tst (x : Nat) : Bool :=
diff --git a/tests/lean/run/def13.lean b/tests/lean/run/def13.lean
index a41c43be30..fd23a4565a 100644
--- a/tests/lean/run/def13.lean
+++ b/tests/lean/run/def13.lean
@@ -11,9 +11,9 @@ theorem filter_cons (a : α) (as : List α) : filter p (a :: as) = if p a then a
 rfl
 
 theorem filter_cons_of_pos {a : α} (as : List α) (h : p a) : filter p (a :: as) = a :: filter p as := by
-rw filter_cons;
-rw ifPos h
+rw [filter_cons];
+rw [ifPos h]
 
 theorem filter_cons_of_neg {a : α} (as : List α) (h : ¬ p a) : filter p (a :: as) = filter p as := by
-rw filter_cons;
-rw ifNeg h
+rw [filter_cons];
+rw [ifNeg h]
diff --git a/tests/lean/run/inductive_pred.lean b/tests/lean/run/inductive_pred.lean
index 4962a9d54c..8bb7fd05c1 100644
--- a/tests/lean/run/inductive_pred.lean
+++ b/tests/lean/run/inductive_pred.lean
@@ -2,10 +2,10 @@ namespace Ex
 inductive LE : Nat → Nat → Prop
   | refl : LE n n
   | succ : LE n m → LE n m.succ
-  
-def typeOf {α : Sort u} (a : α) := α 
 
-theorem LE_brecOn : typeOf @LE.brecOn = 
+def typeOf {α : Sort u} (a : α) := α
+
+theorem LE_brecOn : typeOf @LE.brecOn =
 ∀ {motive : (a a_1 : Nat) → LE a a_1 → Prop} {a a_1 : Nat} (x : LE a a_1),
   (∀ (a a_2 : Nat) (x : LE a a_2), @LE.below motive a a_2 x → motive a a_2 x) → motive a a_1 x := rfl
 
@@ -42,7 +42,7 @@ theorem mul_left_comm (n m o : Nat) : n * (m * o) = m * (n * o) := by
 inductive Power2 : Nat → Prop
   | base : Power2 1
   | ind  : Power2 n → Power2 (2*n) -- Note that index here is not a constructor
-  
+
 theorem Power2_brecOn : typeOf @Power2.brecOn = ∀ {motive : (a : Nat) → Power2 a → Prop} {a : Nat} (x : Power2 a),
   (∀ (a : Nat) (x : Power2 a), @Power2.below motive a x → motive a x) → motive a x := rfl
 
@@ -59,7 +59,7 @@ theorem Power2.mul : Power2 n → Power2 m → Power2 (n*m) := by
 --  | h1, ind h2 => mul_left_comm .. ▸ ind (mul' h1 h2)
 
 inductive tm : Type :=
-  | C : Nat → tm 
+  | C : Nat → tm
   | P : tm → tm → tm
 
 open tm
@@ -79,15 +79,15 @@ inductive step : tm → tm → Prop :=
 def deterministic {X : Type} (R : X → X → Prop) :=
   ∀ x y1 y2 : X, R x y1 → R x y2 → y1 = y2
 
-theorem step_deterministic' : deterministic step := λ x y₁ y₂ hy₁ hy₂ => 
-  @step.brecOn (λ s t st => ∀ y₂, s ==> y₂ → t = y₂) _ _ hy₁ (λ s t st hy₁ y₂ hy₂ => 
+theorem step_deterministic' : deterministic step := λ x y₁ y₂ hy₁ hy₂ =>
+  @step.brecOn (λ s t st => ∀ y₂, s ==> y₂ → t = y₂) _ _ hy₁ (λ s t st hy₁ y₂ hy₂ =>
     match hy₁, hy₂ with
     | step.below.ST_PlusConstConst _ _, step.ST_PlusConstConst _ _ => rfl
-    | step.below.ST_Plus1 _ _ _ _ hy₁ ih, step.ST_Plus1 _ t₁' _ _ => by rw ←ih t₁'; assumption
+    | step.below.ST_Plus1 _ _ _ _ hy₁ ih, step.ST_Plus1 _ t₁' _ _ => by rw [←ih t₁']; assumption
     | step.below.ST_Plus1 _ _ _ _ hy₁ ih, step.ST_Plus2 _ _ _ _ => by cases hy₁
-    | step.below.ST_Plus2 _ _ _ _ _ ih, step.ST_Plus2 _ _ t₂ _ => by rw ←ih t₂; assumption
+    | step.below.ST_Plus2 _ _ _ _ _ ih, step.ST_Plus2 _ _ t₂ _ => by rw [←ih t₂]; assumption
     | step.below.ST_Plus2 _ _ _ _ hy₁ _, step.ST_PlusConstConst _ _ => by cases hy₁
-    ) y₂ hy₂ 
+    ) y₂ hy₂
 
 section NestedRecursion
 
@@ -108,10 +108,10 @@ axiom FS {n : Nat} : P n → P (f (f n))
 -- | _, is_nat.S is_nat.Z => F1
 -- | _, is_nat.S (@is_nat.S n h) => FS (foo h)
 
-theorem foo' : ∀ {n}, is_nat n → P n := fun h => 
-  @is_nat.brecOn (fun n hn => P n) _ h fun n h ih => 
+theorem foo' : ∀ {n}, is_nat n → P n := fun h =>
+  @is_nat.brecOn (fun n hn => P n) _ h fun n h ih =>
   match ih with
-  | is_nat.below.Z => F0 
+  | is_nat.below.Z => F0
   | is_nat.below.S _ is_nat.below.Z _ => F1
   | is_nat.below.S _ (is_nat.below.S a b hx) h₂ => FS hx