diff --git a/doc/tactics.md b/doc/tactics.md
index 6c7dfca37c..c24f142cf8 100644
--- a/doc/tactics.md
+++ b/doc/tactics.md
@@ -176,11 +176,11 @@ theorem ex (x : Nat) {y : Nat} (h : y > 0) : x % y < y := by
     rw [Nat.mod_eq_sub_mod h₁.2]
     exact ih h
   | base x y h₁ =>
-     have ¬ 0 < y ∨ ¬ y ≤ x from Iff.mp (Decidable.notAndIffOrNot ..) h₁
+     have : ¬ 0 < y ∨ ¬ y ≤ x := Iff.mp (Decidable.notAndIffOrNot ..) h₁
      match this with
      | Or.inl h₁ => exact absurd h h₁
      | Or.inr h₁ =>
-       have hgt : y > x from Nat.gtOfNotLe h₁
+       have hgt : y > x := Nat.gtOfNotLe h₁
        rw [← Nat.mod_eq_of_lt hgt] at hgt
        assumption
 ```
diff --git a/src/Init/Classical.lean b/src/Init/Classical.lean
index 9ff9ff36ea..138c3b1984 100644
--- a/src/Init/Classical.lean
+++ b/src/Init/Classical.lean
@@ -28,30 +28,30 @@ theorem chooseSpec {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : p (choose
 theorem em (p : Prop) : p ∨ ¬p :=
   let U (x : Prop) : Prop := x = True ∨ p;
   let V (x : Prop) : Prop := x = False ∨ p;
-  have exU : ∃ x, U x from ⟨True, Or.inl rfl⟩;
-  have exV : ∃ x, V x from ⟨False, Or.inl rfl⟩;
+  have exU : ∃ x, U x := ⟨True, Or.inl rfl⟩;
+  have exV : ∃ x, V x := ⟨False, Or.inl rfl⟩;
   let u : Prop := choose exU;
   let v : Prop := choose exV;
-  have uDef : U u from chooseSpec exU;
-  have vDef : V v from chooseSpec exV;
-  have notUvOrP : u ≠ v ∨ p from
+  have uDef : U u := chooseSpec exU;
+  have vDef : V v := chooseSpec exV;
+  have notUvOrP : u ≠ v ∨ p :=
     match uDef, vDef with
     | Or.inr h, _ => Or.inr h
     | _, Or.inr h => Or.inr h
     | Or.inl hut, Or.inl hvf =>
-      have hne : u ≠ v from hvf.symm ▸ hut.symm ▸ trueNeFalse
+      have hne : u ≠ v := hvf.symm ▸ hut.symm ▸ trueNeFalse
       Or.inl hne
-  have pImpliesUv : p → u = v from
+  have pImpliesUv : p → u = v :=
     fun hp =>
-    have hpred : U = V from
+    have hpred : U = V :=
       funext fun x =>
-        have hl : (x = True ∨ p) → (x = False ∨ p) from
+        have hl : (x = True ∨ p) → (x = False ∨ p) :=
           fun a => Or.inr hp;
-        have hr : (x = False ∨ p) → (x = True ∨ p) from
+        have hr : (x = False ∨ p) → (x = True ∨ p) :=
           fun a => Or.inr hp;
         show (x = True ∨ p) = (x = False ∨ p) from
           propext (Iff.intro hl hr);
-    have h₀ : ∀ exU exV, @choose _ U exU = @choose _ V exV from
+    have h₀ : ∀ exU exV, @choose _ U exU = @choose _ V exV :=
       hpred ▸ fun exU exV => rfl;
     show u = v from h₀ ..;
   match notUvOrP with
diff --git a/src/Init/Control/Lawful.lean b/src/Init/Control/Lawful.lean
index d400331b7e..ab1848d88d 100644
--- a/src/Init/Control/Lawful.lean
+++ b/src/Init/Control/Lawful.lean
@@ -75,7 +75,7 @@ theorem bind_congr [Bind m] {x : m α} {f g : α → m β} (h : ∀ a, f a = g a
   simp [funext h]
 
 @[simp] theorem bind_pure_unit [Monad m] [LawfulMonad m] {x : m PUnit} : (x >>= fun _ => pure ⟨⟩) = x := by
-  have (x >>= fun _ => pure ⟨⟩) = (x >>= pure) by
+  have : (x >>= fun _ => pure ⟨⟩) = (x >>= pure) := by
     apply bind_congr; intro u
     cases u; simp
   rw [bind_pure] at this
diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 413e5eda21..bf0495da2c 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -222,7 +222,7 @@ theorem neFalseOfSelf : p → p ≠ False :=
 
 theorem neTrueOfNot : ¬p → p ≠ True :=
   fun (hnp : ¬p) (h : p = True) =>
-    have ¬True from h ▸ hnp
+    have : ¬True := h ▸ hnp
     this trivial
 
 theorem trueNeFalse : ¬True = False :=
diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index a084b98f77..e5c08dc348 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -90,7 +90,7 @@ def swapAt! (a : Array α) (i : Nat) (v : α) : α × Array α :=
   if h : i < a.size then
     swapAt a ⟨i, h⟩ v
   else
-    have Inhabited α from ⟨v⟩
+    have : Inhabited α := ⟨v⟩
     panic! ("index " ++ toString i ++ " out of bounds")
 
 @[extern "lean_array_pop"]
@@ -143,7 +143,7 @@ def modifyOp [Inhabited α] (self : Array α) (idx : Nat) (f : α → α) : Arra
 private theorem zeroLtOfLt : {a b : Nat} → a < b → 0 < b
   | 0,   _, h => h
   | a+1, b, h =>
-    have a < b from Nat.ltTrans (Nat.ltSuccSelf _) h
+    have : a < b := Nat.ltTrans (Nat.ltSuccSelf _) h
     zeroLtOfLt this
 
 /- Reference implementation for `forIn` -/
@@ -153,9 +153,9 @@ protected def forIn {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m
     match i, h with
     | 0,   _ => pure b
     | i+1, h =>
-      have h' : i < as.size          from Nat.ltOfLtOfLe (Nat.ltSuccSelf i) h
-      have as.size - 1 < as.size     from Nat.subLt (zeroLtOfLt h') (by decide)
-      have as.size - 1 - i < as.size from Nat.ltOfLeOfLt (Nat.subLe (as.size - 1) i) this
+      have h' : i < as.size            := Nat.ltOfLtOfLe (Nat.ltSuccSelf i) h
+      have : as.size - 1 < as.size     := Nat.subLt (zeroLtOfLt h') (by decide)
+      have : as.size - 1 - i < as.size := Nat.ltOfLeOfLt (Nat.subLe (as.size - 1) i) this
       match (← f (as.get ⟨as.size - 1 - i, this⟩) b) with
       | ForInStep.done b  => pure b
       | ForInStep.yield b => loop i (Nat.leOfLt h') b
@@ -225,7 +225,7 @@ def foldrM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α
     else match i, h with
       | 0, _   => pure b
       | i+1, h =>
-        have i < as.size from Nat.ltOfLtOfLe (Nat.ltSuccSelf _) h
+        have : i < as.size := Nat.ltOfLtOfLe (Nat.ltSuccSelf _) h
         fold i (Nat.leOfLt this) (← f (as.get ⟨i, this⟩) b)
   if h : start ≤ as.size then
     if stop < start then
@@ -262,9 +262,9 @@ def mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as :
     match i, inv with
     | 0,    _  => pure bs
     | i+1, inv =>
-      have j < as.size by rw [← inv, Nat.add_assoc, Nat.add_comm 1 j, Nat.add_left_comm]; apply Nat.leAddRight
+      have : j < as.size := by rw [← inv, Nat.add_assoc, Nat.add_comm 1 j, Nat.add_left_comm]; apply Nat.leAddRight
       let idx : Fin as.size := ⟨j, this⟩
-      have i + (j + 1) = as.size by rw [← inv, Nat.add_comm j 1, Nat.add_assoc]
+      have : i + (j + 1) = as.size := by rw [← inv, Nat.add_comm j 1, Nat.add_assoc]
       map i (j+1) this (bs.push (← f idx (as.get idx)))
   map as.size 0 rfl (mkEmpty as.size)
 
@@ -339,12 +339,12 @@ def findSomeRevM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m]
   let rec @[specialize] find : (i : Nat) → i ≤ as.size → m (Option β)
     | 0,   h => pure none
     | i+1, h => do
-      have i < as.size from Nat.ltOfLtOfLe (Nat.ltSuccSelf _) h
+      have : i < as.size := Nat.ltOfLtOfLe (Nat.ltSuccSelf _) h
       let r ← f (as.get ⟨i, this⟩)
       match r with
       | some v => pure r
       | none   =>
-        have i ≤ as.size from Nat.leOfLt this
+        have : i ≤ as.size := Nat.leOfLt this
         find i this
   find as.size (Nat.leRefl _)
 
@@ -412,7 +412,7 @@ def findIdx? {α : Type u} (as : Array α) (p : α → Bool) : Option Nat :=
         if p (as.get ⟨j, hlt⟩) then
           some j
         else
-          have i + (j+1) = as.size by
+          have : i + (j+1) = as.size := by
             rw [← inv, Nat.add_comm j 1, Nat.add_assoc]
           loop i (j+1) this
     else
@@ -576,17 +576,17 @@ theorem ext (a b : Array α)
       cases b with
       | nil => rw [List.length_cons] at h₁; injection h₁
       | cons b bs =>
-        have hz₁ : 0 < (a::as).length by rw [List.length_cons]; apply Nat.zeroLtSucc
-        have hz₂ : 0 < (b::bs).length by rw [List.length_cons]; apply Nat.zeroLtSucc
-        have headEq : a = b from h₂ 0 hz₁ hz₂
-        have h₁' : as.length = bs.length by rw [List.length_cons, List.length_cons] at h₁; injection h₁; assumption
-        have h₂' : (i : Nat) → (hi₁ : i < as.length) → (hi₂ : i < bs.length) → as.get i hi₁ = bs.get i hi₂ by
+        have hz₁ : 0 < (a::as).length := by rw [List.length_cons]; apply Nat.zeroLtSucc
+        have hz₂ : 0 < (b::bs).length := by rw [List.length_cons]; apply Nat.zeroLtSucc
+        have headEq : a = b := h₂ 0 hz₁ hz₂
+        have h₁' : as.length = bs.length := by rw [List.length_cons, List.length_cons] at h₁; injection h₁; assumption
+        have h₂' : (i : Nat) → (hi₁ : i < as.length) → (hi₂ : i < bs.length) → as.get i hi₁ = bs.get i hi₂ := by
           intro i hi₁ hi₂
-          have hi₁' : i+1 < (a::as).length by rw [List.length_cons]; apply Nat.succ_lt_succ; assumption
-          have hi₂' : i+1 < (b::bs).length by rw [List.length_cons]; apply Nat.succ_lt_succ; assumption
-          have (a::as).get (i+1) hi₁' = (b::bs).get (i+1) hi₂' from h₂ (i+1) hi₁' hi₂'
+          have hi₁' : i+1 < (a::as).length := by rw [List.length_cons]; apply Nat.succ_lt_succ; assumption
+          have hi₂' : i+1 < (b::bs).length := by rw [List.length_cons]; apply Nat.succ_lt_succ; assumption
+          have : (a::as).get (i+1) hi₁' = (b::bs).get (i+1) hi₂' := h₂ (i+1) hi₁' hi₂'
           apply this
-        have tailEq : as = bs from ih bs h₁' h₂'
+        have tailEq : as = bs := ih bs h₁' h₂'
         rw [headEq, tailEq]
   cases a; cases b
   apply congrArg
@@ -748,7 +748,7 @@ def isPrefixOf [BEq α] (as bs : Array α) : Bool :=
 private def allDiffAuxAux [BEq α] (as : Array α) (a : α) : forall (i : Nat), i < as.size → Bool
   | 0,   h => true
   | i+1, h =>
-    have i < as.size from Nat.ltTrans (Nat.ltSuccSelf _) h;
+    have : i < as.size := Nat.ltTrans (Nat.ltSuccSelf _) h;
     a != as.get ⟨i, this⟩ && allDiffAuxAux as a i this
 
 private partial def allDiffAux [BEq α] (as : Array α) : Nat → Bool
diff --git a/src/Init/Data/Array/InsertionSort.lean b/src/Init/Data/Array/InsertionSort.lean
index 6b6cdaa83c..4aca4e50d9 100644
--- a/src/Init/Data/Array/InsertionSort.lean
+++ b/src/Init/Data/Array/InsertionSort.lean
@@ -21,7 +21,7 @@ where
     match he:j with
     | 0    => a
     | j'+1 =>
-      have h' : j' < a.size by subst j; exact Nat.ltTrans (Nat.ltSuccSelf _) h
+      have h' : j' < a.size := by subst j; exact Nat.ltTrans (Nat.ltSuccSelf _) h
       if lt (a.get ⟨j, h⟩) (a.get ⟨j', h'⟩) then
         swapLoop (a.swap ⟨j, h⟩ ⟨j', h'⟩) j' (by rw [size_swap]; assumption done)
       else
diff --git a/src/Init/Data/Fin/Basic.lean b/src/Init/Data/Fin/Basic.lean
index a91785d334..84ef5c1163 100644
--- a/src/Init/Data/Fin/Basic.lean
+++ b/src/Init/Data/Fin/Basic.lean
@@ -29,7 +29,7 @@ protected def ofNat' {n : Nat} (a : Nat) (h : n > 0) : Fin n :=
 private theorem mlt {b : Nat} : {a : Nat} → a < n → b % n < n
   | 0,   h => Nat.mod_lt _ h
   | a+1, h =>
-    have n > 0 from Nat.ltTrans (Nat.zeroLtSucc _) h;
+    have : n > 0 := Nat.ltTrans (Nat.zeroLtSucc _) h;
     Nat.mod_lt _ this
 
 protected def add : Fin n → Fin n → Fin n
diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean
index 550b65c781..230a30725d 100644
--- a/src/Init/Data/Nat/Basic.lean
+++ b/src/Init/Data/Nat/Basic.lean
@@ -67,7 +67,7 @@ theorem succ_Eq_add_one (n : Nat) : succ n = n + 1 :=
 protected theorem add_comm : ∀ (n m : Nat), n + m = m + n
   | n, 0   => Eq.symm (Nat.zero_add n)
   | n, m+1 => by
-    have succ (n + m) = succ (m + n) by apply congrArg; apply Nat.add_comm
+    have : succ (n + m) = succ (m + n) := by apply congrArg; apply Nat.add_comm
     rw [succ_add m n]
     apply this
 
@@ -123,21 +123,21 @@ protected theorem left_distrib (n m k : Nat) : n * (m + k) = n * m + n * k := by
   | succ n ih => simp [succ_mul, ih]; rw [Nat.add_assoc, Nat.add_assoc (n*m)]; apply congrArg; apply Nat.add_left_comm
 
 protected theorem right_distrib (n m k : Nat) : (n + m) * k = n * k + m * k :=
-  have h₁ : (n + m) * k = k * (n + m)     from Nat.mul_comm ..
-  have h₂ : k * (n + m) = k * n + k * m   from Nat.left_distrib ..
-  have h₃ : k * n + k * m = n * k + k * m from Nat.mul_comm n k ▸ rfl
-  have h₄ : n * k + k * m = n * k + m * k from Nat.mul_comm m k ▸ rfl
+  have h₁ : (n + m) * k = k * (n + m)     := Nat.mul_comm ..
+  have h₂ : k * (n + m) = k * n + k * m   := Nat.left_distrib ..
+  have h₃ : k * n + k * m = n * k + k * m := Nat.mul_comm n k ▸ rfl
+  have h₄ : n * k + k * m = n * k + m * k := Nat.mul_comm m k ▸ rfl
   ((h₁.trans h₂).trans h₃).trans h₄
 
 protected theorem mul_assoc : ∀ (n m k : Nat), (n * m) * k = n * (m * k)
   | n, m, 0      => rfl
   | n, m, succ k =>
-    have h₁ : n * m * succ k = n * m * (k + 1)              from rfl
-    have h₂ : n * m * (k + 1) = (n * m * k) + n * m * 1     from Nat.left_distrib ..
-    have h₃ : (n * m * k) + n * m * 1 = (n * m * k) + n * m by rw [Nat.mul_one (n*m)]
-    have h₄ : (n * m * k) + n * m = (n * (m * k)) + n * m   by rw [Nat.mul_assoc n m k]
-    have h₅ : (n * (m * k)) + n * m = n * (m * k + m)       from (Nat.left_distrib n (m*k) m).symm
-    have h₆ : n * (m * k + m) = n * (m * succ k)            from Nat.mul_succ m k ▸ rfl
+    have h₁ : n * m * succ k = n * m * (k + 1)              := rfl
+    have h₂ : n * m * (k + 1) = (n * m * k) + n * m * 1     := Nat.left_distrib ..
+    have h₃ : (n * m * k) + n * m * 1 = (n * m * k) + n * m := by rw [Nat.mul_one (n*m)]
+    have h₄ : (n * m * k) + n * m = (n * (m * k)) + n * m   := by rw [Nat.mul_assoc n m k]
+    have h₅ : (n * (m * k)) + n * m = n * (m * k + m)       := (Nat.left_distrib n (m*k) m).symm
+    have h₆ : n * (m * k + m) = n * (m * succ k)            := Nat.mul_succ m k ▸ rfl
     ((((h₁.trans h₂).trans h₃).trans h₄).trans h₅).trans h₆
 
 /- Inequalities -/
@@ -254,8 +254,8 @@ theorem ltOrEqOrLeSucc {m n : Nat} (h : m ≤ succ n) : m ≤ n ∨ m = succ n :
   Decidable.byCases
     (fun (h' : m = succ n) => Or.inr h')
     (fun (h' : m ≠ succ n) =>
-       have m < succ n from Nat.ltOfLeAndNe h h'
-       have succ m ≤ succ n from succLeOfLt this
+       have : m < succ n := Nat.ltOfLeAndNe h h'
+       have : succ m ≤ succ n := succLeOfLt this
        Or.inl (leOfSuccLeSucc this))
 
 theorem leAddRight : ∀ (n k : Nat), n ≤ n + k
@@ -270,8 +270,8 @@ theorem le.dest : ∀ {n m : Nat}, n ≤ m → Exists (fun k => n + k = m)
   | zero,   succ n, h => ⟨succ n, Nat.add_comm 0 (succ n) ▸ rfl⟩
   | succ n, zero,   h => Bool.noConfusion h
   | succ n, succ m, h =>
-    have n ≤ m from h
-    have Exists (fun k => n + k = m) from dest this
+    have : n ≤ m := h
+    have : Exists (fun k => n + k = m) := dest this
     match this with
     | ⟨k, h⟩ => ⟨k, show succ n + k = succ m from ((succ_add n k).symm ▸ h ▸ rfl)⟩
 
@@ -282,7 +282,7 @@ protected theorem notLeOfGt {n m : Nat} (h : n > m) : ¬ n ≤ m := fun h₁ =>
   match Nat.ltOrGe n m with
   | Or.inl h₂ => absurd (Nat.ltTrans h h₂) (Nat.ltIrrefl _)
   | Or.inr h₂ =>
-    have Heq : n = m from Nat.leAntisymm h₁ h₂
+    have Heq : n = m := Nat.leAntisymm h₁ h₂
     absurd (@Eq.subst _ _ _ _ Heq h) (Nat.ltIrrefl m)
 
 theorem gtOfNotLe {n m : Nat} (h : ¬ n ≤ m) : n > m :=
@@ -293,8 +293,8 @@ theorem gtOfNotLe {n m : Nat} (h : ¬ n ≤ m) : n > m :=
 protected theorem addLeAddLeft {n m : Nat} (h : n ≤ m) (k : Nat) : k + n ≤ k + m :=
   match le.dest h with
   | ⟨w, hw⟩ =>
-    have h₁ : k + n + w = k + (n + w) from Nat.add_assoc ..
-    have h₂ : k + (n + w) = k + m     from congrArg _ hw
+    have h₁ : k + n + w = k + (n + w) := Nat.add_assoc ..
+    have h₂ : k + (n + w) = k + m     := congrArg _ hw
     le.intro <| h₁.trans h₂
 
 protected theorem addLeAddRight {n m : Nat} (h : n ≤ m) (k : Nat) : n + k ≤ m + k := by
@@ -336,7 +336,7 @@ theorem succNeZero (n : Nat) : succ n ≠ 0 :=
 theorem mulLeMulLeft {n m : Nat} (k : Nat) (h : n ≤ m) : k * n ≤ k * m :=
   match le.dest h with
   | ⟨l, hl⟩ =>
-    have k * n + k * l = k * m from Nat.left_distrib k n l ▸ hl.symm ▸ rfl
+    have : k * n + k * l = k * m := Nat.left_distrib k n l ▸ hl.symm ▸ rfl
     le.intro this
 
 theorem mulLeMulRight {n m : Nat} (k : Nat) (h : n ≤ m) : n * k ≤ m * k :=
@@ -352,7 +352,7 @@ protected theorem mulLtMulOfPosRight {n m k : Nat} (h : n < m) (hk : k > 0) : n
   Nat.mul_comm k m ▸ Nat.mul_comm k n ▸ Nat.mulLtMulOfPosLeft h hk
 
 protected theorem mulPos {n m : Nat} (ha : n > 0) (hb : m > 0) : n * m > 0 :=
-  have h : 0 * m < n * m from Nat.mulLtMulOfPosRight ha hb
+  have h : 0 * m < n * m := Nat.mulLtMulOfPosRight ha hb
   Nat.zero_mul m ▸ h
 
 /- power -/
@@ -368,12 +368,12 @@ theorem powLePowOfLeLeft {n m : Nat} (h : n ≤ m) : ∀ (i : Nat), n^i ≤ m^i
 
 theorem powLePowOfLeRight {n : Nat} (hx : n > 0) {i : Nat} : ∀ {j}, i ≤ j → n^i ≤ n^j
   | 0,      h =>
-    have i = 0 from eqZeroOfLeZero h
+    have : i = 0 := eqZeroOfLeZero h
     this.symm ▸ Nat.leRefl _
   | succ j, h =>
     match ltOrEqOrLeSucc h with
     | Or.inl h => show n^i ≤ n^j * n from
-      have n^i * 1 ≤ n^j * n from Nat.mulLeMul (powLePowOfLeRight hx h) hx
+      have : n^i * 1 ≤ n^j * n := Nat.mulLeMul (powLePowOfLeRight hx h) hx
       Nat.mul_one (n^i) ▸ this
     | Or.inr h =>
       h.symm ▸ Nat.leRefl _
diff --git a/src/Init/Data/Nat/Div.lean b/src/Init/Data/Nat/Div.lean
index 729bdf0b41..47acde42d5 100644
--- a/src/Init/Data/Nat/Div.lean
+++ b/src/Init/Data/Nat/Div.lean
@@ -65,14 +65,14 @@ theorem mod.inductionOn.{u}
   div.inductionOn x y ind base
 
 theorem mod_zero (a : Nat) : a % 0 = a :=
-  have (if 0 < 0 ∧ 0 ≤ a then (a - 0) % 0 else a) = a from
-    have h : ¬ (0 < 0 ∧ 0 ≤ a) from fun ⟨h₁, _⟩ => absurd h₁ (Nat.ltIrrefl _)
+  have : (if 0 < 0 ∧ 0 ≤ a then (a - 0) % 0 else a) = a :=
+    have h : ¬ (0 < 0 ∧ 0 ≤ a) := fun ⟨h₁, _⟩ => absurd h₁ (Nat.ltIrrefl _)
     ifNeg h
   (mod_eq a 0).symm ▸ this
 
 theorem mod_eq_of_lt {a b : Nat} (h : a < b) : a % b = a :=
-  have (if 0 < b ∧ b ≤ a then (a - b) % b else a) = a from
-    have h' : ¬(0 < b ∧ b ≤ a) from fun ⟨_, h₁⟩ => absurd h₁ (Nat.notLeOfGt h)
+  have : (if 0 < b ∧ b ≤ a then (a - b) % b else a) = a :=
+    have h' : ¬(0 < b ∧ b ≤ a) := fun ⟨_, h₁⟩ => absurd h₁ (Nat.notLeOfGt h)
     ifNeg h'
   (mod_eq a b).symm ▸ this
 
@@ -85,12 +85,12 @@ theorem mod_lt (x : Nat) {y : Nat} : y > 0 → x % y < y := by
   induction x, y using mod.inductionOn with
   | base x y h₁ =>
     intro h₂
-    have h₁ : ¬ 0 < y ∨ ¬ y ≤ x from Iff.mp (Decidable.notAndIffOrNot _ _) h₁
+    have h₁ : ¬ 0 < y ∨ ¬ y ≤ x := Iff.mp (Decidable.notAndIffOrNot _ _) h₁
     match h₁ with
     | Or.inl h₁ => exact absurd h₂ h₁
     | Or.inr h₁ =>
-      have hgt : y > x from gtOfNotLe h₁
-      have heq : x % y = x from mod_eq_of_lt hgt
+      have hgt : y > x := gtOfNotLe h₁
+      have heq : x % y = x := mod_eq_of_lt hgt
       rw [← heq] at hgt
       exact hgt
   | ind x y h h₂ =>
@@ -108,7 +108,7 @@ theorem mod_le (x y : Nat) : x % y ≤ x := by
 
 @[simp] theorem zero_mod (b : Nat) : 0 % b = 0 := by
   rw [mod_eq]
-  have ¬ (0 < b ∧ b ≤ 0) by
+  have : ¬ (0 < b ∧ b ≤ 0) := by
     intro ⟨h₁, h₂⟩
     exact absurd (Nat.ltOfLtOfLe h₁ h₂) (Nat.ltIrrefl 0)
   simp [this]
@@ -117,8 +117,8 @@ theorem mod_le (x y : Nat) : x % y ≤ x := by
   rw [mod_eq_sub_mod (Nat.leRefl _), Nat.sub_self, zero_mod]
 
 theorem mod_one (x : Nat) : x % 1 = 0 := by
-  have h : x % 1 < 1 from mod_lt x (by decide)
-  have (y : Nat) → y < 1 → y = 0 by
+  have h : x % 1 < 1 := mod_lt x (by decide)
+  have : (y : Nat) → y < 1 → y = 0 := by
     intro y
     cases y with
     | zero   => intro h; rfl
diff --git a/src/Init/Data/Stream.lean b/src/Init/Data/Stream.lean
index f277d7e0b3..f1e464871a 100644
--- a/src/Init/Data/Stream.lean
+++ b/src/Init/Data/Stream.lean
@@ -93,7 +93,7 @@ instance : Stream (List α) α where
 instance : Stream (Subarray α) α where
   next? s :=
     if h : s.start < s.stop then
-      have s.start + 1 ≤ s.stop from Nat.succLeOfLt h
+      have : s.start + 1 ≤ s.stop := Nat.succLeOfLt h
       some (s.as.get ⟨s.start, Nat.ltOfLtOfLe h s.h₂⟩, { s with start := s.start + 1, h₁ := this })
     else
       none
diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
index 931227bf99..827504d16c 100644
--- a/src/Init/Meta.lean
+++ b/src/Init/Meta.lean
@@ -792,7 +792,7 @@ private partial def filterSepElemsMAux {m : Type → Type} [Monad m] (a : Array
       if acc.isEmpty then
         filterSepElemsMAux a p (i+2) (acc.push stx)
       else if hz : i ≠ 0 then
-        have i.pred < i from Nat.predLt hz
+        have : i.pred < i := Nat.predLt hz
         let sepStx := a.get ⟨i.pred, Nat.ltTrans this h⟩
         filterSepElemsMAux a p (i+2) ((acc.push sepStx).push stx)
       else
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index d0180bc2be..d0e20b4561 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -108,7 +108,7 @@ inductive HEq {α : Sort u} (a : α) : {β : Sort u} → β → Prop where
   HEq.refl a
 
 theorem eqOfHEq {α : Sort u} {a a' : α} (h : HEq a a') : Eq a a' :=
-  have (α β : Sort u) → (a : α) → (b : β) → HEq a b → (h : Eq α β) → Eq (cast h a) b from
+  have : (α β : Sort u) → (a : α) → (b : β) → HEq a b → (h : Eq α β) → Eq (cast h a) b :=
     fun α β a b h₁ =>
       HEq.rec (motive := fun {β} (b : β) (h : HEq a b) => (h₂ : Eq α β) → Eq (cast h₂ a) b)
         (fun (h₂ : Eq α α) => rfl)
@@ -555,8 +555,8 @@ theorem Nat.eqOfBeqEqTrue : {n m : Nat} → Eq (beq n m) true → Eq n m
   | zero,   succ m, h => Bool.noConfusion h
   | succ n, zero,   h => Bool.noConfusion h
   | succ n, succ m, h =>
-    have Eq (beq n m) true from h
-    have Eq n m from eqOfBeqEqTrue this
+    have : Eq (beq n m) true := h
+    have : Eq n m := eqOfBeqEqTrue this
     this ▸ rfl
 
 theorem Nat.neOfBeqEqFalse : {n m : Nat} → Eq (beq n m) false → Not (Eq n m)
@@ -564,7 +564,7 @@ theorem Nat.neOfBeqEqFalse : {n m : Nat} → Eq (beq n m) false → Not (Eq n m)
   | zero,   succ m, h₁, h₂ => Nat.noConfusion h₂
   | succ n, zero,   h₁, h₂ => Nat.noConfusion h₂
   | succ n, succ m, h₁, h₂ =>
-    have Eq (beq n m) false from h₁
+    have : Eq (beq n m) false := h₁
     Nat.noConfusion h₂ (fun h₂ => absurd h₂ (neOfBeqEqFalse this))
 
 @[extern "lean_nat_dec_eq"]
@@ -625,8 +625,8 @@ theorem Nat.leStep : {n m : Nat} → LE.le n m → LE.le n (succ m)
   | zero,   succ n, h => rfl
   | succ n, zero,   h => Bool.noConfusion h
   | succ n, succ m, h =>
-    have LE.le n m from h
-    have LE.le n (succ m) from leStep this
+    have : LE.le n m := h
+    have : LE.le n (succ m) := leStep this
     succLeSucc this
 
 protected theorem Nat.leTrans : {n m k : Nat} → LE.le n m → LE.le m k → LE.le n k
@@ -634,8 +634,8 @@ protected theorem Nat.leTrans : {n m k : Nat} → LE.le n m → LE.le m k → LE
   | succ n, zero,   k,      h₁, h₂ => Bool.noConfusion h₁
   | succ n, succ m, zero,   h₁, h₂ => Bool.noConfusion h₂
   | succ n, succ m, succ k, h₁, h₂ =>
-    have h₁' : LE.le n m from h₁
-    have h₂' : LE.le m k from h₂
+    have h₁' : LE.le n m := h₁
+    have h₂' : LE.le m k := h₂
     show LE.le n k from
     Nat.leTrans h₁' h₂'
 
@@ -654,7 +654,7 @@ protected theorem Nat.eqOrLtOfLe : {n m: Nat} → LE.le n m → Or (Eq n m) (LT.
   | zero,   succ n, h => Or.inr (zeroLe n)
   | succ n, zero,   h => Bool.noConfusion h
   | succ n, succ m, h =>
-    have LE.le n m from h
+    have : LE.le n m := h
     match Nat.eqOrLtOfLe this with
     | Or.inl h => Or.inl (h ▸ rfl)
     | Or.inr h => Or.inr (succLeSucc h)
@@ -679,8 +679,8 @@ protected theorem Nat.leAntisymm : {n m : Nat} → LE.le n m → LE.le m n → E
   | succ n, zero,   h₁, h₂ => Bool.noConfusion h₁
   | zero,   succ m, h₁, h₂ => Bool.noConfusion h₂
   | succ n, succ m, h₁, h₂ =>
-    have h₁' : LE.le n m from h₁
-    have h₂' : LE.le m n from h₂
+    have h₁' : LE.le n m := h₁
+    have h₂' : LE.le m n := h₂
     (Nat.leAntisymm h₁' h₂') ▸ rfl
 
 protected theorem Nat.ltOfLeOfNe {n m : Nat} (h₁ : LE.le n m) (h₂ : Not (Eq n m)) : LT.lt n m :=
@@ -1038,7 +1038,7 @@ def List.get {α : Type u} : (as : List α) → (i : Nat) → LT.lt i as.length
   | nil,       i,          h => absurd h (Nat.notLtZero _)
   | cons a as, 0,          h => a
   | cons a as, Nat.succ i, h =>
-    have LT.lt i.succ as.length.succ from length_cons .. ▸ h
+    have : LT.lt i.succ as.length.succ := length_cons .. ▸ h
     get as i (Nat.leOfSuccLeSucc this)
 
 structure String where
diff --git a/src/Init/SimpLemmas.lean b/src/Init/SimpLemmas.lean
index ff3d0a7b71..721c41fdf5 100644
--- a/src/Init/SimpLemmas.lean
+++ b/src/Init/SimpLemmas.lean
@@ -35,16 +35,16 @@ theorem impCongr {p₁ p₂ : Sort u} {q₁ q₂ : Sort v} (h₁ : p₁ = p₂)
 theorem impCongrCtx {p₁ p₂ q₁ q₂ : Prop} (h₁ : p₁ = p₂) (h₂ : p₂ → q₁ = q₂) : (p₁ → q₁) = (p₂ → q₂) :=
   propext <| Iff.intro
     (fun h hp₂ =>
-      have p₁ from h₁ ▸ hp₂
-      have q₁ from h this
+      have : p₁ := h₁ ▸ hp₂
+      have : q₁ := h this
       h₂ hp₂ ▸ this)
     (fun h hp₁ =>
-      have hp₂ : p₂ from h₁ ▸ hp₁
-      have q₂ from h hp₂
+      have hp₂ : p₂ := h₁ ▸ hp₁
+      have : q₂ := h hp₂
       h₂ hp₂ ▸ this)
 
 theorem forallCongr {α : Sort u} {p q : α → Prop} (h : ∀ a, (p a = q a)) : (∀ a, p a) = (∀ a, q a) :=
-  have p = q from funext h
+  have : p = q := funext h
   this ▸ rfl
 
 @[congr]
diff --git a/src/Init/WF.lean b/src/Init/WF.lean
index cad2c26329..bc8300ffa5 100644
--- a/src/Init/WF.lean
+++ b/src/Init/WF.lean
@@ -155,7 +155,7 @@ def Nat.ltWf : WellFounded Nat.lt := by
   | succ n ih =>
     apply Acc.intro (Nat.succ n)
     intro m h
-    have m = n ∨ m < n from Nat.eqOrLtOfLe (Nat.leOfSuccLeSucc h)
+    have : m = n ∨ m < n := Nat.eqOrLtOfLe (Nat.leOfSuccLeSucc h)
     match this with
     | Or.inl e => subst e; assumption
     | Or.inr e => exact Acc.inv ih e
diff --git a/src/Lean/Data/Lsp/LanguageFeatures.lean b/src/Lean/Data/Lsp/LanguageFeatures.lean
index 9650660af0..d5c02a452d 100644
--- a/src/Lean/Data/Lsp/LanguageFeatures.lean
+++ b/src/Lean/Data/Lsp/LanguageFeatures.lean
@@ -166,7 +166,7 @@ partial instance : ToJson DocumentSymbol where
   toJson :=
     let rec go
       | DocumentSymbol.mk sym =>
-        have ToJson DocumentSymbol from ⟨go⟩
+        have : ToJson DocumentSymbol := ⟨go⟩
         toJson sym
     go
 
diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index c635b6df6c..498c3b3a33 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -75,7 +75,7 @@ open Meta
   | `(suffices $x:ident : $type from $val $[;]? $body)            => `(have $x : $type := $body; $val)
   | `(suffices $type:term from $val $[;]? $body)                  => `(have : $type := $body; $val)
   | `(suffices $x:ident : $type by%$b $tac:tacticSeq $[;]? $body) => `(have $x : $type := $body; by%$b $tac:tacticSeq)
-  | `(suffices $type:term by%$b $tac:tacticSeq $[;]? $body)       => `(have $type := $body; by%$b $tac:tacticSeq)
+  | `(suffices $type:term by%$b $tac:tacticSeq $[;]? $body)       => `(have : $type := $body; by%$b $tac:tacticSeq)
   | _                                                             => Macro.throwUnsupported
 
 open Lean.Parser in
diff --git a/src/Std/Data/HashMap.lean b/src/Std/Data/HashMap.lean
index eb3f573b23..5b4a852247 100644
--- a/src/Std/Data/HashMap.lean
+++ b/src/Std/Data/HashMap.lean
@@ -84,7 +84,7 @@ partial def moveEntries [Hashable α] (i : Nat) (source : Array (AssocList α β
 
 def expand [Hashable α] (size : Nat) (buckets : HashMapBucket α β) : HashMapImp α β :=
   let nbuckets := buckets.val.size * 2
-  have nbuckets > 0 from Nat.mulPos buckets.property (by decide)
+  have : nbuckets > 0 := Nat.mulPos buckets.property (by decide)
   let new_buckets : HashMapBucket α β := ⟨mkArray nbuckets AssocList.nil, by simp; assumption⟩
   { size    := size,
     buckets := moveEntries 0 buckets.val new_buckets }
diff --git a/src/Std/Data/HashSet.lean b/src/Std/Data/HashSet.lean
index 108b42576b..913fd4a9f2 100644
--- a/src/Std/Data/HashSet.lean
+++ b/src/Std/Data/HashSet.lean
@@ -71,7 +71,7 @@ partial def moveEntries [Hashable α] (i : Nat) (source : Array (List α)) (targ
 
 def expand [Hashable α] (size : Nat) (buckets : HashSetBucket α) : HashSetImp α :=
   let nbuckets := buckets.val.size * 2
-  have nbuckets > 0 from Nat.mulPos buckets.property (by decide)
+  have : nbuckets > 0 := Nat.mulPos buckets.property (by decide)
   let new_buckets : HashSetBucket α := ⟨mkArray nbuckets [], by rw [Array.size_mkArray]; assumption⟩
   { size    := size,
     buckets := moveEntries 0 buckets.val new_buckets }
diff --git a/src/Std/Data/PersistentHashMap.lean b/src/Std/Data/PersistentHashMap.lean
index e47c704c41..15a864b6ac 100644
--- a/src/Std/Data/PersistentHashMap.lean
+++ b/src/Std/Data/PersistentHashMap.lean
@@ -211,7 +211,7 @@ def isUnaryNode : Node α β → Option (α × β)
   | Node.entries entries         => isUnaryEntries entries 0 none
   | Node.collision keys vals heq =>
     if h : 1 = keys.size then
-      have 0 < keys.size by rw [←h]; decide
+      have : 0 < keys.size := by rw [←h]; decide
       some (keys.get ⟨0, this⟩, vals.get ⟨0, by rw [←heq]; assumption⟩)
     else
       none
@@ -222,7 +222,7 @@ partial def eraseAux [BEq α] : Node α β → USize → α → Node α β × Bo
     | some idx =>
       let ⟨keys', keq⟩ := keys.eraseIdx' idx
       let ⟨vals', veq⟩ := vals.eraseIdx' (Eq.ndrec idx heq)
-      have keys.size - 1 = vals.size - 1 by rw [heq]
+      have : keys.size - 1 = vals.size - 1 := by rw [heq]
       (Node.collision keys' vals' (keq.trans (this.trans veq.symm)), true)
     | none     => (n, false)
   | n@(Node.entries entries), h, k =>
diff --git a/tests/lean/Reformat.lean.expected.out b/tests/lean/Reformat.lean.expected.out
index 955bb90eb2..2472c0fb5b 100644
--- a/tests/lean/Reformat.lean.expected.out
+++ b/tests/lean/Reformat.lean.expected.out
@@ -132,7 +132,7 @@ def HEq.rfl {α : Sort u} {a : α} : HEq a a :=
   HEq.refl a 
 
 theorem eqOfHEq {α : Sort u} {a a' : α} (h : HEq a a') : Eq a a' :=
-  have (α β : Sort u) → (a : α) → (b : β) → HEq a b → (h : Eq α β) → Eq (cast h a) b from
+  have  : (α β : Sort u) → (a : α) → (b : β) → HEq a b → (h : Eq α β) → Eq (cast h a) b :=
     fun α β a b h₁ =>
       HEq.rec (motive := fun {β} (b : β) (h : HEq a b) => (h₂ : Eq α β) → Eq (cast h₂ a) b) (fun (h₂ : Eq α α) => rfl)
         h₁ 
diff --git a/tests/lean/Reformat/Input.lean b/tests/lean/Reformat/Input.lean
index fed9c10875..8a0b417966 100644
--- a/tests/lean/Reformat/Input.lean
+++ b/tests/lean/Reformat/Input.lean
@@ -111,7 +111,7 @@ inductive HEq {α : Sort u} (a : α) : {β : Sort u} → β → Prop
   HEq.refl a
 
 theorem eqOfHEq {α : Sort u} {a a' : α} (h : HEq a a') : Eq a a' :=
-  have (α β : Sort u) → (a : α) → (b : β) → HEq a b → (h : Eq α β) → Eq (cast h a) b from
+  have : (α β : Sort u) → (a : α) → (b : β) → HEq a b → (h : Eq α β) → Eq (cast h a) b :=
     fun α β a b h₁ =>
       HEq.rec (motive := fun {β} (b : β) (h : HEq a b) => (h₂ : Eq α β) → Eq (cast h₂ a) b)
         (fun (h₂ : Eq α α) => rfl)
diff --git a/tests/lean/StxQuot.lean b/tests/lean/StxQuot.lean
index a8aadadcd7..7f749fff83 100644
--- a/tests/lean/StxQuot.lean
+++ b/tests/lean/StxQuot.lean
@@ -107,9 +107,3 @@ syntax "foo" term : term
 #eval run ``(fun x => y)
 #eval run ``(fun x y => x y)
 #eval run ``(fun ⟨x, y⟩ => x)
-
-#eval run do
-  match ← `(have x := y; z) with
-  | `(have $[$x :]? $type from $val $[;]? $body)   => pure 0
-  | `(have $pattern:term := $val:term $[;]? $body) => pure 1
-  | _                                              => pure 2
diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out
index a303f4dbcc..16ede81946 100644
--- a/tests/lean/StxQuot.lean.expected.out
+++ b/tests/lean/StxQuot.lean.expected.out
@@ -54,4 +54,3 @@ StxQuot.lean:101:13-101:14: error: unknown identifier 'x' at quotation precheck;
 StxQuot.lean:107:22-107:23: error: unknown identifier 'y' at quotation precheck; you can use `set_option quotPrecheck false` to disable this check.
 "(Term.fun\n \"fun\"\n (Term.basicFun\n  [`x._@.UnhygienicMain._hyg.1 `y._@.UnhygienicMain._hyg.1]\n  \"=>\"\n  (Term.app `x._@.UnhygienicMain._hyg.1 [`y._@.UnhygienicMain._hyg.1])))"
 "(Term.fun\n \"fun\"\n (Term.basicFun\n  [(Term.anonymousCtor \"⟨\" [`x._@.UnhygienicMain._hyg.1 \",\" `y._@.UnhygienicMain._hyg.1] \"⟩\")]\n  \"=>\"\n  `x._@.UnhygienicMain._hyg.1))"
