chore: fix tests

src/Init/Core.lean

@@ -897,43 +897,43 @@ section
 variable {α β φ : Sort u} {a a' : α} {b b' : β} {c : φ}
 
 /-- Non-dependent recursor for `HEq` -/
-noncomputable def HEq.ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : {β : Sort u2} → β → Sort u1} (m : motive a) {β : Sort u2} {b : β} (h : HEq a b) : motive b :=
+noncomputable def HEq.ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : {β : Sort u2} → β → Sort u1} (m : motive a) {β : Sort u2} {b : β} (h : a ≍ b) : motive b :=
   h.rec m
 
 /-- `HEq.ndrec` variant -/
-noncomputable def HEq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : {β : Sort u2} → β → Sort u1} {β : Sort u2} {b : β} (h : HEq a b) (m : motive a) : motive b :=
+noncomputable def HEq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : {β : Sort u2} → β → Sort u1} {β : Sort u2} {b : β} (h : a ≍ b) (m : motive a) : motive b :=
   h.rec m
 
 /-- `HEq.ndrec` variant -/
-noncomputable def HEq.elim {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : HEq a b) (h₂ : p a) : p b :=
+noncomputable def HEq.elim {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : a ≍ b) (h₂ : p a) : p b :=
   eq_of_heq h₁ ▸ h₂
 
 /-- Substitution with heterogeneous equality. -/
-theorem HEq.subst {p : (T : Sort u) → T → Prop} (h₁ : HEq a b) (h₂ : p α a) : p β b :=
+theorem HEq.subst {p : (T : Sort u) → T → Prop} (h₁ : a ≍ b) (h₂ : p α a) : p β b :=
   HEq.ndrecOn h₁ h₂
 
 /-- Heterogeneous equality is symmetric. -/
-@[symm] theorem HEq.symm (h : HEq a b) : HEq b a :=
+@[symm] theorem HEq.symm (h : a ≍ b) : b ≍ a :=
   h.rec (HEq.refl a)
 
 /-- Propositionally equal terms are also heterogeneously equal. -/
