diff --git a/src/Init/Data/Array/DecidableEq.lean b/src/Init/Data/Array/DecidableEq.lean
index 6afecd70d8..593840201d 100644
--- a/src/Init/Data/Array/DecidableEq.lean
+++ b/src/Init/Data/Array/DecidableEq.lean
@@ -11,13 +11,13 @@ namespace Array
 
 theorem eq_of_isEqvAux [DecidableEq α] (a b : Array α) (hsz : a.size = b.size) (i : Nat) (hi : i ≤ a.size) (heqv : Array.isEqvAux a b hsz (fun x y => x = y) i) (j : Nat) (low : i ≤ j) (high : j < a.size) : a.get ⟨j, high⟩ = b.get ⟨j, hsz ▸ high⟩ := by
   by_cases h : i < a.size
-  . unfold Array.isEqvAux at heqv
+  · unfold Array.isEqvAux at heqv
     simp [h] at heqv
     have hind := eq_of_isEqvAux a b hsz (i+1) (Nat.succ_le_of_lt h) heqv.2
     by_cases heq : i = j
-    . subst heq; exact heqv.1
-    . exact hind j (Nat.succ_le_of_lt (Nat.lt_of_le_and_ne low heq)) high
-  . have heq : i = a.size := Nat.le_antisymm hi (Nat.ge_of_not_lt h)
+    · subst heq; exact heqv.1
+    · exact hind j (Nat.succ_le_of_lt (Nat.lt_of_le_and_ne low heq)) high
+  · have heq : i = a.size := Nat.le_antisymm hi (Nat.ge_of_not_lt h)
     subst heq
     exact absurd (Nat.lt_of_lt_of_le high low) (Nat.lt_irrefl j)
 termination_by _ => a.size - i
diff --git a/src/Init/Data/Array/Mem.lean b/src/Init/Data/Array/Mem.lean
index 6cad3386ac..b9d7ce7b74 100644
--- a/src/Init/Data/Array/Mem.lean
+++ b/src/Init/Data/Array/Mem.lean
@@ -33,10 +33,10 @@ theorem sizeOf_lt_of_mem [DecidableEq α] [SizeOf α] {as : Array α} (h : a ∈
   let rec aux (j : Nat) (h : anyM.loop (m := Id) (fun b => decide (a = b)) as as.size (Nat.le_refl ..) j = true) : sizeOf a < sizeOf as := by
     unfold anyM.loop at h
     split at h
-    . simp [Bind.bind, pure] at h; split at h
+    · simp [Bind.bind, pure] at h; split at h
       next he => subst a; apply sizeOf_get_lt
       next => have ih := aux (j+1) h; assumption
-    . contradiction
+    · contradiction
   apply aux 0 h
 termination_by aux j _ => as.size - j
 
diff --git a/src/Init/Data/Nat/Linear.lean b/src/Init/Data/Nat/Linear.lean
index d447fcdebc..9cc081956a 100644
--- a/src/Init/Data/Nat/Linear.lean
+++ b/src/Init/Data/Nat/Linear.lean
@@ -356,26 +356,26 @@ theorem Poly.denote_eq_cancelAux (ctx : Context) (fuel : Nat) (m₁ m₂ r₁ r
     split <;> simp at h <;> try assumption
     rename_i k₁ v₁ m₁ k₂ v₂ m₂
     by_cases hltv : Nat.blt v₁ v₂ <;> simp [hltv]
-    . apply ih; simp [denote_eq] at h |-; assumption
-    . by_cases hgtv : Nat.blt v₂ v₁ <;> simp [hgtv]
-      . apply ih; simp [denote_eq] at h |-; assumption
-      . have heqv : v₁ = v₂ := eq_of_not_blt_eq_true hltv hgtv; subst heqv
+    · apply ih; simp [denote_eq] at h |-; assumption
+    · by_cases hgtv : Nat.blt v₂ v₁ <;> simp [hgtv]
+      · apply ih; simp [denote_eq] at h |-; assumption
+      · have heqv : v₁ = v₂ := eq_of_not_blt_eq_true hltv hgtv; subst heqv
         by_cases hltk : Nat.blt k₁ k₂ <;> simp [hltk]
-        . apply ih
+        · apply ih
           simp [denote_eq] at h |-
           have haux : k₁ * Var.denote ctx v₁ ≤ k₂ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt (Nat.blt_eq.mp hltk))
           rw [Nat.mul_sub_right_distrib, ← Nat.add_assoc, ← Nat.add_sub_assoc haux]
           apply Eq.symm
           apply Nat.sub_eq_of_eq_add
           simp [h]
-        . by_cases hgtk : Nat.blt k₂ k₁ <;> simp [hgtk]
-          . apply ih
+        · by_cases hgtk : Nat.blt k₂ k₁ <;> simp [hgtk]
+          · apply ih
             simp [denote_eq] at h |-
             have haux : k₂ * Var.denote ctx v₁ ≤ k₁ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt (Nat.blt_eq.mp hgtk))
             rw [Nat.mul_sub_right_distrib, ← Nat.add_assoc, ← Nat.add_sub_assoc haux]
             apply Nat.sub_eq_of_eq_add
             simp [h]
