diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index b4e0f1e28f..89984c1ea6 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -236,47 +236,47 @@ end Ne
 section
 variable {α β φ : Sort u} {a a' : α} {b b' : β} {c : φ}
 
-theorem HEq.ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : {β : Sort u2} → β → Sort u1} (m : motive a) {β : Sort u2} {b : β} (h : a ≅ b) : motive b :=
+theorem HEq.ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : {β : Sort u2} → β → Sort u1} (m : motive a) {β : Sort u2} {b : β} (h : HEq a b) : motive b :=
   @HEq.rec α a (fun b _ => motive b) m β b h
 
-theorem HEq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : {β : Sort u2} → β → Sort u1} {β : Sort u2} {b : β} (h : a ≅ b) (m : motive a) : motive b :=
+theorem HEq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : {β : Sort u2} → β → Sort u1} {β : Sort u2} {b : β} (h : HEq a b) (m : motive a) : motive b :=
   @HEq.rec α a (fun b _ => motive b) m β b h
 
-theorem HEq.elim {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : a ≅ b) (h₂ : p a) : p b :=
+theorem HEq.elim {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : HEq a b) (h₂ : p a) : p b :=
   eq_of_heq h₁ ▸ h₂
 
-theorem HEq.subst {p : (T : Sort u) → T → Prop} (h₁ : a ≅ b) (h₂ : p α a) : p β b :=
+theorem HEq.subst {p : (T : Sort u) → T → Prop} (h₁ : HEq a b) (h₂ : p α a) : p β b :=
   HEq.ndrecOn h₁ h₂
 
-theorem HEq.symm (h : a ≅ b) : b ≅ a :=
-  HEq.ndrecOn (motive := fun x => x ≅ a) h (HEq.refl a)
+theorem HEq.symm (h : HEq a b) : HEq b a :=
+  HEq.ndrecOn (motive := fun x => HEq x a) h (HEq.refl a)
 
