diff --git a/src/Lean/Data/Json/Basic.lean b/src/Lean/Data/Json/Basic.lean
index 7a304cfdfe..0be8058f96 100644
--- a/src/Lean/Data/Json/Basic.lean
+++ b/src/Lean/Data/Json/Basic.lean
@@ -5,6 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Marc Huisinga
 -/
 import Std.Data.RBTree
+namespace Std end Std -- Hack for old frontend
+
 namespace Lean
 
 -- mantissa * 10^-exponent
diff --git a/src/Lean/Level.lean b/src/Lean/Level.lean
index 39739e5fac..069509d102 100644
--- a/src/Lean/Level.lean
+++ b/src/Lean/Level.lean
@@ -10,6 +10,8 @@ import Std.Data.PersistentHashSet
 import Lean.Data.Name
 import Lean.Data.Format
 
+namespace Std end Std -- Hack for old frontend
+
 def Nat.imax (n m : Nat) : Nat :=
 if m = 0 then 0 else Nat.max n m
 
diff --git a/src/Std/Data/HashSet.lean b/src/Std/Data/HashSet.lean
index 0186c596f9..9a7fce4030 100644
--- a/src/Std/Data/HashSet.lean
+++ b/src/Std/Data/HashSet.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -18,16 +19,16 @@ structure HashSetImp (α : Type u) :=
 (buckets    : HashSetBucket α)
 
 def mkHashSetImp {α : Type u} (nbuckets := 8) : HashSetImp α :=
-let n := if nbuckets = 0 then 8 else nbuckets;
+let n := if nbuckets = 0 then 8 else nbuckets
 { size       := 0,
   buckets    :=
   ⟨ mkArray n [],
-    have p₁ : (mkArray n ([] : List α)).size = n from Array.szMkArrayEq _ _;
-    have p₂ : n = (if nbuckets = 0 then 8 else nbuckets) from rfl;
+    have p₁ : (mkArray n ([] : List α)).size = n from Array.szMkArrayEq _ _
+    have p₂ : n = (if nbuckets = 0 then 8 else nbuckets) from rfl
     have p₃ : (if nbuckets = 0 then 8 else nbuckets) > 0 from
       match nbuckets with
       | 0            => Nat.zeroLtSucc _
-      | (Nat.succ x) => Nat.zeroLtSucc _;
+      | (Nat.succ x) => Nat.zeroLtSucc _
     transRelRight Greater (Eq.trans p₁ p₂) p₃ ⟩ }
 
 namespace HashSetImp