-          . have heqk : k₁ = k₂ := eq_of_not_blt_eq_true hltk hgtk; subst heqk
+          · have heqk : k₁ = k₂ := eq_of_not_blt_eq_true hltk hgtk; subst heqk
             apply ih
             simp [denote_eq] at h |-
             rw [← Nat.add_assoc, ← Nat.add_assoc] at h
@@ -390,25 +390,25 @@ theorem Poly.of_denote_eq_cancelAux (ctx : Context) (fuel : Nat) (m₁ m₂ r₁
     split at h <;> simp <;> try assumption
     rename_i k₁ v₁ m₁ k₂ v₂ m₂
     by_cases hltv : Nat.blt v₁ v₂ <;> simp [hltv] at h
-    . have ih := ih (h := h); simp [denote_eq] at ih ⊢; assumption
-    . by_cases hgtv : Nat.blt v₂ v₁ <;> simp [hgtv] at h
-      . have ih := ih (h := h); simp [denote_eq] at ih ⊢; assumption
-      . have heqv : v₁ = v₂ := eq_of_not_blt_eq_true hltv hgtv; subst heqv
+    · have ih := ih (h := h); simp [denote_eq] at ih ⊢; assumption
+    · by_cases hgtv : Nat.blt v₂ v₁ <;> simp [hgtv] at h
+      · have ih := ih (h := h); simp [denote_eq] at ih ⊢; assumption
+      · have heqv : v₁ = v₂ := eq_of_not_blt_eq_true hltv hgtv; subst heqv
         by_cases hltk : Nat.blt k₁ k₂ <;> simp [hltk] at h
-        . have ih := ih (h := h); simp [denote_eq] at ih ⊢
+        · have ih := ih (h := h); simp [denote_eq] at ih ⊢
           have haux : k₁ * Var.denote ctx v₁ ≤ k₂ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt (Nat.blt_eq.mp hltk))
           rw [Nat.mul_sub_right_distrib, ← Nat.add_assoc, ← Nat.add_sub_assoc haux] at ih
           have ih := Nat.eq_add_of_sub_eq (Nat.le_trans haux (Nat.le_add_left ..)) ih.symm
           simp at ih
           rw [ih]
-        . by_cases hgtk : Nat.blt k₂ k₁ <;> simp [hgtk] at h
-          . have ih := ih (h := h); simp [denote_eq] at ih ⊢
+        · by_cases hgtk : Nat.blt k₂ k₁ <;> simp [hgtk] at h
+          · have ih := ih (h := h); simp [denote_eq] at ih ⊢
             have haux : k₂ * Var.denote ctx v₁ ≤ k₁ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt (Nat.blt_eq.mp hgtk))
             rw [Nat.mul_sub_right_distrib, ← Nat.add_assoc, ← Nat.add_sub_assoc haux] at ih
             have ih := Nat.eq_add_of_sub_eq (Nat.le_trans haux (Nat.le_add_left ..)) ih
             simp at ih
             rw [ih]
-          . have heqk : k₁ = k₂ := eq_of_not_blt_eq_true hltk hgtk; subst heqk
+          · have heqk : k₁ = k₂ := eq_of_not_blt_eq_true hltk hgtk; subst heqk
             have ih := ih (h := h); simp [denote_eq] at ih ⊢
             rw [← Nat.add_assoc, ih, Nat.add_assoc]
 