-"1"
diff --git a/tests/lean/have.lean b/tests/lean/have.lean
index fc8331080c..93a26e765e 100644
--- a/tests/lean/have.lean
+++ b/tests/lean/have.lean
@@ -1,5 +1,5 @@
 example : False :=
-  have False from _
+  have : False := _
 
 example : 5 = 3 :=
   have t : True := _
diff --git a/tests/lean/interactive/goalIssue.lean b/tests/lean/interactive/goalIssue.lean
index b46c559163..76554d1ad1 100644
--- a/tests/lean/interactive/goalIssue.lean
+++ b/tests/lean/interactive/goalIssue.lean
@@ -1,6 +1,6 @@
 theorem foo1 (x : Nat) : 0 + x = x := by
   first
-   | skip; have x + x = x + x from rfl; done
+   | skip; have : x + x = x + x := rfl; done
           --^ $/lean/plainGoal
    | simp
 
diff --git a/tests/lean/interactive/haveInfo.lean b/tests/lean/interactive/haveInfo.lean
index 8b55c3af90..9f83f27bc0 100644
--- a/tests/lean/interactive/haveInfo.lean
+++ b/tests/lean/interactive/haveInfo.lean
@@ -1,26 +1,26 @@
 example : False := by
-  have True by
+  have : True := by
     skip
   --^ $/lean/plainGoal
     skip
   admit
 
 example : False := by