@@ -37,7 +38,7 @@ def mkIdx {n : Nat} (h : n > 0) (u : USize) : { u : USize // u.toNat < n } :=
 ⟨u %ₙ n, USize.modnLt _ h⟩
 
 @[inline] def reinsertAux (hashFn : α → USize) (data : HashSetBucket α) (a : α) : HashSetBucket α :=
-let ⟨i, h⟩ := mkIdx data.property (hashFn a);
+let ⟨i, h⟩ := mkIdx data.property (hashFn a)
 data.update i (a :: data.val.uget i h) h
 
 @[inline] def foldBucketsM {δ : Type w} {m : Type w → Type w} [Monad m] (data : HashSetBucket α) (d : δ) (f : δ → α → m δ) : m δ :=
@@ -55,45 +56,46 @@ foldBuckets m.buckets d f
 def find? [HasBeq α] [Hashable α] (m : HashSetImp α) (a : α) : Option α :=
 match m with
 | ⟨_, buckets⟩ =>
-  let ⟨i, h⟩ := mkIdx buckets.property (hash a);
+  let ⟨i, h⟩ := mkIdx buckets.property (hash a)
   (buckets.val.uget i h).find? (fun a' => a == a')
 
 def contains [HasBeq α] [Hashable α] (m : HashSetImp α) (a : α) : Bool :=
 match m with
 | ⟨_, buckets⟩ =>
-  let ⟨i, h⟩ := mkIdx buckets.property (hash a);
+  let ⟨i, h⟩ := mkIdx buckets.property (hash a)
   (buckets.val.uget i h).contains a
 
 -- TODO: remove `partial` by using well-founded recursion
 partial def moveEntries [Hashable α] : Nat → Array (List α) → HashSetBucket α → HashSetBucket α
 | i, source, target =>
   if h : i < source.size then
-     let idx : Fin source.size := ⟨i, h⟩;
-     let es  : List α   := source.get idx;
+     let idx : Fin source.size := ⟨i, h⟩
+     let es  : List α   := source.get idx
      -- We remove `es` from `source` to make sure we can reuse its memory cells when performing es.foldl
-     let source                := source.set idx [];
-     let target                := es.foldl (reinsertAux hash) target;
+     let source                := source.set idx []
+     let target                := es.foldl (reinsertAux hash) target
      moveEntries (i+1) source target
   else target
 
 def expand [Hashable α] (size : Nat) (buckets : HashSetBucket α) : HashSetImp α :=
-let nbuckets := buckets.val.size * 2;
-have aux₁  : nbuckets > 0 from Nat.mulPos buckets.property (Nat.zeroLtBit0 Nat.oneNeZero);
-have aux₂  : (mkArray nbuckets ([] : List α)).size = nbuckets from Array.szMkArrayEq _ _;
-let new_buckets : HashSetBucket α := ⟨mkArray nbuckets [], aux₂.symm ▸ aux₁⟩;
+let nbuckets := buckets.val.size * 2
+have nbuckets > 0 from Nat.mulPos buckets.property (Nat.zeroLtBit0 Nat.oneNeZero)
+have (mkArray nbuckets ([] : List α)).size = nbuckets from Array.szMkArrayEq _ _
+have Array.size (mkArray nbuckets List.nil) > 0 by rw this; assumption
+let new_buckets : HashSetBucket α := ⟨mkArray nbuckets [], this⟩;
 { size    := size,
   buckets := moveEntries 0 buckets.val new_buckets }
 
 def insert [HasBeq α] [Hashable α] (m : HashSetImp α) (a : α) : HashSetImp α :=
 match m with
 | ⟨size, buckets⟩ =>
-  let ⟨i, h⟩ := mkIdx buckets.property (hash a);
-  let bkt    := buckets.val.uget i h;
+  let ⟨i, h⟩ := mkIdx buckets.property (hash a)
+  let bkt    := buckets.val.uget i h
   if bkt.contains a
   then ⟨size, buckets.update i (bkt.replace a a) h⟩
   else
-    let size'    := size + 1;
-    let buckets' := buckets.update i (a :: bkt) h;
+    let size'    := size + 1
+    let buckets' := buckets.update i (a :: bkt) h
     if size' ≤ buckets.val.size
     then { size := size', buckets := buckets' }
     else expand size' buckets'
@@ -101,8 +103,8 @@ match m with
 def erase [HasBeq α] [Hashable α] (m : HashSetImp α) (a : α) : HashSetImp α :=
 match m with
 | ⟨ size, buckets ⟩ =>
-  let ⟨i, h⟩ := mkIdx buckets.property (hash a);
-  let bkt    := buckets.val.uget i h;
+  let ⟨i, h⟩ := mkIdx buckets.property (hash a)
+  let bkt    := buckets.val.uget i h
   if bkt.contains a then ⟨size - 1, buckets.update i (bkt.erase a) h⟩
   else m
 
diff --git a/src/Std/Data/PersistentHashMap.lean b/src/Std/Data/PersistentHashMap.lean
index 1ff2a2468e..26dcb20586 100644
--- a/src/Std/Data/PersistentHashMap.lean
+++ b/src/Std/Data/PersistentHashMap.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -9,15 +10,15 @@ universes u v w w'
 namespace PersistentHashMap
 
 inductive Entry (α : Type u) (β : Type v) (σ : Type w)
-| entry (key : α) (val : β) : Entry
-| ref   (node : σ) : Entry
-| null  : Entry
+| entry (key : α) (val : β) : Entry α β σ
+| ref   (node : σ) : Entry α β σ
+| null  : Entry α β σ
 
 instance Entry.inhabited {α β σ} : Inhabited (Entry α β σ) := ⟨Entry.null⟩
 
 inductive Node (α : Type u) (β : Type v) : Type (max u v)
-| entries   (es : Array (Entry α β Node)) : Node
-| collision (ks : Array α) (vs : Array β) (h : ks.size = vs.size) : Node
+| entries   (es : Array (Entry α β (Node α β))) : Node α β
+| collision (ks : Array α) (vs : Array β) (h : ks.size = vs.size) : Node α β
 
 instance Node.inhabited {α β} : Inhabited (Node α β) := ⟨Node.entries #[]⟩
 
@@ -66,14 +67,14 @@ abbrev EntriesNode (α β) := { n : Node α β // IsEntriesNode n }
 
 private theorem setSizeEq {ks : Array α} {vs : Array β} (h : ks.size = vs.size) (i : Fin ks.size) (j : Fin vs.size) (k : α) (v : β)
                            : (ks.set i k).size = (vs.set j v).size :=
-have h₁ : (ks.set i k).size = ks.size from Array.szFSetEq _ _ _;
-have h₂ : (vs.set j v).size = vs.size from Array.szFSetEq _ _ _;
+have h₁ : (ks.set i k).size = ks.size by apply Array.szFSetEq
+have h₂ : (vs.set j v).size = vs.size by apply Array.szFSetEq
 (h₁.trans h).trans h₂.symm
 
 private theorem pushSizeEq {ks : Array α} {vs : Array β} (h : ks.size = vs.size) (k : α) (v : β) : (ks.push k).size = (vs.push v).size :=
-have h₁ : (ks.push k).size = ks.size + 1 from Array.szPushEq _ _;
-have h₂ : (vs.push v).size = vs.size + 1 from Array.szPushEq _ _;
-have h₃ : ks.size + 1 = vs.size + 1      from h ▸ rfl;
+have h₁ : (ks.push k).size = ks.size + 1 by apply Array.szPushEq
+have h₂ : (vs.push v).size = vs.size + 1 by apply Array.szPushEq
+have h₃ : ks.size + 1 = vs.size + 1      by rw h; exact rfl
 (h₁.trans h₃).trans h₂.symm
 
 partial def insertAtCollisionNodeAux [HasBeq α] : CollisionNode α β → Nat → α → β → CollisionNode α β
@@ -82,7 +83,7 @@ partial def insertAtCollisionNodeAux [HasBeq α] : CollisionNode α β → Nat 
     let idx : Fin keys.size := ⟨i, h⟩;
     let k' := keys.get idx;
     if k == k' then
-       let j : Fin vals.size := ⟨i, heq ▸ h⟩;
+       let j : Fin vals.size := ⟨i, by rw [←heq]; assumption⟩
        ⟨Node.collision (keys.set idx k) (vals.set j v) (setSizeEq heq idx j k v), IsCollisionNode.mk _ _ _⟩
     else insertAtCollisionNodeAux n (i+1) k v
   else
@@ -97,30 +98,28 @@ def getCollisionNodeSize : CollisionNode α β → Nat
 | ⟨Node.entries _, h⟩          => False.elim (nomatch h)
 
 def mkCollisionNode (k₁ : α) (v₁ : β) (k₂ : α) (v₂ : β) : Node α β :=
-let ks : Array α := Array.mkEmpty maxCollisions;
-let ks := (ks.push k₁).push k₂;
-let vs : Array β := Array.mkEmpty maxCollisions;
-let vs := (vs.push v₁).push v₂;
+let ks : Array α := Array.mkEmpty maxCollisions
+let ks := (ks.push k₁).push k₂
+let vs : Array β := Array.mkEmpty maxCollisions
+let vs := (vs.push v₁).push v₂
 Node.collision ks vs rfl
 
 partial def insertAux [HasBeq α] [Hashable α] : Node α β → USize → USize → α → β → Node α β
 | Node.collision keys vals heq, _, depth, k, v =>
-  let newNode := insertAtCollisionNode ⟨Node.collision keys vals heq, IsCollisionNode.mk _ _ _⟩ k v;
+  let newNode := insertAtCollisionNode ⟨Node.collision keys vals heq, IsCollisionNode.mk _ _ _⟩ k v
   if depth >= maxDepth || getCollisionNodeSize newNode < maxCollisions then newNode.val
   else match newNode with
     | ⟨Node.entries _, h⟩ => False.elim (nomatch h)
     | ⟨Node.collision keys vals heq, _⟩ =>
-      let entries : Node α β := mkEmptyEntries;
-      keys.iterate entries $ fun i k entries =>
-        let v := vals.get ⟨i.val, heq ▸ i.isLt⟩;
-        let h := hash k;
-        -- dbgTrace ("toCollision " ++ toString i ++ ", h: " ++ toString h ++ ", depth: " ++ toString depth ++ ", h': " ++
-        --          toString (div2Shift h (shift * (depth - 1)))) $ fun _ =>
-        let h := div2Shift h (shift * (depth - 1));
+      let entries : Node α β := mkEmptyEntries
+      keys.iterate entries fun i k entries =>
+        let v := vals.get ⟨i.val, by rw [←heq]; exact i.isLt⟩
+        let h := hash k
+        let h := div2Shift h (shift * (depth - 1))
         insertAux entries h depth k v
 | Node.entries entries, h, depth, k, v =>
-  let j     := (mod2Shift h shift).toNat;
-  Node.entries $ entries.modify j $ fun entry =>
+  let j     := (mod2Shift h shift).toNat
+  Node.entries $ entries.modify j fun entry =>
     match entry with
     | Entry.null        => Entry.entry k v
     | Entry.ref node    => Entry.ref $ insertAux node (div2Shift h shift) (depth+1) k v
@@ -134,14 +133,14 @@ def insert [HasBeq α] [Hashable α] : PersistentHashMap α β → α → β →
 partial def findAtAux [HasBeq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) : Nat → α → Option β
 | i, k =>
   if h : i < keys.size then
-    let k' := keys.get ⟨i, h⟩;
-    if k == k' then some (vals.get ⟨i, heq ▸ h⟩)
-    else findAtAux (i+1) k
+    let k' := keys.get ⟨i, h⟩
+    if k == k' then some (vals.get ⟨i, by rw [←heq]; assumption⟩)
+    else findAtAux keys vals heq (i+1) k
   else none
 
 partial def findAux [HasBeq α] : Node α β → USize → α → Option β
 | Node.entries entries, h, k =>
-  let j     := (mod2Shift h shift).toNat;
+  let j     := (mod2Shift h shift).toNat
   match entries.get! j with
   | Entry.null       => none
   | Entry.ref node   => findAux node (div2Shift h shift) k
@@ -165,14 +164,14 @@ match m.find? a with
 partial def findEntryAtAux [HasBeq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) : Nat → α → Option (α × β)
 | i, k =>
   if h : i < keys.size then
-    let k' := keys.get ⟨i, h⟩;
-    if k == k' then some (k', vals.get ⟨i, heq ▸ h⟩)
-    else findEntryAtAux (i+1) k
+    let k' := keys.get ⟨i, h⟩
+    if k == k' then some (k', vals.get ⟨i, by rw [←heq]; assumption⟩)
+    else findEntryAtAux keys vals heq (i+1) k
   else none
 
 partial def findEntryAux [HasBeq α] : Node α β → USize → α → Option (α × β)
 | Node.entries entries, h, k =>