@@ -435,25 +435,25 @@ theorem Poly.denote_le_cancelAux (ctx : Context) (fuel : Nat) (m₁ m₂ r₁ r
     split <;> simp at h <;> try assumption
     rename_i k₁ v₁ m₁ k₂ v₂ m₂
     by_cases hltv : Nat.blt v₁ v₂ <;> simp [hltv]
-    . apply ih; simp [denote_le] at h |-; assumption
-    . by_cases hgtv : Nat.blt v₂ v₁ <;> simp [hgtv]
-      . apply ih; simp [denote_le] at h |-; assumption
-      . have heqv : v₁ = v₂ := eq_of_not_blt_eq_true hltv hgtv; subst heqv
+    · apply ih; simp [denote_le] at h |-; assumption
+    · by_cases hgtv : Nat.blt v₂ v₁ <;> simp [hgtv]
+      · apply ih; simp [denote_le] at h |-; assumption
+      · have heqv : v₁ = v₂ := eq_of_not_blt_eq_true hltv hgtv; subst heqv
         by_cases hltk : Nat.blt k₁ k₂ <;> simp [hltk]
-        . apply ih
+        · apply ih
           simp [denote_le] at h |-
           have haux : k₁ * Var.denote ctx v₁ ≤ k₂ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt (Nat.blt_eq.mp hltk))
           rw [Nat.mul_sub_right_distrib, ← Nat.add_assoc, ← Nat.add_sub_assoc haux]
           apply Nat.le_sub_of_add_le
           simp [h]
-        . by_cases hgtk : Nat.blt k₂ k₁ <;> simp [hgtk]
-          . apply ih
+        · by_cases hgtk : Nat.blt k₂ k₁ <;> simp [hgtk]
+          · apply ih
             simp [denote_le] at h |-
             have haux : k₂ * Var.denote ctx v₁ ≤ k₁ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt (Nat.blt_eq.mp hgtk))
             rw [Nat.mul_sub_right_distrib, ← Nat.add_assoc, ← Nat.add_sub_assoc haux]
             apply Nat.sub_le_of_le_add
             simp [h]
-          . have heqk : k₁ = k₂ := eq_of_not_blt_eq_true hltk hgtk; subst heqk
+          · have heqk : k₁ = k₂ := eq_of_not_blt_eq_true hltk hgtk; subst heqk
             apply ih
             simp [denote_le] at h |-
             rw [← Nat.add_assoc, ← Nat.add_assoc] at h
@@ -469,25 +469,25 @@ theorem Poly.of_denote_le_cancelAux (ctx : Context) (fuel : Nat) (m₁ m₂ r₁
     split at h <;> simp <;> try assumption
     rename_i k₁ v₁ m₁ k₂ v₂ m₂
     by_cases hltv : Nat.blt v₁ v₂ <;> simp [hltv] at h
-    . have ih := ih (h := h); simp [denote_le] at ih ⊢; assumption
-    . by_cases hgtv : Nat.blt v₂ v₁ <;> simp [hgtv] at h
-      . have ih := ih (h := h); simp [denote_le] at ih ⊢; assumption
-      . have heqv : v₁ = v₂ := eq_of_not_blt_eq_true hltv hgtv; subst heqv
+    · have ih := ih (h := h); simp [denote_le] at ih ⊢; assumption
+    · by_cases hgtv : Nat.blt v₂ v₁ <;> simp [hgtv] at h
+      · have ih := ih (h := h); simp [denote_le] at ih ⊢; assumption
+      · have heqv : v₁ = v₂ := eq_of_not_blt_eq_true hltv hgtv; subst heqv
         by_cases hltk : Nat.blt k₁ k₂ <;> simp [hltk] at h
-        . have ih := ih (h := h); simp [denote_le] at ih ⊢
+        · have ih := ih (h := h); simp [denote_le] at ih ⊢
           have haux : k₁ * Var.denote ctx v₁ ≤ k₂ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt (Nat.blt_eq.mp hltk))
           rw [Nat.mul_sub_right_distrib, ← Nat.add_assoc, ← Nat.add_sub_assoc haux] at ih
           have := Nat.add_le_of_le_sub (Nat.le_trans haux (Nat.le_add_left ..)) ih
           simp at this
           exact this