-  have True by
-          --^ $/lean/plainGoal
+  have : True := by
+               --^ $/lean/plainGoal
     skip
     skip
   admit
 
 example : False := by
-  have True by
-           --^ $/lean/plainGoal
+  have : True := by
+               --^ $/lean/plainGoal
     skip
     skip
   admit
 
 example : False := by
-  have True by
+  have : True := by
     skip
 --^ $/lean/plainGoal
     skip
diff --git a/tests/lean/interactive/haveInfo.lean.expected.out b/tests/lean/interactive/haveInfo.lean.expected.out
index 5f5930b8b6..8b7b863789 100644
--- a/tests/lean/interactive/haveInfo.lean.expected.out
+++ b/tests/lean/interactive/haveInfo.lean.expected.out
@@ -2,10 +2,10 @@
  "position": {"line": 2, "character": 4}}
 {"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]}
 {"textDocument": {"uri": "file://haveInfo.lean"},
- "position": {"line": 8, "character": 12}}
+ "position": {"line": 8, "character": 17}}
 {"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]}
 {"textDocument": {"uri": "file://haveInfo.lean"},
- "position": {"line": 15, "character": 13}}
+ "position": {"line": 15, "character": 17}}
 {"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]}
 {"textDocument": {"uri": "file://haveInfo.lean"},
  "position": {"line": 23, "character": 2}}
diff --git a/tests/lean/interactive/macroGoalIssue.lean b/tests/lean/interactive/macroGoalIssue.lean
index 32b685742a..5371388aeb 100644
--- a/tests/lean/interactive/macroGoalIssue.lean
+++ b/tests/lean/interactive/macroGoalIssue.lean
@@ -1,5 +1,5 @@
 theorem ex (n : Nat) : True := by
-  have n = 0 + n by rw [Nat.zero_add]
+  have : n = 0 + n := by rw [Nat.zero_add]
   skip
 --^ $/lean/plainGoal
   exact True.intro
diff --git a/tests/lean/precissues.lean b/tests/lean/precissues.lean
index 790122133f..078cde7447 100644
--- a/tests/lean/precissues.lean
+++ b/tests/lean/precissues.lean
@@ -12,15 +12,15 @@ def f (x : Nat) (g : Nat → Nat) := g x
 
 #check f 1 (fun x => x)
 
-#check id have True from ⟨⟩; this -- should fail
+#check id have : True := ⟨⟩; this -- should fail
 
 #check id let x := 10; x
 
 #check 1
 
-#check id (have True from ⟨⟩; this)
+#check id (have : True := ⟨⟩; this)
 
-#check 0 = have Nat from 1; this
+#check 0 = have : Nat := 1; this
 #check 0 = let x := 0; x
 
 variable (p q r : Prop)
diff --git a/tests/lean/revertlet.lean b/tests/lean/revertlet.lean
index 345c9f8d43..882e9a3e67 100644
--- a/tests/lean/revertlet.lean
+++ b/tests/lean/revertlet.lean
@@ -1,7 +1,7 @@
 theorem ex (n : Nat) (h : n = 0) : 0 + n = 0 := by
   let m := n + 1
   let v := m + 1
-  have v = n + 2 from rfl
+  have : v = n + 2 := rfl
   traceState
   subst h
   traceState
diff --git a/tests/lean/run/500_lean3.lean b/tests/lean/run/500_lean3.lean
index 6e469ac78f..893baa58d6 100644
--- a/tests/lean/run/500_lean3.lean
+++ b/tests/lean/run/500_lean3.lean
@@ -1,4 +1,4 @@
 example (foo bar : OptionM Nat) : False := by
-  have do { let x ← bar; foo } = bar >>= fun x => foo from rfl
+  have : do { let x ← bar; foo } = bar >>= fun x => foo := rfl
   admit
   done
diff --git a/tests/lean/run/alg.lean b/tests/lean/run/alg.lean
index 1ef85d2f37..477e1d267c 100644
--- a/tests/lean/run/alg.lean
+++ b/tests/lean/run/alg.lean
@@ -64,7 +64,7 @@ theorem inv_inv [Group α] (a : α) : (a⁻¹)⁻¹ = a :=
   inv_eq_of_mul_eq_one (mul_left_inv a)
 
 theorem mul_right_inv [Group α] (a : α) : a * a⁻¹ = 1 := by
-  have a⁻¹⁻¹ * a⁻¹ = 1 by rw [mul_left_inv]
+  have : a⁻¹⁻¹ * a⁻¹ = 1 := by rw [mul_left_inv]
   rw [inv_inv] at this
   assumption
 
diff --git a/tests/lean/run/balg.lean b/tests/lean/run/balg.lean
index 5222c35eb3..03913e650e 100644
--- a/tests/lean/run/balg.lean
+++ b/tests/lean/run/balg.lean
@@ -81,7 +81,7 @@ theorem inv_inv {G : Group} (a : G) : (a⁻¹)⁻¹ = a :=
   inv_eq_of_mul_eq_one (G.mul_left_inv a)
 
 theorem mul_right_inv {G : Group} (a : G) : a * a⁻¹ = 1 := by
-  have a⁻¹⁻¹ * a⁻¹ = 1 by rw [G.mul_left_inv]; rfl
+  have : a⁻¹⁻¹ * a⁻¹ = 1 := by rw [G.mul_left_inv]; rfl
   rw [inv_inv] at this
   assumption
 
diff --git a/tests/lean/run/concatElim.lean b/tests/lean/run/concatElim.lean
index 49ec834558..1ed372e5a3 100644
--- a/tests/lean/run/concatElim.lean
+++ b/tests/lean/run/concatElim.lean
@@ -38,8 +38,8 @@ theorem dropLastLen {α} (xs : List α) : (n : Nat) → xs.length = n+1 → (dro
   | []    => intros; contradiction
   | [a]   =>
     intro n h
-    have 1 = n + 1 from h
-    have 0 = n by injection this; assumption
+    have : 1 = n + 1 := h
+    have : 0 = n := by injection this; assumption
     subst this
     rfl
   | x₁::x₂::xs =>
@@ -49,8 +49,8 @@ theorem dropLastLen {α} (xs : List α) : (n : Nat) → xs.length = n+1 → (dro
       simp [lengthCons] at h
       injection h
     | succ n =>
-      have (x₁ :: x₂ :: xs).length = xs.length + 2 by simp [lengthCons]
-      have xs.length = n by rw [this] at h; injection h with h; injection h with h; assumption
+      have : (x₁ :: x₂ :: xs).length = xs.length + 2 := by simp [lengthCons]
+      have : xs.length = n := by rw [this] at h; injection h with h; injection h with h; assumption
       simp [dropLast, lengthCons, dropLastLen (x₂::xs) xs.length (lengthCons ..), this]
 
 @[inline]
@@ -66,7 +66,7 @@ def concatElim {α}
       subst aux
       apply base ()
     | n+1, xs, h => by
-      have notNil : xs ≠ [] by intro h1; subst h1; injection h
+      have notNil : xs ≠ [] := by intro h1; subst h1; injection h
       let ih  := aux n (dropLast xs) (dropLastLen _ _ h)
       let aux := ind (dropLast xs) (last xs notNil) ih
       rw [concatEq] at aux
diff --git a/tests/lean/run/decClassical.lean b/tests/lean/run/decClassical.lean
index 821ad9caaa..ed2d59fd99 100644
--- a/tests/lean/run/decClassical.lean
+++ b/tests/lean/run/decClassical.lean
@@ -1,9 +1,9 @@
 open Classical
 
 theorem ex : if (fun x => x + 1) = (fun x => x + 2) then False else True := by
-  have (fun x => x + 1) ≠ (fun x => x + 2) by
+  have : (fun x => x + 1) ≠ (fun x => x + 2) := by
     intro h
-    have 1 = 2 from congrFun h 0
+    have : 1 = 2 := congrFun h 0
     contradiction
   rw [ifNeg this]
   exact True.intro
diff --git a/tests/lean/run/def7.lean b/tests/lean/run/def7.lean
index 5d3cea28cd..719bb856c3 100644
--- a/tests/lean/run/def7.lean
+++ b/tests/lean/run/def7.lean
@@ -37,8 +37,8 @@ theorem L.appendNil {α} : (as : L α) → append as nil = as
 | nil       => rfl
 | cons a as =>
   show cons a (fun _ => append (as ()) nil) = cons a as from
-  have ih : append (as ()) nil = as () from appendNil $ as ()
-  have thunkAux : (fun _ => as ()) = as from funext fun x => by
+  have ih : append (as ()) nil = as () := appendNil $ as ()
+  have thunkAux : (fun _ => as ()) = as := funext fun x => by
     cases x
     exact rfl
   by rw [ih, thunkAux]
diff --git a/tests/lean/run/doNotation3.lean b/tests/lean/run/doNotation3.lean
index bc6bfb5a74..d19e3095ec 100644
--- a/tests/lean/run/doNotation3.lean
+++ b/tests/lean/run/doNotation3.lean
@@ -1,16 +1,16 @@
 theorem zeroLtOfLt : {a b : Nat} → a < b → 0 < b
 | 0,   _, h => h
 | a+1, b, h =>
-  have a < b from Nat.ltTrans (Nat.ltSuccSelf _) h
+  have : a < b := Nat.ltTrans (Nat.ltSuccSelf _) h
   zeroLtOfLt this
 
 def fold {m α β} [Monad m] (as : Array α) (b : β) (f : α → β → m β) : m β := do
 let rec loop : (i : Nat) → i ≤ as.size → β → m β
   | 0,   h, b => b
   | i+1, h, b => do
-    have h' : i < as.size          from Nat.ltOfLtOfLe (Nat.ltSuccSelf i) h
-    have as.size - 1 < as.size     from Nat.subLt (zeroLtOfLt h') (by decide)
-    have as.size - 1 - i < as.size from Nat.ltOfLeOfLt (Nat.subLe (as.size - 1) i) this
+    have h' : i < as.size          := Nat.ltOfLtOfLe (Nat.ltSuccSelf i) h
+    have : as.size - 1 < as.size     := Nat.subLt (zeroLtOfLt h') (by decide)
+    have : as.size - 1 - i < as.size := Nat.ltOfLeOfLt (Nat.subLe (as.size - 1) i) this
     let b ← f (as.get ⟨as.size - 1 - i, this⟩) b
     loop i (Nat.leOfLt h') b
 loop as.size (Nat.leRefl _) b
@@ -25,9 +25,9 @@ let rec loop (i : Nat) (h : i ≤ as.size) (b : β) : m β := do
   match i, h with
   | 0,   h => return b
   | i+1, h =>
-    have h' : i < as.size          from Nat.ltOfLtOfLe (Nat.ltSuccSelf i) h
-    have as.size - 1 < as.size     from Nat.subLt (zeroLtOfLt h') (by decide)
-    have as.size - 1 - i < as.size from Nat.ltOfLeOfLt (Nat.subLe (as.size - 1) i) this
+    have h' : i < as.size          := Nat.ltOfLtOfLe (Nat.ltSuccSelf i) h
+    have : as.size - 1 < as.size     := Nat.subLt (zeroLtOfLt h') (by decide)
+    have : as.size - 1 - i < as.size := Nat.ltOfLeOfLt (Nat.subLe (as.size - 1) i) this
     let b ← f (as.get ⟨as.size - 1 - i, this⟩) b
     loop i (Nat.leOfLt h') b
 loop as.size (Nat.leRefl _) b
diff --git a/tests/lean/run/do_eqv.lean b/tests/lean/run/do_eqv.lean
index 8d294de41b..9c3519386e 100644
--- a/tests/lean/run/do_eqv.lean
+++ b/tests/lean/run/do_eqv.lean
@@ -1,5 +1,5 @@
 theorem byCases_Bool_bind [Monad m] (x : m Bool) (f g : Bool → m β) (isTrue : f true = g true) (isFalse : f false = g false) : (x >>= f) = (x >>= g) := by
-  have f = g by
+  have : f = g := by
     funext b; cases b <;> assumption
   rw [this]
 
diff --git a/tests/lean/run/impLambdaTac.lean b/tests/lean/run/impLambdaTac.lean
index 721dcec937..aaced11641 100644
--- a/tests/lean/run/impLambdaTac.lean
+++ b/tests/lean/run/impLambdaTac.lean
@@ -19,13 +19,13 @@ example (P : Prop) : ∀ {p : P}, P := by
   apply id
 
 example (P : Prop) : ∀ p : P, P := by
-  have _ from 1
+  have : _ := 1
   apply id
 
 example (P : Prop) : ∀ {p : P}, P := by
-  refine noImplicitLambda% (have _ from 1; ?_)
+  refine noImplicitLambda% (have : _ := 1; ?_)
   apply id
 
 example (P : Prop) : ∀ {p : P}, P := by
-  have _ from 1
+  have : _ := 1
   apply id
diff --git a/tests/lean/run/inj1.lean b/tests/lean/run/inj1.lean
index 91ebec82a9..413063df6a 100644
--- a/tests/lean/run/inj1.lean
+++ b/tests/lean/run/inj1.lean
@@ -13,7 +13,7 @@ by {
 }
 
 theorem test3 {α} (a b : α) (as bs : List α) (h : (x : List α) → (y : List α) → x = y) : as = bs :=
-have a::as = b::bs from h (a::as) (b::bs);
+have : a::as = b::bs := h (a::as) (b::bs);
 by {
   injection this with h1 h2;
   exact h2
diff --git a/tests/lean/run/lean3_zulip_issues_1.lean b/tests/lean/run/lean3_zulip_issues_1.lean
index 422a068b5c..497f9030bc 100644
--- a/tests/lean/run/lean3_zulip_issues_1.lean
+++ b/tests/lean/run/lean3_zulip_issues_1.lean
@@ -29,11 +29,11 @@ def f : wrap → Nat
   | _ => 1
 
 example (a : Nat) : True := by
-  have ∀ n, n ≥ 0 → a ≤ a from fun _ _ => Nat.leRefl ..
+  have : ∀ n, n ≥ 0 → a ≤ a := fun _ _ => Nat.leRefl ..
   exact True.intro
 
 example (ᾰ : Nat) : True := by
-  have ∀ n, n ≥ 0 → ᾰ ≤ ᾰ from fun _ _ => Nat.leRefl ..
+  have : ∀ n, n ≥ 0 → ᾰ ≤ ᾰ := fun _ _ => Nat.leRefl ..
   exact True.intro
 
 inductive Vec.{u} (α : Type u) : Nat → Type u
diff --git a/tests/lean/run/letrecInProofs.lean b/tests/lean/run/letrecInProofs.lean
index 73e7457fbb..853b9f821a 100644
--- a/tests/lean/run/letrecInProofs.lean
+++ b/tests/lean/run/letrecInProofs.lean
@@ -16,12 +16,12 @@ theorem Tree.acyclic (x t : Tree) : x = t → x ≮ t := by
       apply And.intro _ trivial
       intro h; injection h
     | node l r, h =>
-      have ihl : x ≮ l → node s x ≠ l ∧ node s x ≮ l from right x s l
-      have ihr : x ≮ r → node s x ≠ r ∧ node s x ≮ r from right x s r
-      have hl : x ≠ l ∧ x ≮ l from h.1
-      have hr : x ≠ r ∧ x ≮ r from h.2.1
-      have ihl : node s x ≠ l ∧ node s x ≮ l from ihl hl.2
-      have ihr : node s x ≠ r ∧ node s x ≮ r from ihr hr.2
+      have ihl : x ≮ l → node s x ≠ l ∧ node s x ≮ l := right x s l
+      have ihr : x ≮ r → node s x ≠ r ∧ node s x ≮ r := right x s r
+      have hl : x ≠ l ∧ x ≮ l := h.1
+      have hr : x ≠ r ∧ x ≮ r := h.2.1
+      have ihl : node s x ≠ l ∧ node s x ≮ l := ihl hl.2
+      have ihr : node s x ≠ r ∧ node s x ≮ r := ihr hr.2
       apply And.intro
       focus
         intro h
@@ -39,12 +39,12 @@ theorem Tree.acyclic (x t : Tree) : x = t → x ≮ t := by
       apply And.intro _ trivial
       intro h; injection h
     | node l r, h =>
-      have ihl : x ≮ l → node x t ≠ l ∧ node x t ≮ l from left x t l
-      have ihr : x ≮ r → node x t ≠ r ∧ node x t ≮ r from left x t r
-      have hl : x ≠ l ∧ x ≮ l from h.1
-      have hr : x ≠ r ∧ x ≮ r from h.2.1
-      have ihl : node x t ≠ l ∧ node x t ≮ l from ihl hl.2
-      have ihr : node x t ≠ r ∧ node x t ≮ r from ihr hr.2
+      have ihl : x ≮ l → node x t ≠ l ∧ node x t ≮ l := left x t l
+      have ihr : x ≮ r → node x t ≠ r ∧ node x t ≮ r := left x t r
+      have hl : x ≠ l ∧ x ≮ l := h.1
+      have hr : x ≠ r ∧ x ≮ r := h.2.1
+      have ihl : node x t ≠ l ∧ node x t ≮ l := ihl hl.2
+      have ihr : node x t ≠ r ∧ node x t ≮ r := ihr hr.2
       apply And.intro
       focus
         intro h
@@ -59,8 +59,8 @@ theorem Tree.acyclic (x t : Tree) : x = t → x ≮ t := by
   let rec aux : (x : Tree) → x ≮ x
     | leaf     => trivial
     | node l r => by
-        have ih₁ : l ≮ l from aux l
-        have ih₂ : r ≮ r from aux r
+        have ih₁ : l ≮ l := aux l
+        have ih₂ : r ≮ r := aux r
         show (node l r ≠ l ∧ node l r ≮ l) ∧ (node l r ≠ r ∧ node l r ≮ r) ∧ True
         apply And.intro
         focus
diff --git a/tests/lean/run/matrix.lean b/tests/lean/run/matrix.lean
index e2d6882949..325ffc9467 100644
--- a/tests/lean/run/matrix.lean
+++ b/tests/lean/run/matrix.lean
@@ -39,7 +39,7 @@ where
     match i, h with
     | 0, h   => acc
     | i+1, h =>
-      have i < m from Nat.ltOfLtOfLe (Nat.ltSuccSelf _) h
+      have : i < m := Nat.ltOfLtOfLe (Nat.ltSuccSelf _) h
       loop i (Nat.leOfLt this) (acc + u ⟨i, this⟩ * v ⟨i, this⟩)
 
 instance [Zero α] : Zero (Matrix m n α) where
diff --git a/tests/lean/run/nativeReflBackdoor.lean b/tests/lean/run/nativeReflBackdoor.lean
index fecd31ee5a..65f7cfd7e7 100644
--- a/tests/lean/run/nativeReflBackdoor.lean
+++ b/tests/lean/run/nativeReflBackdoor.lean
@@ -20,13 +20,13 @@ match b with
 | true  =>
   /- The following `nativeDecide` is going to use `g` to evaluate `f`
      because of the `implementedBy` directive. -/
-  have (f true) = false by nativeDecide
+  have : (f true) = false := by nativeDecide
   this
 | false => rfl
 
 theorem trueEqFalse : true = false :=
-have h₁ : f true = true  from rfl;
-have h₂ : f true = false from fConst true;
+have h₁ : f true = true  := rfl;
+have h₂ : f true = false := fConst true;
 Eq.trans h₁.symm h₂
 
 /-
diff --git a/tests/lean/run/newfrontend1.lean b/tests/lean/run/newfrontend1.lean
index 2246eb2829..f1d7064b33 100644
--- a/tests/lean/run/newfrontend1.lean
+++ b/tests/lean/run/newfrontend1.lean
@@ -379,7 +379,7 @@ by intros h1 h2 h3;
 
 theorem simple21 (x y z : Nat) : y = z → x = x → y = x → x = z :=
 fun h1 _ h3 =>
-  have x = y from by { apply Eq.symm; assumption };
+  have : x = y := by { apply Eq.symm; assumption };
   Eq.trans this (by assumption)
 
 theorem simple22 (x y z : Nat) : y = z → y = x → id (x = z + 0) :=
@@ -391,12 +391,12 @@ fun h1 h2 => show x = z + 0 by
 
 theorem simple23 (x y z : Nat) : y = z → x = x → y = x → x = z :=
 fun h1 _ h3 =>
-  have x = y by apply Eq.symm; assumption
+  have : x = y := by apply Eq.symm; assumption
   Eq.trans this (by assumption)
 
 theorem simple24 (x y z : Nat) : y = z → x = x → y = x → x = z :=
 fun h1 _ h3 =>
-  have h : x = y by apply Eq.symm; assumption
+  have h : x = y := by apply Eq.symm; assumption
   Eq.trans h (by assumption)
 
 def f1 (x : Nat) : Nat :=
diff --git a/tests/lean/run/openInScopeBug.lean b/tests/lean/run/openInScopeBug.lean
index 52f4fc5f73..fe8fc4f663 100644
--- a/tests/lean/run/openInScopeBug.lean
+++ b/tests/lean/run/openInScopeBug.lean
@@ -13,8 +13,8 @@ theorem ex1 : f (g (g (g x))) = x := by
   simp [Foo.ax1, Foo.ax2]
 
 theorem ex2 : f (g (g (g x))) = x :=
-  have h₁ : f (g (g (g x))) = f (g x) by simp; /- try again with `Foo` scoped lemmas -/ open Foo in simp
-  have h₂ : f (g x) = x               by simp; open Foo in simp
+  have h₁ : f (g (g (g x))) = f (g x) := by simp; /- try again with `Foo` scoped lemmas -/ open Foo in simp
+  have h₂ : f (g x) = x               := by simp; open Foo in simp
   Eq.trans h₁ h₂
   -- open Foo in simp -- works
 
diff --git a/tests/lean/run/tactic1.lean b/tests/lean/run/tactic1.lean
index 824b8717e0..48bb5c9903 100644
--- a/tests/lean/run/tactic1.lean
+++ b/tests/lean/run/tactic1.lean
@@ -12,7 +12,7 @@ by {
 
 theorem ex3 (x y z : Nat) (h₁ : x = y) (h₂ : z = y) : x = z :=
 by {
-  have y = z from h₂.symm;
+  have : y = z := h₂.symm;
   apply Eq.trans;
   exact h₁;
   assumption
@@ -44,14 +44,14 @@ by {
 }
 
 theorem ex7 (x y z : Nat) (h₁ : x = y) (h₂ : z = y) : x = z := by
-have y = z by apply Eq.symm; assumption
+have : y = z := by apply Eq.symm; assumption
 apply Eq.trans
 exact h₁
 assumption
 
 theorem ex8 (x y z : Nat) (h₁ : x = y) (h₂ : z = y) : x = z :=
 by apply Eq.trans h₁;
-   have y = z by
+   have : y = z := by
      apply Eq.symm;
      assumption;
    exact this
diff --git a/tests/lean/substlet.lean b/tests/lean/substlet.lean
index 53bf8c374c..3a90761d2d 100644
--- a/tests/lean/substlet.lean
+++ b/tests/lean/substlet.lean
@@ -21,6 +21,6 @@ theorem ex2 (n : Nat) : 0 + n = n := by
 theorem ex3 (n : Nat) (h : n = 0) : 0 + n = 0 := by
   let m := n + 1
   let v := m + 1
-  have v = n + 2 from rfl
+  have : v = n + 2 := rfl
   subst v -- error
   done
diff --git a/tests/lean/tacUnsolvedGoalsErrors.lean b/tests/lean/tacUnsolvedGoalsErrors.lean
index 0cf3de51af..f8c79e2ebe 100644
--- a/tests/lean/tacUnsolvedGoalsErrors.lean
+++ b/tests/lean/tacUnsolvedGoalsErrors.lean
@@ -1,11 +1,11 @@
 theorem ex1 (p q r : Prop) (h1 : p ∨ q) (h2 : p → q) : q :=
-  have q by -- Error here
+  have : q := by -- Error here
     skip
   by skip -- Error here
      skip
 
 theorem ex2 (p q r : Prop) (h1 : p ∨ q) (h2 : p → q) : q :=
-  have q by {
+  have : q := by {
     skip
   } -- Error here
   by skip -- Error here
diff --git a/tests/lean/tacUnsolvedGoalsErrors.lean.expected.out b/tests/lean/tacUnsolvedGoalsErrors.lean.expected.out
index 2209f54334..4d95c7d3e0 100644
--- a/tests/lean/tacUnsolvedGoalsErrors.lean.expected.out
+++ b/tests/lean/tacUnsolvedGoalsErrors.lean.expected.out
@@ -1,4 +1,4 @@
-tacUnsolvedGoalsErrors.lean:2:9-3:8: error: unsolved goals
+tacUnsolvedGoalsErrors.lean:2:14-3:8: error: unsolved goals
 p q r : Prop
 h1 : p ∨ q
 h2 : p → q
diff --git a/tests/lean/unknownTactic.lean b/tests/lean/unknownTactic.lean
index 0fdd4d3be3..01ad345ecc 100644
--- a/tests/lean/unknownTactic.lean
+++ b/tests/lean/unknownTactic.lean
@@ -5,11 +5,11 @@ theorem ex1 (x : Nat) : x = x → x = x := by
 #print "---"
 
 theorem ex2 (x : Nat) : x = x → x = x :=
-  have x = x by foo
+  have : x = x := by foo
   fun h => h
 
 #print "---"
 
 theorem ex3 (x : Nat) : x = x → x = x :=
-  have x = x by foo (aaa bbb)
+  have : x = x := by foo (aaa bbb)
   fun h => h
diff --git a/tests/lean/unknownTactic.lean.expected.out b/tests/lean/unknownTactic.lean.expected.out
index 243577c98e..a80599a311 100644
--- a/tests/lean/unknownTactic.lean.expected.out
+++ b/tests/lean/unknownTactic.lean.expected.out
@@ -4,12 +4,12 @@ x : Nat
 a✝ : x = x
 ⊢ x = x
 ---
-unknownTactic.lean:8:17: error: unknown tactic
-unknownTactic.lean:8:13-8:19: error: unsolved goals
+unknownTactic.lean:8:22: error: unknown tactic
+unknownTactic.lean:8:18-8:24: error: unsolved goals
 x : Nat
 ⊢ x = x
 ---
-unknownTactic.lean:14:17: error: unknown tactic
-unknownTactic.lean:14:13-14:19: error: unsolved goals
+unknownTactic.lean:14:22: error: unknown tactic
+unknownTactic.lean:14:18-14:24: error: unsolved goals
 x : Nat
 ⊢ x = x