-  let j     := (mod2Shift h shift).toNat;
+  let j     := (mod2Shift h shift).toNat
   match entries.get! j with
   | Entry.null       => none
   | Entry.ref node   => findEntryAux node (div2Shift h shift) k
@@ -185,14 +184,14 @@ def findEntry? [HasBeq α] [Hashable α] : PersistentHashMap α β → α → Op
 partial def containsAtAux [HasBeq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) : Nat → α → Bool
 | i, k =>
   if h : i < keys.size then
-    let k' := keys.get ⟨i, h⟩;
+    let k' := keys.get ⟨i, h⟩
     if k == k' then true
-    else containsAtAux (i+1) k
+    else containsAtAux keys vals heq (i+1) k
   else false
 
 partial def containsAux [HasBeq α] : Node α β → USize → α → Bool
 | Node.entries entries, h, k =>
-  let j     := (mod2Shift h shift).toNat;
+  let j     := (mod2Shift h shift).toNat
   match entries.get! j with
   | Entry.null       => false
   | Entry.ref node   => containsAux node (div2Shift h shift) k
@@ -206,11 +205,11 @@ partial def isUnaryEntries (a : Array (Entry α β (Node α β))) : Nat → Opti
 | i, acc =>
   if h : i < a.size then
     match a.get ⟨i, h⟩ with