-        . by_cases hgtk : Nat.blt k₂ k₁ <;> simp [hgtk] at h
-          . have ih := ih (h := h); simp [denote_le] at ih ⊢
+        · by_cases hgtk : Nat.blt k₂ k₁ <;> simp [hgtk] at h
+          · have ih := ih (h := h); simp [denote_le] at ih ⊢
             have haux : k₂ * Var.denote ctx v₁ ≤ k₁ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt (Nat.blt_eq.mp hgtk))
             rw [Nat.mul_sub_right_distrib, ← Nat.add_assoc, ← Nat.add_sub_assoc haux] at ih
             have := Nat.le_add_of_sub_le ih
             simp at this
             exact this
-          . have heqk : k₁ = k₂ := eq_of_not_blt_eq_true hltk hgtk; subst heqk
+          · have heqk : k₁ = k₂ := eq_of_not_blt_eq_true hltk hgtk; subst heqk
             have ih := ih (h := h); simp [denote_le] at ih ⊢
             have := Nat.add_le_add_right ih (k₁ * Var.denote ctx v₁)
             simp at this
@@ -560,8 +560,8 @@ theorem ExprCnstr.denote_toPoly (ctx : Context) (c : ExprCnstr) : c.toPoly.denot
   cases c; rename_i eq lhs rhs
   simp [ExprCnstr.denote, PolyCnstr.denote, ExprCnstr.toPoly];
   by_cases h : eq = true <;> simp [h]
-  . simp [Poly.denote_eq, Expr.toPoly]
-  . simp [Poly.denote_le, Expr.toPoly]
+  · simp [Poly.denote_eq, Expr.toPoly]
+  · simp [Poly.denote_le, Expr.toPoly]
 
 attribute [local simp] ExprCnstr.denote_toPoly
 
@@ -569,8 +569,8 @@ theorem ExprCnstr.denote_toNormPoly (ctx : Context) (c : ExprCnstr) : c.toNormPo
   cases c; rename_i eq lhs rhs
   simp [ExprCnstr.denote, PolyCnstr.denote, ExprCnstr.toNormPoly]
   by_cases h : eq = true <;> simp [h]
-  . rw [Poly.denote_eq_cancel_eq]; simp [Poly.denote_eq, Expr.toNormPoly, Poly.norm]
-  . rw [Poly.denote_le_cancel_eq]; simp [Poly.denote_le, Expr.toNormPoly, Poly.norm]
+  · rw [Poly.denote_eq_cancel_eq]; simp [Poly.denote_eq, Expr.toNormPoly, Poly.norm]
+  · rw [Poly.denote_le_cancel_eq]; simp [Poly.denote_le, Expr.toNormPoly, Poly.norm]
 
 attribute [local simp] ExprCnstr.denote_toNormPoly
 