-theorem heq_of_eq (h : a = a') : HEq a a' :=
+theorem heq_of_eq (h : a = a') : a ≍ a' :=
   Eq.subst h (HEq.refl a)
 
 /-- Heterogeneous equality is transitive. -/
-theorem HEq.trans (h₁ : HEq a b) (h₂ : HEq b c) : HEq a c :=
+theorem HEq.trans (h₁ : a ≍ b) (h₂ : b ≍ c) : a ≍ c :=
   HEq.subst h₂ h₁
 
 /-- Heterogeneous equality precomposes with propositional equality. -/
-theorem heq_of_heq_of_eq (h₁ : HEq a b) (h₂ : b = b') : HEq a b' :=
+theorem heq_of_heq_of_eq (h₁ : a ≍ b) (h₂ : b = b') : a ≍ b' :=
   HEq.trans h₁ (heq_of_eq h₂)
 
 /-- Heterogeneous equality postcomposes with propositional equality. -/
-theorem heq_of_eq_of_heq (h₁ : a = a') (h₂ : HEq a' b) : HEq a b :=
+theorem heq_of_eq_of_heq (h₁ : a = a') (h₂ : a' ≍ b) : a ≍ b :=
   HEq.trans (heq_of_eq h₁) h₂
 
 /-- If two terms are heterogeneously equal then their types are propositionally equal. -/
-theorem type_eq_of_heq (h : HEq a b) : α = β :=
+theorem type_eq_of_heq (h : a ≍ b) : α = β :=
   h.rec (Eq.refl α)
 
 end
@@ -942,7 +942,7 @@ end
 Rewriting inside `φ` using `Eq.recOn` yields a term that's heterogeneously equal to the original
 term.
 -/
-theorem eqRec_heq {α : Sort u} {φ : α → Sort v} {a a' : α} : (h : a = a') → (p : φ a) → HEq (Eq.recOn (motive := fun x _ => φ x) h p) p
+theorem eqRec_heq {α : Sort u} {φ : α → Sort v} {a a' : α} : (h : a = a') → (p : φ a) → Eq.recOn (motive := fun x _ => φ x) h p ≍ p
   | rfl, p => HEq.refl p
 
 /--
@@ -950,8 +950,8 @@ Heterogeneous equality with an `Eq.rec` application on the left is equivalent to
 equality on the original term.
 -/
 theorem eqRec_heq_iff {α : Sort u} {a : α} {motive : (b : α) → a = b → Sort v}
-    {b : α} {refl : motive a (Eq.refl a)} {h : a = b} {c : motive b h} :
-    HEq (@Eq.rec α a motive refl b h) c ↔ HEq refl c :=
+    {b : α} {refl : motive a (Eq.refl a)} {h : a = b} {c : motive b h}
+    : @Eq.rec α a motive refl b h ≍ c ↔ refl ≍ c :=
   h.rec (fun _ => ⟨id, id⟩) c
 
 /--
@@ -960,7 +960,7 @@ equality on the original term.
 -/
 theorem heq_eqRec_iff {α : Sort u} {a : α} {motive : (b : α) → a = b → Sort v}
     {b : α} {refl : motive a (Eq.refl a)} {h : a = b} {c : motive b h} :
-    HEq c (@Eq.rec α a motive refl b h) ↔ HEq c refl :=
+    c ≍ @Eq.rec α a motive refl b h ↔ c ≍ refl :=
   h.rec (fun _ => ⟨id, id⟩) c
 
 /--
@@ -977,7 +977,7 @@ theorem apply_eqRec {α : Sort u} {a : α} (motive : (b : α) → a = b → Sort
 If casting a term with `Eq.rec` to another type makes it equal to some other term, then the two
 terms are heterogeneously equal.
 -/
-theorem heq_of_eqRec_eq {α β : Sort u} {a : α} {b : β} (h₁ : α = β) (h₂ : Eq.rec (motive := fun α _ => α) a h₁ = b) : HEq a b := by
+theorem heq_of_eqRec_eq {α β : Sort u} {a : α} {b : β} (h₁ : α = β) (h₂ : Eq.rec (motive := fun α _ => α) a h₁ = b) : a ≍ b := by
   subst h₁
   apply heq_of_eq
   exact h₂
@@ -985,7 +985,7 @@ theorem heq_of_eqRec_eq {α β : Sort u} {a : α} {b : β} (h₁ : α = β) (h
 /--
 The result of casting a term with `cast` is heterogeneously equal to the original term.
 -/
-theorem cast_heq {α β : Sort u} : (h : α = β) → (a : α) → HEq (cast h a) a
+theorem cast_heq {α β : Sort u} : (h : α = β) → (a : α) → cast h a ≍ a
   | rfl, a => HEq.refl a
 
 variable {a b c d : Prop}
@@ -1014,8 +1014,8 @@ instance : Trans Iff Iff Iff where
 theorem Eq.comm {a b : α} : a = b ↔ b = a := Iff.intro Eq.symm Eq.symm
 theorem eq_comm {a b : α} : a = b ↔ b = a := Eq.comm
 
-theorem HEq.comm {a : α} {b : β} : HEq a b ↔ HEq b a := Iff.intro HEq.symm HEq.symm
-theorem heq_comm {a : α} {b : β} : HEq a b ↔ HEq b a := HEq.comm
+theorem HEq.comm {a : α} {b : β} : a ≍ b ↔ b ≍ a := Iff.intro HEq.symm HEq.symm
+theorem heq_comm {a : α} {b : β} : a ≍ b ↔ b ≍ a := HEq.comm
 
 @[symm] theorem Iff.symm (h : a ↔ b) : b ↔ a := Iff.intro h.mpr h.mp
 theorem Iff.comm : (a ↔ b) ↔ (b ↔ a) := Iff.intro Iff.symm Iff.symm
@@ -1239,7 +1239,7 @@ protected theorem Subsingleton.elim {α : Sort u} [h : Subsingleton α] : (a b :
 If two types are equal and one of them is a subsingleton, then all of their elements are
 [heterogeneously equal](lean-manual://section/HEq).
 -/
-protected theorem Subsingleton.helim {α β : Sort u} [h₁ : Subsingleton α] (h₂ : α = β) (a : α) (b : β) : HEq a b := by
+protected theorem Subsingleton.helim {α β : Sort u} [h₁ : Subsingleton α] (h₂ : α = β) (a : α) (b : β) : a ≍ b := by
   subst h₂
   apply heq_of_eq
   apply Subsingleton.elim
@@ -1690,7 +1690,7 @@ theorem true_iff_false : (True ↔ False) ↔ False := iff_false_intro (·.mp  T
 theorem false_iff_true : (False ↔ True) ↔ False := iff_false_intro (·.mpr True.intro)
 
 theorem iff_not_self : ¬(a ↔ ¬a) | H => let f h := H.1 h h; f (H.2 f)
-theorem heq_self_iff_true (a : α) : HEq a a ↔ True := iff_true_intro HEq.rfl
+theorem heq_self_iff_true (a : α) : a ≍ a ↔ True := iff_true_intro HEq.rfl
 
 /-! ## implies -/
 
@@ -1890,7 +1890,7 @@ a structure.
 protected abbrev hrecOn
     (q : Quot r)
     (f : (a : α) → motive (Quot.mk r a))
-    (c : (a b : α) → (p : r a b) → HEq (f a) (f b))
+    (c : (a b : α) → (p : r a b) → f a ≍ f b)
     : motive q :=
   Quot.recOn q f fun a b p => eq_of_heq (eqRec_heq_iff.mpr (c a b p))
 
@@ -2088,7 +2088,7 @@ a structure.
 protected abbrev hrecOn
     (q : Quotient s)
     (f : (a : α) → motive (Quotient.mk s a))
-    (c : (a b : α) → (p : a ≈ b) → HEq (f a) (f b))
+    (c : (a b : α) → (p : a ≈ b) → f a ≍ f b)
     : motive q :=
   Quot.hrecOn q f c
 end

src/Init/Grind/Lemmas.lean

@@ -147,17 +147,17 @@ theorem dite_cond_eq_false' {α : Sort u} {c : Prop} {_ : Decidable c} {a : c
 
 theorem eqRec_heq.{u_1, u_2} {α : Sort u_2} {a : α}
         {motive : (x : α) → a = x → Sort u_1} (v : motive a (Eq.refl a)) {b : α} (h : a = b)
-        : HEq (@Eq.rec α a motive v b h) v := by
+        : @Eq.rec α a motive v b h ≍ v := by
  subst h; rfl
 
 theorem eqRecOn_heq.{u_1, u_2} {α : Sort u_2} {a : α}
         {motive : (x : α) → a = x → Sort u_1} {b : α} (h : a = b) (v : motive a (Eq.refl a))
-        : HEq (@Eq.recOn α a motive b h v) v := by
+        : @Eq.recOn α a motive b h v ≍ v := by
  subst h; rfl
 
 theorem eqNDRec_heq.{u_1, u_2} {α : Sort u_2} {a : α}
         {motive : α → Sort u_1} (v : motive a) {b : α} (h : a = b)
-        : HEq (@Eq.ndrec α a motive v b h) v := by
+        : @Eq.ndrec α a motive v b h ≍ v := by
  subst h; rfl
 
 /-! decide -/

src/Init/Notation.lean

@@ -377,6 +377,8 @@ recommended_spelling "not" for "~~~" in [Complement.complement, «term~~~_»]
 @[inherit_doc] infix:50 " > "  => GT.gt
 @[inherit_doc] infix:50 " = "  => Eq
 @[inherit_doc] infix:50 " == " => BEq.beq
+@[inherit_doc] 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.

src/Init/SimpLemmas.lean

@@ -284,7 +284,7 @@ theorem Bool.not_eq_false' (b : Bool) : ((!b) = false) = (b = true) := by simp
   cases g <;> (rename_i gp; simp [gp])
 theorem not_decide_eq_true [h : Decidable p] : ((!decide p) = true) = ¬ p := by simp
 
-@[simp] theorem heq_eq_eq (a b : α) : HEq a b = (a = b) := propext <| Iff.intro eq_of_heq heq_of_eq
+@[simp] theorem heq_eq_eq (a b : α) : (a ≍ b) = (a = b) := propext <| Iff.intro eq_of_heq heq_of_eq
 
 @[simp] theorem cond_true (a b : α) : cond true a b = a := rfl
 @[simp] theorem cond_false (a b : α) : cond false a b = b := rfl

tests/lean/ppMotives.lean.expected.out

@@ -16,13 +16,13 @@ fun x x_1 =>
         | a, b.succ => fun x => (x.1 a).succ)
         f)
     x
-theorem ex.{u} : ∀ {α β : Sort u} (h : α = β) (a : α), HEq (cast h a) a :=
+theorem ex.{u} : ∀ {α β : Sort u} (h : α = β) (a : α), 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 : α), HEq (cast h a) a :=
+theorem ex.{u} : ∀ {α β : Sort u} (h : α = β) (a : α), cast h a ≍ a :=
 fun x x_1 x_2 x_3 =>
-  match (motive := ∀ (x x_4 : Sort u) (x_5 : x = x_4) (x_6 : x), HEq (cast x_5 x_6) x_6) x, x_1, x_2, x_3 with
+  match (motive := ∀ (x x_4 : Sort u) (x_5 : x = x_4) (x_6 : x), cast x_5 x_6 ≍ x_6) x, x_1, x_2, x_3 with
   | α, .(α), Eq.refl α, a => HEq.refl a
 def fact : Nat → Nat :=
 fun n => Nat.recOn n 1 fun n acc => (n + 1) * acc

tests/lean/run/congrReserved.lean

@@ -2,8 +2,8 @@ import Lean
 
 /--
 info: Vector.extract.hcongr_5.{u_1} (α α' : Type u_1) (e_1 : α = α') (n n' : Nat) (e_2 : n = n') (xs : Vector α n)
-  (xs' : Vector α' n') (e_3 : HEq xs xs') (start start' : Nat) (e_4 : start = start') (stop stop' : Nat)
-  (e_5 : stop = stop') : HEq (xs.extract start stop) (xs'.extract start' stop')
+  (xs' : Vector α' n') (e_3 : xs ≍ xs') (start start' : Nat) (e_4 : start = start') (stop stop' : Nat)
+  (e_5 : stop = stop') : xs.extract start stop ≍ xs'.extract start' stop'
 -/
 #guard_msgs in
 #check Vector.extract.hcongr_5

tests/lean/run/congrThm2.lean

@@ -20,13 +20,13 @@ info: ∀ (coll coll' : Type u),
         ∀ (elem elem' : Type w),
           elem = elem' →
             ∀ (valid : coll → idx → Prop) (valid' : coll' → idx' → Prop),
-              HEq valid valid' →
+              valid ≍ valid' →
                 ∀ (self : GetElem coll idx elem valid) (self' : GetElem coll' idx' elem' valid'),
-                  HEq self self' →
+                  self ≍ self' →
                     ∀ (xs : coll) (xs' : coll'),
-                      HEq xs xs' →
+                      xs ≍ xs' →
                         ∀ (i : idx) (i' : idx'),
-                          HEq i i' → ∀ (h : valid xs i) (h' : valid' xs' i'), HEq h h' → HEq xs[i] xs'[i']
+                          i ≍ i' → ∀ (h : valid xs i) (h' : valid' xs' i'), h ≍ h' → xs[i] ≍ xs'[i']
 -/
 #guard_msgs in
 #eval genHCongr ``GetElem.getElem
@@ -41,7 +41,7 @@ info: ∀ {coll : Type u} {idx : Type v} {elem : Type w} {valid : coll → idx
 def f (x := 0) (_ : x = x := by rfl) := x + 1
 
 /--
-info: ∀ (x x' : Nat), x = x' → ∀ (x_1 : x = x) (x'_1 : x' = x'), HEq x_1 x'_1 → HEq (f x x_1) (f x' x'_1)
+info: ∀ (x x' : Nat), x = x' → ∀ (x_1 : x = x) (x'_1 : x' = x'), x_1 ≍ x'_1 → f x x_1 ≍ f x' x'_1
 -/
 #guard_msgs in
 #eval genHCongr ``f

tests/lean/run/generalizeMany.lean

@@ -7,7 +7,7 @@ v : Fin n
 n' : Nat
 v' : Fin n'
 h₁ : n + 1 = n'
-h₂ : HEq v.succ v'
+h₂ : v.succ ≍ v'
 ⊢ p n' v'
 ---
 warning: declaration uses 'sorry'

tests/lean/run/genindices.lean

@@ -36,7 +36,7 @@ trace: [Elab] ⊢ ∀ (α : Type u) (xs : List (List α)) (h : Pred (List α) xs
     α : Type u
     a✝ : List α
     h✝ : Pred α a✝
-    ⊢ List α✝ = α → HEq xs✝ a✝ → HEq h✝¹ h✝ → xs✝ ≠ [] → xs✝ = xs✝
+    ⊢ List α✝ = α → xs✝ ≍ a✝ → h✝¹ ≍ h✝ → xs✝ ≠ [] → xs✝ = xs✝
 -/
 #guard_msgs in
 #eval tst1

tests/lean/run/grind_cases_tac.lean

@@ -18,12 +18,12 @@ def f (v : Vec α n) : Bool :=
 trace: n : Nat
 v : Vec Nat n
 h : f v ≠ false
-⊢ n + 1 = 0 → HEq (Vec.cons 10 v) Vec.nil → False
+⊢ n + 1 = 0 → Vec.cons 10 v ≍ Vec.nil → False
 ---
 trace: n : Nat
 v : Vec Nat n
 h : f v ≠ false
-⊢ ∀ {n_1 : Nat} (a : Nat) (a_1 : Vec Nat n_1), n + 1 = n_1 + 1 → HEq (Vec.cons 10 v) (Vec.cons a a_1) → False
+⊢ ∀ {n_1 : Nat} (a : Nat) (a_1 : Vec Nat n_1), n + 1 = n_1 + 1 → Vec.cons 10 v ≍ Vec.cons a a_1 → False
 -/
 #guard_msgs (trace) in
 example (v : Vec Nat n) (h : f v ≠ false) : False := by

tests/lean/run/grind_eq.lean

@@ -69,9 +69,9 @@ trace: [grind.assert] x1 = appV a_2 b
 [grind.assert] x2 = appV x1 c
 [grind.assert] x3 = appV b c
 [grind.assert] x4 = appV a_2 x3
-[grind.assert] ¬HEq x2 x4
-[grind.ematch.instance] appV_assoc: HEq (appV a_2 (appV b c)) (appV (appV a_2 b) c)
-[grind.assert] HEq (appV a_2 (appV b c)) (appV (appV a_2 b) c)
+[grind.assert] ¬x2 ≍ x4
+[grind.ematch.instance] appV_assoc: appV a_2 (appV b c) ≍ appV (appV a_2 b) c
+[grind.assert] appV a_2 (appV b c) ≍ appV (appV a_2 b) c
 -/
 #guard_msgs (trace) in
 example : x1 = appV a b → x2 = appV x1 c → x3 = appV b c → x4 = appV a x3 → HEq x2 x4 := by

tests/lean/run/grind_pre.lean

@@ -140,16 +140,16 @@ case grind.1
 α : Type
 a : α
 p q r : Prop
-h₁ : HEq p a
-h₂ : HEq q a
+h₁ : p ≍ a
+h₂ : q ≍ a
 h₃ : p = r
 left : p
 right : r
 ⊢ False
 [grind] Goal diagnostics
   [facts] Asserted facts
-    [prop] HEq p a
-    [prop] HEq q a
+    [prop] p ≍ a
+    [prop] q ≍ a
     [prop] p = r
     [prop] p
     [prop] r
@@ -193,14 +193,14 @@ f : Nat → Bool
 g : Int → Bool
 a : Nat
 b : Int
-h : HEq f g
-h_1 : HEq a b
+h : f ≍ g
+h_1 : a ≍ b
 h_2 : ¬f a = g b
 ⊢ False
 [grind] Goal diagnostics
   [facts] Asserted facts
-    [prop] HEq f g
-    [prop] HEq a b
+    [prop] f ≍ g
+    [prop] a ≍ b
     [prop] ¬f a = g b
   [eqc] False propositions
     [prop] f a = g b

tests/lean/run/grind_split_issue.lean

@@ -11,13 +11,13 @@ c : Nat
 q : X c 0
 s : Nat
 h : 0 = s
-h_1 : HEq ⋯ ⋯
+h_1 : ⋯ ≍ ⋯
 ⊢ False
 [grind] Goal diagnostics
   [facts] Asserted facts
     [prop] X c 0
     [prop] 0 = s
-    [prop] HEq ⋯ ⋯
+    [prop] ⋯ ≍ ⋯
   [eqc] True propositions
     [prop] X c 0
     [prop] X c s

tests/lean/run/linearNoConfusion.lean

@@ -58,7 +58,7 @@ info: @[reducible] protected def Vec.noConfusionType.{u_1, u} : {α : Type} →
   {a : Nat} → Sort u_1 → Vec α a → Vec α a → Sort u_1 :=
 fun {α} {a} P x1 x2 =>
   Vec.casesOn x1 (Vec.noConfusionType.withCtor α (Sort u_1) 0 (fun x => P → P) P a x2) fun {n} a_1 a_2 =>
-    Vec.noConfusionType.withCtor α (Sort u_1) 1 (fun x {n_1} a a_3 => (n = n_1 → a_1 = a → HEq a_2 a_3 → P) → P) P a x2
+    Vec.noConfusionType.withCtor α (Sort u_1) 1 (fun x {n_1} a a_3 => (n = n_1 → a_1 = a → a_2 ≍ a_3 → P) → P) P a x2
 -/
 #guard_msgs in
 #print Vec.noConfusionType

tests/lean/run/matchCongrEqns.lean

@@ -24,11 +24,10 @@ info: myTest.match_1.splitter.{u_1, u_2} {α : Type u_1} (motive : List α → S
 info: myTest.match_1.congr_eq_1.{u_1, u_2} {α : Type u_1} (motive : List α → Sort u_2) (x✝ : List α)
   (h_1 : (a : α) → (dc : List α) → x✝ = a :: dc → motive (a :: dc)) (h_2 : (x' : List α) → x✝ = x' → motive x') (a : α)
   (dc : List α) (heq_1 : x✝ = a :: dc) :
-  HEq
-    (match h : x✝ with
+  (match h : x✝ with
     | a :: dc => h_1 a dc h
-    | x' => h_2 x' h)
-    (h_1 a dc heq_1)
+    | x' => h_2 x' h) ≍
+    h_1 a dc heq_1
 -/
 #guard_msgs(pass trace, all) in
 #check myTest.match_1.congr_eq_1
@@ -38,11 +37,10 @@ info: myTest.match_1.congr_eq_2.{u_1, u_2} {α : Type u_1} (motive : List α →
   (h_1 : (a : α) → (dc : List α) → x✝ = a :: dc → motive (a :: dc)) (h_2 : (x' : List α) → x✝ = x' → motive x')
   (x' : List α) (heq_1 : x✝ = x') :
   (∀ (a : α) (dc : List α), x' = a :: dc → False) →
-    HEq
-      (match h : x✝ with
+    (match h : x✝ with
       | a :: dc => h_1 a dc h
-      | x' => h_2 x' h)
-      (h_2 x' heq_1)
+      | x' => h_2 x' h) ≍
+      h_2 x' heq_1
 -/
 #guard_msgs(pass trace, all) in
 #check myTest.match_1.congr_eq_2
@@ -66,12 +64,11 @@ info: take.match_1.congr_eq_1.{u_1, u_2} {α : Type u_1} (motive : Nat → List
   (h_1 : (x : List α) → motive 0 x) (h_2 : (n : Nat) → motive n.succ [])
   (h_3 : (n : Nat) → (a : α) → (as : List α) → motive n.succ (a :: as)) (x✝ : List α) (heq_1 : n✝ = 0)
   (heq_2 : xs✝ = x✝) :
-  HEq
-    (match n✝, xs✝ with
+  (match n✝, xs✝ with
     | 0, x => h_1 x
     | n.succ, [] => h_2 n
-    | n.succ, a :: as => h_3 n a as)
-    (h_1 x✝)
+    | n.succ, a :: as => h_3 n a as) ≍
+    h_1 x✝
 -/
 #guard_msgs(pass trace, all) in #check take.match_1.congr_eq_1
 
@@ -85,11 +82,10 @@ def matchOptionUnit (o? : Option Unit) : Bool := Id.run do
 info: matchOptionUnit.match_1.congr_eq_1.{u_1} (motive : Option Unit → Sort u_1) (o?✝ : Option Unit)
   (h_1 : (val : Unit) → motive (some val)) (h_2 : (x : Option Unit) → motive x) (val✝ : Unit)
   (heq_1 : o?✝ = some val✝) :
-  HEq
-    (match o?✝ with
+  (match o?✝ with
     | some val => h_1 ()
-    | x => h_2 x)
-    (h_1 val✝)
+    | x => h_2 x) ≍
+    h_1 val✝
 -/
 #guard_msgs(pass trace, all) in
 #check matchOptionUnit.match_1.congr_eq_1
@@ -104,11 +100,10 @@ info: utf16PosToCodepointPosFromAux.match_1.congr_eq_1.{u_1} (motive : Nat → S
   (x✝¹ : String.Pos) (x✝² : Nat) (h_1 : (x : String.Pos) → (cp : Nat) → motive 0 x cp)
   (h_2 : (utf16pos : Nat) → (utf8pos : String.Pos) → (cp : Nat) → motive utf16pos utf8pos cp) (x✝³ : String.Pos)
   (cp : Nat) (heq_1 : x✝ = 0) (heq_2 : x✝¹ = x✝³) (heq_3 : x✝² = cp) :
-  HEq
-    (match x✝, x✝¹, x✝² with
+  (match x✝, x✝¹, x✝² with
     | 0, x, cp => h_1 x cp
-    | utf16pos, utf8pos, cp => h_2 utf16pos utf8pos cp)
-    (h_1 x✝³ cp)
+    | utf16pos, utf8pos, cp => h_2 utf16pos utf8pos cp) ≍
+    h_1 x✝³ cp
 -/
 #guard_msgs(pass trace, all) in
 #check utf16PosToCodepointPosFromAux.match_1.congr_eq_1
@@ -123,12 +118,10 @@ def wrongEq (m? : Option Nat) (h : some_expr = m?)
 info: wrongEq.match_1.congr_eq_1.{u_1} (motive : (m? : Option Nat) → 0 < m?.getD 0 → some_expr = m? → Sort u_1)
   (m?✝ : Option Nat) (w✝ : 0 < m?✝.getD 0) (h : some_expr = m?✝)
   (h_1 : (m? : Nat) → (x : 0 < (some m?).getD 0) → (h : some_expr = some m?) → motive (some m?) x h) (m? : Nat)
-  (x✝ : 0 < (some m?).getD 0) (h✝ : some_expr = some m?) (heq_1 : m?✝ = some m?) (heq_2 : HEq w✝ x✝)
-  (heq_3 : HEq h h✝) :
-  HEq
-    (match m?✝, w✝, h with
-    | some m?, x, h => h_1 m? x h)
-    (h_1 m? x✝ h✝)
+  (x✝ : 0 < (some m?).getD 0) (h✝ : some_expr = some m?) (heq_1 : m?✝ = some m?) (heq_2 : w✝ ≍ x✝) (heq_3 : h ≍ h✝) :
+  (match m?✝, w✝, h with
+    | some m?, x, h => h_1 m? x h) ≍
+    h_1 m? x✝ h✝
 -/
 #guard_msgs(pass trace, all) in #check wrongEq.match_1.congr_eq_1
 
@@ -142,11 +135,10 @@ noncomputable def myNamedPatternTest (x : List Bool) : Bool :=
 info: myNamedPatternTest.match_1.congr_eq_1.{u_1} (motive : List Bool → Sort u_1) (x✝ : List Bool)
   (h_1 : (x' : List Bool) → (x : Bool) → (xs : List Bool) → x' = x :: xs → x✝ = x :: xs → motive (x :: xs))
   (h_2 : (x' : List Bool) → x✝ = x' → motive x') (x : Bool) (xs : List Bool) (heq_1 : x✝ = x :: xs) :
-  HEq
-    (match hx : x✝ with
+  (match hx : x✝ with
     | x'@hx':(x :: xs) => h_1 x' x xs hx' hx
-    | x' => h_2 x' hx)
-    (h_1 (x :: xs) x xs ⋯ heq_1)
+    | x' => h_2 x' hx) ≍
+    h_1 (x :: xs) x xs ⋯ heq_1
 -/
 #guard_msgs(pass trace, all) in
 #check myNamedPatternTest.match_1.congr_eq_1
@@ -161,11 +153,10 @@ def testMe (n : Nat) : Bool :=
 info: testMe.match_1.congr_eq_2.{u_1} (motive : Nat → Sort u_1) (x✝ : Nat) (h_1 : x✝ = 0 → motive 0)
   (h_2 : (m : Nat) → x✝ = m → motive m) (m : Nat) (heq_1 : x✝ = m) :
   (m = 0 → False) →
-    HEq
-      (match h : x✝ with
+    (match h : x✝ with
       | 0 => h_1 h
-      | m => h_2 m h)
-      (h_2 m heq_1)
+      | m => h_2 m h) ≍
+      h_2 m heq_1
 -/
 #guard_msgs(pass trace, all) in
 #check testMe.match_1.congr_eq_2

tests/lean/run/multiTargetCasesInductionIssue.lean

@@ -50,7 +50,7 @@ as✝ : Vec α n✝
 n : Nat
 a : α
 as : Vec α n
-ih : n + 1 = n → HEq (Vec.cons a as) as → Vec.cons a as = Vec.cons a as
+ih : n + 1 = n → Vec.cons a as ≍ as → Vec.cons a as = Vec.cons a as
 ⊢ Vec.cons a as = Vec.cons a as
 -/
 #guard_msgs in
@@ -70,8 +70,8 @@ n' : Nat
 a' : α
 as' : Vec α n'
 h₁ : n + 2 = n' + 1
-h₂ : HEq (Vec.cons a (Vec.cons a as)) (Vec.cons a' as')
-ih : n' + 1 = n' → HEq (Vec.cons a' as') as' → Vec.cons a' as' = Vec.cons a' as'
+h₂ : Vec.cons a (Vec.cons a as) ≍ Vec.cons a' as'
+ih : n' + 1 = n' → Vec.cons a' as' ≍ as' → Vec.cons a' as' = Vec.cons a' as'
 ⊢ Vec.cons a' as' = Vec.cons a' as'
 -/
 #guard_msgs in

tests/lean/run/rflTacticErrors.lean

@@ -207,8 +207,8 @@ with the goal
   @HEq Bool true'' Bool true
 
 Note: The full type of 'HEq.refl' is
-  ∀ {α : Sort _} (a : α), HEq a a
-⊢ HEq true'' true
+  ∀ {α : Sort _} (a : α), a ≍ a
+⊢ true'' ≍ true
 -/
 #guard_msgs in
 example : HEq true'' true := by with_reducible apply_rfl -- Error
@@ -270,13 +270,13 @@ is not definitionally equal to the right-hand side
 example : false = true   := by apply_rfl -- Error
 /--
 error: tactic 'apply' failed, could not unify the conclusion of 'HEq.refl'
-  HEq ?a ?a
+  ?a ≍ ?a
 with the goal
-  HEq false true
+  false ≍ true
 
 Note: The full type of 'HEq.refl' is
-  ∀ {α : Sort _} (a : α), HEq a a
-⊢ HEq false true
+  ∀ {α : Sort _} (a : α), a ≍ a
+⊢ false ≍ true
 -/
 #guard_msgs in
 example : HEq false true := by apply_rfl -- Error
@@ -337,13 +337,13 @@ is not definitionally equal to the right-hand side
 example : false = true   := by with_reducible apply_rfl -- Error
 /--
 error: tactic 'apply' failed, could not unify the conclusion of 'HEq.refl'
-  HEq ?a ?a
+  ?a ≍ ?a
 with the goal
-  HEq false true
+  false ≍ true
 
 Note: The full type of 'HEq.refl' is
-  ∀ {α : Sort _} (a : α), HEq a a
-⊢ HEq false true
+  ∀ {α : Sort _} (a : α), a ≍ a
+⊢ false ≍ true
 -/
 #guard_msgs in
 example : HEq false true := by with_reducible apply_rfl -- Error
@@ -397,25 +397,25 @@ example : R false true   := by with_reducible apply_rfl -- Error
 
 /--
 error: tactic 'apply' failed, could not unify the conclusion of 'HEq.refl'
-  HEq ?a ?a
+  ?a ≍ ?a
 with the goal
-  HEq true 1
+  true ≍ 1
 
 Note: The full type of 'HEq.refl' is
-  ∀ {α : Sort _} (a : α), HEq a a
-⊢ HEq true 1
+  ∀ {α : Sort _} (a : α), a ≍ a
+⊢ true ≍ 1
 -/
 #guard_msgs in
 example : HEq true 1 := by apply_rfl -- Error
 /--
 error: tactic 'apply' failed, could not unify the conclusion of 'HEq.refl'
-  HEq ?a ?a
+  ?a ≍ ?a
 with the goal
-  HEq true 1
+  true ≍ 1
 
 Note: The full type of 'HEq.refl' is
-  ∀ {α : Sort _} (a : α), HEq a a
-⊢ HEq true 1
+  ∀ {α : Sort _} (a : α), a ≍ a
+⊢ true ≍ 1
 -/
 #guard_msgs in
 example : HEq true 1 := by with_reducible apply_rfl -- Error