-    | Entry.null      => isUnaryEntries (i+1) acc
+    | Entry.null      => isUnaryEntries a (i+1) acc
     | Entry.ref _     => none
     | Entry.entry k v =>
       match acc with
-      | none   => isUnaryEntries (i+1) (some (k, v))
+      | none   => isUnaryEntries a (i+1) (some (k, v))
       | some _ => none
   else acc
 
@@ -218,8 +217,8 @@ 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 from h ▸ (Nat.zeroLtSucc _);
-    some (keys.get ⟨0, this⟩, vals.get ⟨0, heq ▸ this⟩)
+    have 0 < keys.size by rw [←h]; exact decide!
+    some (keys.get ⟨0, this⟩, vals.get ⟨0, by rw [←heq]; assumption⟩)
   else
     none
 
@@ -227,21 +226,21 @@ partial def eraseAux [HasBeq α] : Node α β → USize → α → Node α β ×
 | n@(Node.collision keys vals heq), _, k =>
   match keys.indexOf? k with
   | some idx =>
-    let ⟨keys', keq⟩ := keys.eraseIdx' idx;
-    let ⟨vals', veq⟩ := vals.eraseIdx' (Eq.rec idx heq);
-    have keys.size - 1 = vals.size - 1 from heq ▸ rfl;
+    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]; exact rfl
     (Node.collision keys' vals' (keq.trans (this.trans veq.symm)), true)
   | none     => (n, false)
 | n@(Node.entries entries), h, k =>