@@ -593,10 +593,10 @@ theorem PolyCnstr.denote_mul (ctx : Context) (k : Nat) (c : PolyCnstr) : (c.mul
   have : (1 == 1) = true         := rfl
   by_cases he : eq = true <;> simp [he, PolyCnstr.mul, PolyCnstr.denote, Poly.denote_le, Poly.denote_eq]
      <;> by_cases hk : k == 0 <;> (try simp [eq_of_beq hk]) <;> simp [*] <;> apply propext <;> apply Iff.intro <;> intro h
-  . exact Nat.eq_of_mul_eq_mul_left (Nat.zero_lt_succ _) h
-  . rw [h]
-  . exact Nat.le_of_mul_le_mul_left h (Nat.zero_lt_succ _)
-  . apply Nat.mul_le_mul_left _ h
+  · exact Nat.eq_of_mul_eq_mul_left (Nat.zero_lt_succ _) h
+  · rw [h]
+  · exact Nat.le_of_mul_le_mul_left h (Nat.zero_lt_succ _)
+  · apply Nat.mul_le_mul_left _ h
 
 end
 
@@ -607,10 +607,10 @@ theorem PolyCnstr.denote_combine {ctx : Context} {c₁ c₂ : PolyCnstr} (h₁ :
   simp [denote] at h₁ h₂
   simp [PolyCnstr.combine, denote]
   by_cases he₁ : eq₁ = true <;> by_cases he₂ : eq₂ = true <;> simp [he₁, he₂] at h₁ h₂ |-
-  . rw [Poly.denote_eq_cancel_eq]; simp [Poly.denote_eq] at h₁ h₂ |-; simp [h₁, h₂]
-  . rw [Poly.denote_le_cancel_eq]; simp [Poly.denote_eq, Poly.denote_le] at h₁ h₂ |-; rw [h₁]; apply Nat.add_le_add_left h₂
-  . rw [Poly.denote_le_cancel_eq]; simp [Poly.denote_eq, Poly.denote_le] at h₁ h₂ |-; rw [h₂]; apply Nat.add_le_add_right h₁
-  . rw [Poly.denote_le_cancel_eq]; simp [Poly.denote_eq, Poly.denote_le] at h₁ h₂ |-; apply Nat.add_le_add h₁ h₂
+  · rw [Poly.denote_eq_cancel_eq]; simp [Poly.denote_eq] at h₁ h₂ |-; simp [h₁, h₂]
+  · rw [Poly.denote_le_cancel_eq]; simp [Poly.denote_eq, Poly.denote_le] at h₁ h₂ |-; rw [h₁]; apply Nat.add_le_add_left h₂
+  · rw [Poly.denote_le_cancel_eq]; simp [Poly.denote_eq, Poly.denote_le] at h₁ h₂ |-; rw [h₂]; apply Nat.add_le_add_right h₁
+  · rw [Poly.denote_le_cancel_eq]; simp [Poly.denote_eq, Poly.denote_le] at h₁ h₂ |-; apply Nat.add_le_add h₁ h₂
 
 attribute [local simp] PolyCnstr.denote_combine
 
@@ -624,26 +624,26 @@ theorem Poly.isNum?_eq_some (ctx : Context) {p : Poly} {k : Nat} : p.isNum? = so
 theorem Poly.of_isZero (ctx : Context) {p : Poly} (h : isZero p = true) : p.denote ctx = 0 := by
   simp [isZero] at h
   split at h
-  . simp
-  . contradiction
+  · simp
+  · contradiction
 
 theorem Poly.of_isNonZero (ctx : Context) {p : Poly} (h : isNonZero p = true) : p.denote ctx > 0 := by
   match p with
   | [] => contradiction
   | (k, v) :: p =>
     by_cases he : v == fixedVar <;> simp [he, isNonZero] at h ⊢
-    . simp [eq_of_beq he, Var.denote]; apply Nat.lt_of_succ_le; exact Nat.le_trans h (Nat.le_add_right ..)
-    . have ih := of_isNonZero ctx h
+    · simp [eq_of_beq he, Var.denote]; apply Nat.lt_of_succ_le; exact Nat.le_trans h (Nat.le_add_right ..)
+    · have ih := of_isNonZero ctx h
       exact Nat.le_trans ih (Nat.le_add_right ..)
 
 theorem PolyCnstr.eq_false_of_isUnsat (ctx : Context) {c : PolyCnstr} : c.isUnsat → c.denote ctx = False := by
   cases c; rename_i eq lhs rhs
   simp [isUnsat]
   by_cases he : eq = true <;> simp [he, denote, Poly.denote_eq, Poly.denote_le]
-  . intro
+  · intro
       | Or.inl ⟨h₁, h₂⟩ => simp [Poly.of_isZero, h₁]; have := Nat.not_eq_zero_of_lt (Poly.of_isNonZero ctx h₂); simp [this.symm]
       | Or.inr ⟨h₁, h₂⟩ => simp [Poly.of_isZero, h₂]; have := Nat.not_eq_zero_of_lt (Poly.of_isNonZero ctx h₁); simp [this]
-  . intro ⟨h₁, h₂⟩
+  · intro ⟨h₁, h₂⟩
     simp [Poly.of_isZero, h₂]
     have := Nat.not_le_of_gt (Poly.of_isNonZero ctx h₁)
     simp [this]
@@ -652,9 +652,9 @@ theorem PolyCnstr.eq_true_of_isValid (ctx : Context) {c : PolyCnstr} : c.isValid
   cases c; rename_i eq lhs rhs
   simp [isValid]
   by_cases he : eq = true <;> simp [he, denote, Poly.denote_eq, Poly.denote_le]
-  . intro ⟨h₁, h₂⟩
+  · intro ⟨h₁, h₂⟩
     simp [Poly.of_isZero, h₁, h₂]
-  . intro h
+  · intro h
     simp [Poly.of_isZero, h]
     have := Nat.zero_le (Poly.denote ctx rhs)
     simp [this]
@@ -696,8 +696,8 @@ theorem Certificate.of_combine_isUnsat (ctx : Context) (cs : Certificate) (h : c
 theorem denote_monomialToExpr (ctx : Context) (k : Nat) (v : Var) : (monomialToExpr k v).denote ctx = k * v.denote ctx := by
   simp [monomialToExpr]
   by_cases h : v == fixedVar <;> simp [h, Expr.denote]
-  . simp [eq_of_beq h, Var.denote]
-  . by_cases h : k == 1 <;> simp [h, Expr.denote]; simp [eq_of_beq h]
+  · simp [eq_of_beq h, Var.denote]
+  · by_cases h : k == 1 <;> simp [h, Expr.denote]; simp [eq_of_beq h]
 
 attribute [local simp] denote_monomialToExpr
 
diff --git a/tests/lean/run/1024.lean b/tests/lean/run/1024.lean
index b00887c6f5..25ed557243 100644
--- a/tests/lean/run/1024.lean
+++ b/tests/lean/run/1024.lean
@@ -16,14 +16,14 @@ namespace Vector
     (v.snoc x).nth k = x := by
     cases k; rename_i k hk
     induction v generalizing k <;> subst h
-    . simp only [nth]
-    . simp_all[nth]
+    · simp only [nth]
+    · simp_all[nth]
 
   theorem nth_snoc_eq_works (k: Fin (n+1))(v : Vector α n)
     (h: k.val = n):
     (v.snoc x).nth k = x := by
     cases k; rename_i k hk
     induction v generalizing k <;> subst h
-    . simp only [nth]
-    . simp[*,nth]
+    · simp only [nth]
+    · simp[*,nth]
 end Vector
diff --git a/tests/lean/run/1025.lean b/tests/lean/run/1025.lean
index 3f9c637971..238cdce884 100644
--- a/tests/lean/run/1025.lean
+++ b/tests/lean/run/1025.lean
@@ -15,6 +15,6 @@ namespace Vector
     (h: v.mem y):
     f y ≤ v.foldr (λ x acc => max (f x) acc) init := by
     induction v <;> simp only[foldr,max]
-    . admit
-    . split <;> admit
+    · admit
+    · split <;> admit
 end Vector
diff --git a/tests/lean/run/501.lean b/tests/lean/run/501.lean
index 9e02d49d7e..c2e68857b3 100644
--- a/tests/lean/run/501.lean
+++ b/tests/lean/run/501.lean
@@ -26,5 +26,5 @@ theorem pow_nonneg : ∀ m : Nat, 0 ^ m ≥ 0
   | 0 => by decide
   | m@(_+1) => by
     rw [zeropow]
-    . decide
-    . apply Nat.zero_lt_succ
+    · decide
+    · apply Nat.zero_lt_succ
diff --git a/tests/lean/run/860.lean b/tests/lean/run/860.lean
index 7185b8c4e8..f19f89173f 100644
--- a/tests/lean/run/860.lean
+++ b/tests/lean/run/860.lean
@@ -6,11 +6,11 @@ private theorem pack_loop_terminates : (n : Nat) → n / 2 < n.succ
   | n+2 => by
     rw [Nat.div_eq]
     split
-    . rw [Nat.add_sub_self_right]
+    · rw [Nat.add_sub_self_right]
       have := pack_loop_terminates n
       calc n/2 + 1 < Nat.succ n + 1   := Nat.add_le_add_right this 1
              _     < Nat.succ (n + 2) := Nat.succ_lt_succ (Nat.succ_lt_succ (Nat.lt_succ_self _))
-    . apply Nat.zero_lt_succ
+    · apply Nat.zero_lt_succ
 
 def pack (n: Nat) : List Nat :=
   let rec loop (n : Nat) (acc : Nat) (accs: List Nat) : List Nat :=
diff --git a/tests/lean/run/def10.lean b/tests/lean/run/def10.lean
index 48f2d92654..a91dff8191 100644
--- a/tests/lean/run/def10.lean
+++ b/tests/lean/run/def10.lean
@@ -19,8 +19,8 @@ theorem ex5 : g false true true = 3 := rfl
 theorem f_eq (h : a = true → b = true → False) : f a b = 3 := by
   simp [f]
   split
-  . contradiction
-  . rfl
+  · contradiction
+  · rfl
 
 theorem ex6 : g x y z > 0 := by
   simp [g]
diff --git a/tests/lean/run/eqThm.lean b/tests/lean/run/eqThm.lean
index 7ef40eb157..a6aa20d52f 100644
--- a/tests/lean/run/eqThm.lean
+++ b/tests/lean/run/eqThm.lean
@@ -37,9 +37,9 @@ def foo (xs : List Nat) : List Nat :=
 
 theorem foo_main_eq (xs : List Nat) : foo xs = foo.match_1 (fun _ => List Nat) xs (fun _ => []) (fun x xs => let y := 2*x; foo.match_1 (fun _ => List Nat) xs (fun _ => []) (fun x xs => (y + x)::foo xs)) := by
   split
-  . rfl
-  . split
-    . rfl
-    . rfl
+  · rfl
+  · split
+    · rfl
+    · rfl
 
 #check @foo_main_eq
diff --git a/tests/lean/run/overAndPartialAppsAtWF.lean b/tests/lean/run/overAndPartialAppsAtWF.lean
index c7e4b79dec..62281b3b2f 100644
--- a/tests/lean/run/overAndPartialAppsAtWF.lean
+++ b/tests/lean/run/overAndPartialAppsAtWF.lean
@@ -1,13 +1,13 @@
 theorem eq_of_isEqvAux [DecidableEq α] (a b : Array α) (hsz : a.size = b.size) (i : Nat) (hi : i ≤ a.size) (heqv : Array.isEqvAux a b hsz (fun x y => x = y) i) : ∀ (j : Nat) (hl : i ≤ j) (hj : j < a.size), a.get ⟨j, hj⟩ = b.get ⟨j, hsz ▸ hj⟩ := by
   intro j low high
   by_cases h : i < a.size
-  . unfold Array.isEqvAux at heqv
+  · unfold Array.isEqvAux at heqv
     simp [h] at heqv
     have hind := eq_of_isEqvAux a b hsz (i+1) (Nat.succ_le_of_lt h) heqv.2
     by_cases heq : i = j
-    . subst heq; exact heqv.1
-    . exact hind j (Nat.succ_le_of_lt (Nat.lt_of_le_and_ne low heq)) high
-  . have heq : i = a.size := Nat.le_antisymm hi (Nat.ge_of_not_lt h)
+    · subst heq; exact heqv.1
+    · exact hind j (Nat.succ_le_of_lt (Nat.lt_of_le_and_ne low heq)) high
+  · have heq : i = a.size := Nat.le_antisymm hi (Nat.ge_of_not_lt h)
     subst heq
     exact absurd (Nat.lt_of_lt_of_le high low) (Nat.lt_irrefl j)
 termination_by _ => a.size - i
diff --git a/tests/lean/run/specialize2.lean b/tests/lean/run/specialize2.lean
index 8024199996..55b62870eb 100644
--- a/tests/lean/run/specialize2.lean
+++ b/tests/lean/run/specialize2.lean
@@ -1,11 +1,11 @@
 example : (p → q → False) ↔ (¬ p ∨ ¬ q) := by
   apply Iff.intro
-  . intro h
+  · intro h
     by_cases hp:p <;> by_cases hq:q
-    . specialize h hp hq; contradiction
-    . exact Or.inr hq
-    . exact Or.inl hp
-    . exact Or.inr hq
-  . intro
+    · specialize h hp hq; contradiction
+    · exact Or.inr hq
+    · exact Or.inl hp
+    · exact Or.inr hq
+  · intro
     | Or.inl hnp => intros; contradiction
     | Or.inr hnq => intros; contradiction
diff --git a/tests/lean/run/split2.lean b/tests/lean/run/split2.lean
index 5f4de57ba2..434a655f8f 100644
--- a/tests/lean/run/split2.lean
+++ b/tests/lean/run/split2.lean
@@ -9,19 +9,19 @@ example (x y z : Nat) : x ≠ 5 → y ≠ 5 → z ≠ 5 → f x y z = 1 := by
   intros
   simp [f]
   split
-  . contradiction
-  . contradiction
-  . contradiction
-  . rfl
+  · contradiction
+  · contradiction
+  · contradiction
+  · rfl
 
 example (x y z : Nat) : f x y z = y ∨ f x y z = 1 := by
   intros
   simp [f]
   split
-  . exact Or.inl rfl
-  . exact Or.inl rfl
-  . exact Or.inl rfl
-  . exact Or.inr rfl
+  · exact Or.inl rfl
+  · exact Or.inl rfl
+  · exact Or.inl rfl
+  · exact Or.inr rfl
 
 example (x y z : Nat) : f x y z = y ∨ f x y z = 1 := by
   intros
diff --git a/tests/lean/run/split3.lean b/tests/lean/run/split3.lean
index 1dfb00be9e..7a1da30984 100644
--- a/tests/lean/run/split3.lean
+++ b/tests/lean/run/split3.lean
@@ -17,8 +17,8 @@ example (a b : Bool) (x y z : Nat) (xs : List Nat) (h1 : (if a then x else y) =
 
 example (a : Bool) (h1 : (if a then x else y) = 1) : x + y > 0 := by
   split at h1
-  . subst h1; rw [Nat.succ_add]; apply Nat.zero_lt_succ
-  . subst h1; apply Nat.zero_lt_succ
+  · subst h1; rw [Nat.succ_add]; apply Nat.zero_lt_succ
+  · subst h1; apply Nat.zero_lt_succ
 
 def f (x : Nat) : Nat :=
   match x with
@@ -29,9 +29,9 @@ def f (x : Nat) : Nat :=
 example (h1 : f x = 0) (h2 : x > 300) : False := by
   simp [f] at h1
   split at h1
-  . contradiction
-  . contradiction
-  . contradiction
+  · contradiction
+  · contradiction
+  · contradiction
 
 example (h1 : f x = 0) (h2 : x > 300) : False := by
   simp [f] at h1
diff --git a/tests/lean/run/tactic1.lean b/tests/lean/run/tactic1.lean
index 3785e5945a..8f3ed2fbed 100644
--- a/tests/lean/run/tactic1.lean
+++ b/tests/lean/run/tactic1.lean
@@ -61,9 +61,9 @@ example (x y z : Nat) (h₁ : x = y) (h₂ : z = y) : x = z := by
 
 example (x y z : Nat) (h₁ : x = y) (h₂ : z = y) : x = z := by
   apply Eq.trans
-  . sorry
-  . sorry
-  . sorry
+  · sorry
+  · sorry
+  · sorry
 
 example (x y z : Nat) (h₁ : x = y) (h₂ : z = y) : x = z := by
   apply Eq.trans <;> sorry
diff --git a/tests/lean/run/wfOverapplicationIssue.lean b/tests/lean/run/wfOverapplicationIssue.lean
index 4522ed8e60..fcc2cd14d3 100644
--- a/tests/lean/run/wfOverapplicationIssue.lean
+++ b/tests/lean/run/wfOverapplicationIssue.lean
@@ -4,9 +4,9 @@ theorem Array.sizeOf_lt_of_mem' [DecidableEq α] [SizeOf α] {as : Array α} (h
     unfold anyM.loop
     intro h
     split at h
-    . simp [Bind.bind, pure] at h; split at h
+    · simp [Bind.bind, pure] at h; split at h
       next he => subst a; apply sizeOf_get_lt
       next => have ih := aux (j+1) h; assumption
-    . contradiction
+    · contradiction
   apply aux 0 h
 termination_by aux j => as.size - j
diff --git a/tests/lean/tacUnsolvedGoalsErrors.lean b/tests/lean/tacUnsolvedGoalsErrors.lean
index ffc8605f23..54644d28f6 100644
--- a/tests/lean/tacUnsolvedGoalsErrors.lean
+++ b/tests/lean/tacUnsolvedGoalsErrors.lean
@@ -23,7 +23,7 @@ theorem ex4 (p q r : Prop) (h1 : p ∨ q) (h2 : p → q) : q := by
 
 theorem ex5 (p q r : Prop) (h1 : p ∨ q) (h2 : p → q) : q := by
   cases h1
-  . skip  -- Error here
+  · skip  -- Error here
     skip
-  . skip  -- Error here
+  · skip  -- Error here
     skip