-theorem heq_of_eq (h : a = a') : a ≅ a' :=
+theorem heq_of_eq (h : a = a') : HEq a a' :=
   Eq.subst h (HEq.refl a)
 
-theorem HEq.trans (h₁ : a ≅ b) (h₂ : b ≅ c) : a ≅ c :=
+theorem HEq.trans (h₁ : HEq a b) (h₂ : HEq b c) : HEq a c :=
   HEq.subst h₂ h₁
 
-theorem heq_of_heq_of_eq (h₁ : a ≅ b) (h₂ : b = b') : a ≅ b' :=
+theorem heq_of_heq_of_eq (h₁ : HEq a b) (h₂ : b = b') : HEq a b' :=
   HEq.trans h₁ (heq_of_eq h₂)
 
-theorem heq_of_eq_of_heq (h₁ : a = a') (h₂ : a' ≅ b) : a ≅ b :=
+theorem heq_of_eq_of_heq (h₁ : a = a') (h₂ : HEq a' b) : HEq a b :=
   HEq.trans (heq_of_eq h₁) h₂
 
-def type_eq_of_heq (h : a ≅ b) : α = β :=
+def type_eq_of_heq (h : HEq a b) : α = β :=
   HEq.ndrecOn (motive := @fun (x : Sort u) _ => α = x) h (Eq.refl α)
 
 end
 
-theorem eqRec_heq {α : Sort u} {φ : α → Sort v} {a a' : α} : (h : a = a') → (p : φ a) → (Eq.recOn (motive := fun x _ => φ x) h p) ≅ p
+theorem eqRec_heq {α : Sort u} {φ : α → Sort v} {a a' : α} : (h : a = a') → (p : φ a) → HEq (Eq.recOn (motive := fun x _ => φ x) h p) p
   | rfl, p => HEq.refl p
 
-theorem heq_of_eqRec_eq {α β : Sort u} {a : α} {b : β} (h₁ : α = β) (h₂ : Eq.rec (motive := fun α _ => α) a h₁ = b) : a ≅ b := by
+theorem heq_of_eqRec_eq {α β : Sort u} {a : α} {b : β} (h₁ : α = β) (h₂ : Eq.rec (motive := fun α _ => α) a h₁ = b) : HEq a b := by
   subst h₁
   apply heq_of_eq
   exact h₂
 
-theorem cast_heq {α β : Sort u} : (h : α = β) → (a : α) → cast h a ≅ a
+theorem cast_heq {α β : Sort u} : (h : α = β) → (a : α) → HEq (cast h a) a
   | rfl, a => HEq.refl a
 
 variable {a b c d : Prop}
@@ -472,7 +472,7 @@ class Subsingleton (α : Sort u) : Prop where
 protected def Subsingleton.elim {α : Sort u} [h : Subsingleton α] : (a b : α) → a = b :=
   h.allEq
 
-protected def Subsingleton.helim {α β : Sort u} [h₁ : Subsingleton α] (h₂ : α = β) (a : α) (b : β) : a ≅ b := by
+protected def Subsingleton.helim {α β : Sort u} [h₁ : Subsingleton α] (h₂ : α = β) (a : α) (b : β) : HEq a b := by
   subst h₂
   apply heq_of_eq
   apply Subsingleton.elim
@@ -761,10 +761,10 @@ protected abbrev recOnSubsingleton
 protected abbrev hrecOn
     (q : Quot r)
     (f : (a : α) → motive (Quot.mk r a))
-    (c : (a b : α) → (p : r a b) → f a ≅ f b)
+    (c : (a b : α) → (p : r a b) → HEq (f a) (f b))
     : motive q :=
   Quot.recOn q f fun a b p => eq_of_heq <|
-    have p₁ : Eq.ndrec (f a) (sound p) ≅ f a := eqRec_heq (sound p) (f a)
+    have p₁ : HEq (Eq.ndrec (f a) (sound p)) (f a) := eqRec_heq (sound p) (f a)
     HEq.trans p₁ (c a b p)
 
 end
@@ -830,7 +830,7 @@ protected abbrev recOnSubsingleton
 protected abbrev hrecOn
     (q : Quotient s)
     (f : (a : α) → motive (Quotient.mk a))
-    (c : (a b : α) → (p : a ≈ b) → f a ≅ f b)
+    (c : (a b : α) → (p : a ≈ b) → HEq (f a) (f b))
     : motive q :=
   Quot.hrecOn q f c
 end
diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index 37a6e52f44..71318d583b 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -100,8 +100,6 @@ infix:50 " ≥ "  => GE.ge
 infix:50 " > "  => GT.gt
 infix:50 " = "  => Eq
 infix:50 " == " => BEq.beq
-infix:50 " ~= " => HEq
-infix:50 " ≅ "  => HEq
 /-
   Remark: the infix commands above ensure a delaborator is generated for each relations.
   We redefine the macros below to be able to use the auxiliary `binrel%` elaboration helper for binary relations.
diff --git a/tests/lean/223.lean b/tests/lean/223.lean
index 34ef6ca335..c44647b8a9 100644
--- a/tests/lean/223.lean
+++ b/tests/lean/223.lean
@@ -7,7 +7,7 @@ def h {α β} {f : α → β} : {b : β} → Imf f b → α
 | _, Imf.mk a => a
 
 #print h
-
+infix:50 " ≅ "  => HEq
 theorem ex : ∀ {α β : Sort u} (h : α = β) (a : α), cast h a ≅ a
   | α, _, rfl, a => HEq.refl a
 
diff --git a/tests/lean/calcErrors.lean b/tests/lean/calcErrors.lean
index 2dc9194180..7bd0b4e6da 100644
--- a/tests/lean/calcErrors.lean
+++ b/tests/lean/calcErrors.lean
@@ -18,7 +18,7 @@ theorem ex4 (p : Nat → Prop) (a b : Nat) (h₁ : p a) (h₂ : p b) : p c :=
 theorem ex5 (p : Nat → Nat → Prop) (a b : Nat) (h₁ : p a b) (h₂ : p b c) : p a c :=
   calc  p a b := h₁
         p _ c := h₂
-
+infix:50 " ≅ "  => HEq
 instance {α β γ} : Trans (. ≅ . : α → β → Prop) (. ≅ . : β → γ → Prop) (. ≅ . : α → γ → Prop) where
   trans h₁ h₂ := HEq.trans h₁ h₂
 
diff --git a/tests/lean/doSeqRightIssue.lean b/tests/lean/doSeqRightIssue.lean
index b864eba36d..00f580ec79 100644
--- a/tests/lean/doSeqRightIssue.lean
+++ b/tests/lean/doSeqRightIssue.lean
@@ -3,7 +3,7 @@ set_option autoBoundImplicitLocal false
 universe u
 variable {α : Type u}
 variable {β : α → Type v}
-
+infix:50 " ≅ " => HEq
 theorem ex {p₁ p₂ : Sigma (fun a => β a)} (h₁ : p₁.1 = p₂.1) (h : p₁.2 ≅ p₂.2) : p₁ = p₂ :=
 match p₁, p₂, h₁, h with
 | ⟨_, _⟩, ⟨_, _⟩, rfl, HEq.refl _ => rfl
diff --git a/tests/lean/infoTree.lean.expected.out b/tests/lean/infoTree.lean.expected.out
index b108674f70..7bb8280f2a 100644
--- a/tests/lean/infoTree.lean.expected.out
+++ b/tests/lean/infoTree.lean.expected.out
@@ -51,7 +51,7 @@
         [.] `Bool : some Sort.{?_uniq.441} @ ⟨17, 27⟩-⟨17, 31⟩
         Bool : Type @ ⟨17, 27⟩-⟨17, 31⟩
       b : Bool @ ⟨17, 23⟩-⟨17, 24⟩
-      x + 0 = x : Prop @ ⟨17, 35⟩-⟨17, 44⟩ @ myMacro._@.Init.Notation._hyg.9571
+      x + 0 = x : Prop @ ⟨17, 35⟩-⟨17, 44⟩ @ myMacro._@.Init.Notation._hyg.9093
         Macro expansion
         x + 0 = x
         ===>
diff --git a/tests/lean/match3.lean b/tests/lean/match3.lean
index e44603ab11..ddfad75da5 100644
--- a/tests/lean/match3.lean
+++ b/tests/lean/match3.lean
@@ -9,7 +9,7 @@ match x with
 #eval f 30
 
 universe u
-
+infix:50 " ≅ " => HEq
 theorem ex1 {α : Sort u} {a b : α} (h : a ≅ b) : a = b :=
 match α, a, b, h with
 | _, _, _, HEq.refl _ => rfl
diff --git a/tests/lean/ppMotives.lean b/tests/lean/ppMotives.lean
index 0a42aa62b7..79458499fd 100644
--- a/tests/lean/ppMotives.lean
+++ b/tests/lean/ppMotives.lean
@@ -6,7 +6,7 @@ set_option pp.motives.pi true
 
 #print Nat.add
 
-theorem ex : ∀ {α β : Sort u} (h : α = β) (a : α), cast h a ≅ a
+theorem ex : ∀ {α β : Sort u} (h : α = β) (a : α), HEq (cast h a) a
   | α, _, rfl, a => HEq.refl a
 
 set_option pp.motives.nonConst false
diff --git a/tests/lean/ppMotives.lean.expected.out b/tests/lean/ppMotives.lean.expected.out
index cbf9b3df61..6618f066e1 100644
--- a/tests/lean/ppMotives.lean.expected.out
+++ b/tests/lean/ppMotives.lean.expected.out
@@ -16,13 +16,13 @@ fun x x_1 =>
         | a, Nat.succ b => fun x => Nat.succ (PProd.fst x.fst a))
         f)
     x
-theorem ex.{u} : ∀ {α β : Sort u} (h : α = β) (a : α), cast h a ≅ a :=
+theorem ex.{u} : ∀ {α β : Sort u} (h : α = β) (a : α), HEq (cast h a) a :=
 fun x x_1 x_2 x_3 =>
   match x, x_1, x_2, x_3 with 
   | α, .(α), Eq.refl α, a => HEq.refl a
-theorem ex.{u} : ∀ {α β : Sort u} (h : α = β) (a : α), cast h a ≅ a :=
+theorem ex.{u} : ∀ {α β : Sort u} (h : α = β) (a : α), HEq (cast h a) a :=
 fun x x_1 x_2 x_3 =>
-  match x, x_1, x_2, x_3 : ∀ (x x_4 : Sort u) (x_5 : x = x_4) (x_6 : x), cast x_5 x_6 ≅ x_6 with 
+  match x, x_1, x_2, x_3 : ∀ (x x_4 : Sort u) (x_5 : x = x_4) (x_6 : x), HEq (cast x_5 x_6) x_6 with 
   | α, .(α), Eq.refl α, a => HEq.refl a
 def fact : Nat → Nat :=
 fun n => Nat.recOn n 1 fun n acc => (n + 1) * acc
diff --git a/tests/lean/run/discrRefinement2.lean b/tests/lean/run/discrRefinement2.lean
index 996441117e..56ee80495d 100644
--- a/tests/lean/run/discrRefinement2.lean
+++ b/tests/lean/run/discrRefinement2.lean
@@ -1,3 +1,4 @@
+infix:50 " ≅ "  => HEq
 theorem ex1 {α : Sort u} {a b : α} (h : a ≅ b) : a = b :=
   match h with
   | HEq.refl _ => rfl