-  let j       := (mod2Shift h shift).toNat;
-  let entry   := entries.get! j;
+  let j       := (mod2Shift h shift).toNat
+  let entry   := entries.get! j
   match entry with
   | Entry.null       => (n, false)
   | Entry.entry k' v =>
     if k == k' then (Node.entries (entries.set! j Entry.null), true) else (n, false)
   | Entry.ref node   =>
-    let entries := entries.set! j Entry.null;
-    let (newNode, deleted) := eraseAux node (div2Shift h shift) k;
+    let entries := entries.set! j Entry.null
+    let (newNode, deleted) := eraseAux node (div2Shift h shift) k
     if !deleted then (n, false)
     else match isUnaryNode newNode with
       | none        => (Node.entries (entries.set! j (Entry.ref newNode)), true)
@@ -249,8 +248,8 @@ partial def eraseAux [HasBeq α] : Node α β → USize → α → Node α β ×
 
 def erase [HasBeq α] [Hashable α] : PersistentHashMap α β → α → PersistentHashMap α β
 | { root := n, size := sz }, k =>
-  let h := hash k;
-  let (n, del) := eraseAux n h k;
+  let h := hash k
+  let (n, del) := eraseAux n h k
   { root := n, size := if del then sz - 1 else sz }
 
 section
@@ -258,12 +257,12 @@ variables {m : Type w → Type w'} [Monad m]
 variables {σ : Type w}
 
 @[specialize] partial def foldlMAux (f : σ → α → β → m σ) : Node α β → σ → m σ
-| Node.collision keys vals heq, acc => keys.iterateM acc $ fun i k acc => f acc k (vals.get ⟨i.val, heq ▸ i.isLt⟩)
+| Node.collision keys vals heq, acc => keys.iterateM acc fun i k acc => f acc k (vals.get ⟨i.val, by rw [←heq]; exact i.isLt⟩)
 | Node.entries entries, acc => entries.foldlM (fun acc entry =>
   match entry with
   | Entry.null      => pure acc
   | Entry.entry k v => f acc k v
-  | Entry.ref node  => foldlMAux node acc)
+  | Entry.ref node  => foldlMAux f node acc)
   acc
 
 @[specialize] def foldlM [HasBeq α] [Hashable α] (map : PersistentHashMap α β) (f : σ → α → β → m σ) (acc : σ) : m σ :=
@@ -295,7 +294,7 @@ partial def collectStats : Node α β → Stats → Nat → Stats
   let stats :=
     { stats with
       numNodes      := stats.numNodes + 1,
-      maxDepth      := Nat.max stats.maxDepth depth };
+      maxDepth      := Nat.max stats.maxDepth depth }
   entries.foldl (fun stats entry =>
     match entry with
     | Entry.null      => { stats with numNull := stats.numNull + 1 }
@@ -307,8 +306,7 @@ def stats [HasBeq α] [Hashable α] (m : PersistentHashMap α β) : Stats :=
 collectStats m.root {} 1
 
 def Stats.toString (s : Stats) : String :=
-"{ nodes := " ++  toString  s.numNodes ++ ", null := " ++ toString s.numNull ++
-", collisions := " ++ toString s.numCollisions ++ ", depth := " ++ toString s.maxDepth ++ "}"
+s!"\{ nodes := {s.numNodes}, null := {s.numNull}, collisions := {s.numCollisions}, depth := {s.maxDepth}}"
 
 instance : HasToString Stats := ⟨Stats.toString⟩
 
diff --git a/src/Std/Data/PersistentHashSet.lean b/src/Std/Data/PersistentHashSet.lean
index ed2947da7d..c6a33ab26c 100644
--- a/src/Std/Data/PersistentHashSet.lean
+++ b/src/Std/Data/PersistentHashSet.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
diff --git a/src/Std/Data/RBTree.lean b/src/Std/Data/RBTree.lean
index b2a7f460e0..424e9ed057 100644
--- a/src/Std/Data/RBTree.lean
+++ b/src/Std/Data/RBTree.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.