chore: post-stage0 update fixes

src/Init/Core.lean

@@ -939,9 +939,7 @@ theorem HEq.subst {p : (T : Sort u) → T → Prop} (h₁ : a ≍ b) (h₂ : p
 @[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') : a ≍ a' :=
-  Eq.subst h (HEq.refl a)
+
 
 /-- Heterogeneous equality is transitive. -/
 theorem HEq.trans (h₁ : a ≍ b) (h₂ : b ≍ c) : a ≍ c :=
@@ -1370,7 +1368,7 @@ instance {α : Type u} {p : α → Prop} [BEq α] [LawfulBEq α] : LawfulBEq {x
 instance {α : Sort u} {p : α → Prop} [DecidableEq α] : DecidableEq {x : α // p x} :=
   fun ⟨a, h₁⟩ ⟨b, h₂⟩ =>
     if h : a = b then isTrue (by subst h; exact rfl)
-    else isFalse (fun h' => Subtype.noConfusion h' (fun h' => absurd h' h))
+    else isFalse (fun h' => Subtype.noConfusion rfl .rfl (heq_of_eq h') (fun h' => absurd (eq_of_heq h') h))
 
 end Subtype
 
@@ -1429,8 +1427,8 @@ instance [DecidableEq α] [DecidableEq β] : DecidableEq (α × β) :=
     | isTrue e₁ =>
       match decEq b b' with
       | isTrue e₂  => isTrue (e₁ ▸ e₂ ▸ rfl)
-      | isFalse n₂ => isFalse fun h => Prod.noConfusion h fun _   e₂' => absurd e₂' n₂
-    | isFalse n₁ => isFalse fun h => Prod.noConfusion h fun e₁' _   => absurd e₁' n₁
+      | isFalse n₂ => isFalse fun h => Prod.noConfusion rfl rfl (heq_of_eq h) fun _   e₂' => absurd (eq_of_heq e₂') n₂
+    | isFalse n₁ => isFalse fun h => Prod.noConfusion rfl rfl (heq_of_eq h) fun e₁' _   => absurd (eq_of_heq e₁') n₁
 
 instance [BEq α] [BEq β] : BEq (α × β) where
   beq := fun (a₁, b₁) (a₂, b₂) => a₁ == a₂ && b₁ == b₂

src/Init/Data/Array/DecidableEq.lean

@@ -99,23 +99,23 @@ instance instDecidableEq [DecidableEq α] : DecidableEq (Array α) := fun xs ys
   | ⟨[]⟩ =>
     match ys with
     | ⟨[]⟩ => isTrue rfl
-    | ⟨_ :: _⟩ => isFalse (Array.noConfusion · (List.noConfusion ·))
+    | ⟨_ :: _⟩ => isFalse (fun h => Array.noConfusion rfl (heq_of_eq h) (fun h => List.noConfusion rfl h))
   | ⟨a :: as⟩ =>
     match ys with
-    | ⟨[]⟩ => isFalse (Array.noConfusion · (List.noConfusion ·))
+    | ⟨[]⟩ => isFalse (fun h => Array.noConfusion rfl (heq_of_eq h) (fun h => List.noConfusion rfl h))
     | ⟨b :: bs⟩ => instDecidableEqImpl ⟨a :: as⟩ ⟨b :: bs⟩
 
 @[csimp]
 theorem instDecidableEq_csimp : @instDecidableEq = @instDecidableEqImpl :=
   Subsingleton.allEq _ _
-  
+
 /--
 Equality with `#[]` is decidable even if the underlying type does not have decidable equality.
 -/
 instance instDecidableEqEmp (xs : Array α) : Decidable (xs = #[]) :=
   match xs with
   | ⟨[]⟩ => isTrue rfl
-  | ⟨_ :: _⟩ => isFalse (Array.noConfusion · (List.noConfusion ·))
+  | ⟨_ :: _⟩ => isFalse (fun h => Array.noConfusion rfl (heq_of_eq h) (fun h => List.noConfusion rfl h))
 
 /--
 Equality with `#[]` is decidable even if the underlying type does not have decidable equality.
@@ -123,7 +123,7 @@ Equality with `#[]` is decidable even if the underlying type does not have decid
 instance instDecidableEmpEq (ys : Array α) : Decidable (#[] = ys) :=
   match ys with
   | ⟨[]⟩ => isTrue rfl
-  | ⟨_ :: _⟩ => isFalse (Array.noConfusion · (List.noConfusion ·))
+  | ⟨_ :: _⟩ => isFalse (fun h => Array.noConfusion rfl (heq_of_eq h) (fun h => List.noConfusion rfl h))
 
 theorem beq_eq_decide [BEq α] (xs ys : Array α) :
     (xs == ys) = if h : xs.size = ys.size then

src/Init/Data/List/Basic.lean

@@ -301,7 +301,7 @@ Examples:
 def getLast : ∀ (as : List α), as ≠ [] → α
   | [],       h => absurd rfl h
   | [a],      _ => a
-  | _::b::as, _ => getLast (b::as) (fun h => List.noConfusion h)
+  | _::b::as, _ => getLast (b::as) (fun h => List.noConfusion rfl (heq_of_eq h))
 
 /-! ### getLast? -/
 
@@ -318,7 +318,7 @@ Examples:
 -/
 def getLast? : List α → Option α
   | []    => none
-  | a::as => some (getLast (a::as) (fun h => List.noConfusion h))
+  | a::as => some (getLast (a::as) (fun h => List.noConfusion rfl (heq_of_eq h)))
 
 @[simp, grind =] theorem getLast?_nil : @getLast? α [] = none := rfl
 
@@ -337,7 +337,7 @@ Examples:
 -/
 def getLastD : (as : List α) → (fallback : α) → α
   | [],   a₀ => a₀
-  | a::as, _ => getLast (a::as) (fun h => List.noConfusion h)
+  | a::as, _ => getLast (a::as) (fun h => List.noConfusion rfl (heq_of_eq h))
 
 -- These aren't `simp` lemmas since we always simplify `getLastD` in terms of `getLast?`.
 theorem getLastD_nil {a : α} : getLastD [] a = a := rfl

src/Init/Data/List/BasicAux.lean

@@ -57,7 +57,7 @@ Examples:
 @[expose]
 def getLast! [Inhabited α] : List α → α
   | []    => panic! "empty list"
-  | a::as => getLast (a::as) (fun h => List.noConfusion h)
+  | a::as => getLast (a::as) (fun h => List.noConfusion rfl (heq_of_eq h))
 
 /-! ## Head and tail -/
 

src/Init/Data/Option/Basic.lean

@@ -22,12 +22,12 @@ instance instDecidableEq {α} [inst : DecidableEq α] : DecidableEq (Option α)
   match a with
   | none => match b with
     | none => .isTrue rfl
-    | some _ => .isFalse Option.noConfusion
+    | some _ => .isFalse (fun h => Option.noConfusion rfl (heq_of_eq h))
   | some a => match b with
-    | none => .isFalse Option.noConfusion
+    | none => .isFalse (fun h => Option.noConfusion rfl (heq_of_eq h))
     | some b => match inst a b with
       | .isTrue h => .isTrue (h ▸ rfl)
-      | .isFalse n => .isFalse (Option.noConfusion · n)
+      | .isFalse n => .isFalse (fun h => Option.noConfusion rfl (heq_of_eq h) (fun h' => absurd (eq_of_heq h') n))
 
 /--
 Equality with `none` is decidable even if the wrapped type does not have decidable equality.
@@ -37,7 +37,7 @@ instance decidableEqNone (o : Option α) : Decidable (o = none) :=
     compatibility with the `DecidableEq` instance. -/
   match o with
   | none => .isTrue rfl
-  | some _ => .isFalse Option.noConfusion
+  | some _ => .isFalse (fun h => Option.noConfusion rfl (heq_of_eq h))
 
 /--
 Equality with `none` is decidable even if the wrapped type does not have decidable equality.
@@ -47,7 +47,7 @@ instance decidableNoneEq (o : Option α) : Decidable (none = o) :=
     compatibility with the `DecidableEq` instance. -/
   match o with
   | none => .isTrue rfl
-  | some _ => .isFalse Option.noConfusion
+  | some _ => .isFalse (fun h => Option.noConfusion rfl (heq_of_eq h))
 
 deriving instance BEq for Option
 

src/Init/Data/Option/Instances.lean

@@ -16,9 +16,9 @@ namespace Option
 
 theorem eq_of_eq_some {α : Type u} : ∀ {x y : Option α}, (∀ z, x = some z ↔ y = some z) → x = y
   | none,   none,   _ => rfl
-  | none,   some z, h => Option.noConfusion ((h z).2 rfl)
-  | some z, none,   h => Option.noConfusion ((h z).1 rfl)
-  | some _, some w, h => Option.noConfusion ((h w).2 rfl) (congrArg some)
+  | none,   some z, h => Option.noConfusion rfl (heq_of_eq ((h z).2 rfl))
+  | some z, none,   h => Option.noConfusion rfl (heq_of_eq ((h z).1 rfl))
+  | some _, some w, h => Option.noConfusion rfl (heq_of_eq ((h w).2 rfl)) (fun h => congrArg some (eq_of_heq h))
 
 theorem eq_none_of_isNone {α : Type u} : ∀ {o : Option α}, o.isNone → o = none
   | none, _ => rfl

src/Init/Prelude.lean

@@ -496,6 +496,10 @@ theorem eq_of_heq {α : Sort u} {a a' : α} (h : HEq a a') : Eq a a' :=
       h₁.rec (fun _ => rfl)
   this α α a a' h rfl
 
+/-- Propositionally equal terms are also heterogeneously equal. -/
+theorem heq_of_eq (h : Eq a a') : HEq a a' :=
+  Eq.subst h (HEq.refl a)
+
 /--
 The product type, usually written `α × β`. Product types are also called pair or tuple types.
 Elements of this type are pairs in which the first element is an `α` and the second element is a
@@ -2330,7 +2334,7 @@ def BitVec.decEq (x y : BitVec w) : Decidable (Eq x y) :=
   | ⟨n⟩, ⟨m⟩ =>
     dite (Eq n m)
       (fun h => isTrue (h ▸ rfl))
-      (fun h => isFalse (fun h' => BitVec.noConfusion h' (fun h' => absurd h' h)))
+      (fun h => isFalse (fun h' => BitVec.noConfusion rfl (heq_of_eq h') (fun h' => absurd (eq_of_heq h') h)))
 
 instance : DecidableEq (BitVec w) := BitVec.decEq
 
@@ -2921,15 +2925,15 @@ instance {α} : Inhabited (List α) where
 /-- Implements decidable equality for `List α`, assuming `α` has decidable equality. -/
 protected def List.hasDecEq {α : Type u} [DecidableEq α] : (a b : List α) → Decidable (Eq a b)
   | nil,       nil       => isTrue rfl
-  | cons _ _, nil        => isFalse (fun h => List.noConfusion h)
-  | nil,       cons _ _  => isFalse (fun h => List.noConfusion h)
+  | cons _ _, nil        => isFalse (fun h => List.noConfusion rfl (heq_of_eq h))
+  | nil,       cons _ _  => isFalse (fun h => List.noConfusion rfl (heq_of_eq h))
   | cons a as, cons b bs =>
     match decEq a b with
     | isTrue hab  =>
       match List.hasDecEq as bs with
       | isTrue habs  => isTrue (hab ▸ habs ▸ rfl)
-      | isFalse nabs => isFalse (fun h => List.noConfusion h (fun _ habs => absurd habs nabs))
-    | isFalse nab => isFalse (fun h => List.noConfusion h (fun hab _ => absurd hab nab))
+      | isFalse nabs => isFalse (fun h => List.noConfusion rfl (heq_of_eq h) (fun _ habs => absurd (eq_of_heq habs) nabs))
+    | isFalse nab => isFalse (fun h => List.noConfusion rfl (heq_of_eq h) (fun hab _ => absurd (eq_of_heq hab)   nab))
 
 instance {α : Type u} [DecidableEq α] : DecidableEq (List α) := fun xs ys =>
   /-
@@ -2939,16 +2943,16 @@ instance {α : Type u} [DecidableEq α] : DecidableEq (List α) := fun xs ys =>
   match xs with
   | .nil => match ys with
     | .nil => isTrue rfl
-    | .cons _ _ => isFalse List.noConfusion
+    | .cons _ _ => isFalse (fun h => List.noConfusion rfl (heq_of_eq h))
   | .cons a as => match ys with
-    | .nil => isFalse List.noConfusion
+    | .nil => isFalse (fun h => List.noConfusion rfl (heq_of_eq h))
     | .cons b bs =>
       match decEq a b with
       | isTrue hab =>
         match List.hasDecEq as bs with
         | isTrue habs  => isTrue (hab ▸ habs ▸ rfl)
-        | isFalse nabs => isFalse (List.noConfusion · (fun _ habs => absurd habs nabs))
-      | isFalse nab => isFalse (List.noConfusion · (fun hab _ => absurd hab nab))
+        | isFalse nabs => isFalse (fun h => List.noConfusion rfl (heq_of_eq h) (fun _ habs => absurd (eq_of_heq habs) nabs))
+      | isFalse nab => isFalse (fun h => List.noConfusion rfl (heq_of_eq h) (fun hab _ => absurd (eq_of_heq hab)   nab))
 
 /--
 Equality with `List.nil` is decidable even if the underlying type does not have decidable equality.
@@ -2956,7 +2960,7 @@ Equality with `List.nil` is decidable even if the underlying type does not have
 instance List.instDecidableNilEq (a : List α) : Decidable (Eq List.nil a) :=
   match a with
   | .nil => isTrue rfl
-  | .cons _ _ => isFalse List.noConfusion
+  | .cons _ _ => isFalse (fun h => List.noConfusion rfl (heq_of_eq h))
 
 /--
 Equality with `List.nil` is decidable even if the underlying type does not have decidable equality.
@@ -2964,7 +2968,7 @@ Equality with `List.nil` is decidable even if the underlying type does not have
 instance List.instDecidableEqNil (a : List α) : Decidable (Eq a List.nil) :=
   match a with
   | .nil => isTrue rfl
-  | .cons _ _ => isFalse List.noConfusion
+  | .cons _ _ => isFalse (fun h => List.noConfusion rfl (heq_of_eq h))
 
 /--
 The length of a list.

tests/lean/run/6123_mod_cast.lean

@@ -142,7 +142,7 @@ theorem coe_le_coe : (a : WithBot α) ≤ b ↔ a ≤ b := by
   simp [LE.le]
 
 instance orderBot : OrderBot (WithBot α) where
-  bot_le _ := fun _ h => Option.noConfusion h
+  bot_le _ := fun _ h => Option.noConfusion rfl (heq_of_eq h)
 
 theorem le_coe_iff : ∀ {x : WithBot α}, x ≤ b ↔ ∀ a : α, x = ↑a → a ≤ b
   | (b : α) => by simp

tests/lean/run/concatElim.lean

@@ -20,7 +20,7 @@ theorem concatEq (xs : List α) (h : xs ≠ []) : concat (dropLast xs) (last xs
   match xs, h with
   | [],  h        => contradiction
   | [x], h        => rfl
-  | x₁::x₂::xs, h => simp [concat, dropLast, last, concatEq (x₂::xs) List.noConfusion]
+  | x₁::x₂::xs, h => simp [concat, dropLast, last, concatEq (x₂::xs)]
 
 theorem lengthCons {α} (x : α) (xs : List α) : (x::xs).length = xs.length + 1 :=
   rfl
@@ -42,11 +42,11 @@ theorem dropLastLen {α} (xs : List α) : (n : Nat) → xs.length = n+1 → (dro
     intro n h
     cases n with
     | zero   =>
-      simp [lengthCons] at h
+      simp at h
     | succ n =>
-      have : (x₁ :: x₂ :: xs).length = xs.length + 2 := by simp [lengthCons]
+      have : (x₁ :: x₂ :: xs).length = xs.length + 2 := by simp
       have : xs.length = n := by rw [this] at h; injection h with h; injection h
-      simp [dropLast, lengthCons, dropLastLen (x₂::xs) xs.length (lengthCons ..), this]
+      simp [dropLast, dropLastLen (x₂::xs) xs.length (lengthCons ..), this]
 
 @[inline]
 def concatElim {α}

tests/lean/run/hinj_thm.lean

@@ -8,15 +8,22 @@ inductive Foo' (α β : Type u) : (n : Nat) → P n -> Type u
   | odd  (b : β) (n : Nat) (v : T n) : Foo' α β (Nat.succ (double n)) (pax _)
 
 /--
-info: Foo'.even.hinj.{u} {α β : Type u} {a : α} {n : Nat} {v : T n} {h : P n} {a✝ : α} {n✝ : Nat} {v✝ : T n✝} {h✝ : P n✝} :
-  double n = double n✝ → ⋯ ≍ ⋯ → Foo'.even a n v h ≍ Foo'.even a✝ n✝ v✝ h✝ → a = a✝ ∧ n = n✝ ∧ v ≍ v✝
+info: Foo'.even.hinj.{u} {α β : Type u} {a : α} {n : Nat} {v : T n} {h : P n} {α✝ β✝ : Type u} {a✝ : α✝} {n✝ : Nat}
+  {v✝ : T n✝} {h✝ : P n✝} :
+  α = α✝ →
+    β = β✝ →
+      double n = double n✝ →
+        ⋯ ≍ ⋯ → Foo'.even a n v h ≍ Foo'.even a✝ n✝ v✝ h✝ → α = α✝ ∧ β = β✝ ∧ a ≍ a✝ ∧ n = n✝ ∧ v ≍ v✝
 -/
 #guard_msgs in
 #check Foo'.even.hinj
 
 /--
-info: Foo'.odd.hinj.{u} {α β : Type u} {b : β} {n : Nat} {v : T n} {b✝ : β} {n✝ : Nat} {v✝ : T n✝} :
-  (double n).succ = (double n✝).succ → ⋯ ≍ ⋯ → Foo'.odd b n v ≍ Foo'.odd b✝ n✝ v✝ → b = b✝ ∧ n = n✝ ∧ v ≍ v✝
+info: Foo'.odd.hinj.{u} {α β : Type u} {b : β} {n : Nat} {v : T n} {α✝ β✝ : Type u} {b✝ : β✝} {n✝ : Nat} {v✝ : T n✝} :
+  α = α✝ →
+    β = β✝ →
+      (double n).succ = (double n✝).succ →
+        ⋯ ≍ ⋯ → Foo'.odd b n v ≍ Foo'.odd b✝ n✝ v✝ → α = α✝ ∧ β = β✝ ∧ b ≍ b✝ ∧ n = n✝ ∧ v ≍ v✝
 -/
 #guard_msgs in
 #check Foo'.odd.hinj

tests/lean/run/issue11450.lean

@@ -17,7 +17,7 @@ inductive Term (L: Nat → Type) (n : Nat) : Nat → Type _
 
 /--
 info: @[reducible] def Term.var.noConfusion.{u} : {L : Nat → Type} →
-  {n : Nat} → {P : Sort u} → {k k' : Fin n} → Term.var k = Term.var k' → (k = k' → P) → P
+  {n : Nat} → {P : Sort u} → {k k' : Fin n} → Term.var k = Term.var k' → (k ≍ k' → P) → P
 -/
 #guard_msgs in
 #print sig Term.var.noConfusion
@@ -44,7 +44,7 @@ inductive Vec (α : Type u) : Nat → Type u where
 /--
 info: Vec.cons.noConfusion.{u_1, u} {α : Type u} {P : Sort u_1} {n : Nat} {x : α} {xs : Vec α n} {n' : Nat} {x' : α}
   {xs' : Vec α n'} (eq_1 : n + 1 = n' + 1) (eq_2 : Vec.cons x xs ≍ Vec.cons x' xs')
-  (k : n = n' → x = x' → xs ≍ xs' → P) : P
+  (k : n = n' → x ≍ x' → xs ≍ xs' → P) : P
 -/
 #guard_msgs in
 #check Vec.cons.noConfusion
@@ -60,11 +60,11 @@ theorem Vec.cons.hinj' {α : Type u}
   {x : α} {n : Nat} {xs : Vec α n} {x' : α} {n' : Nat} {xs' : Vec α n'} :
   Vec.cons x xs ≍ Vec.cons x' xs' → (n + 1 = n' + 1 → (x = x' ∧ xs ≍ xs')) := by
   intro h eq_1
-  apply Vec.cons.noConfusion eq_1 h (fun _ eq_x eq_xs => ⟨eq_x, eq_xs⟩)
+  apply Vec.cons.noConfusion eq_1 h (fun _ eq_x eq_xs => ⟨eq_of_heq eq_x, eq_xs⟩)
 
 /--
-info: Vec.cons.hinj.{u} {α : Type u} {n : Nat} {x : α} {xs : Vec α n} {n✝ : Nat} {x✝ : α} {xs✝ : Vec α n✝} :
-  n + 1 = n✝ + 1 → Vec.cons x xs ≍ Vec.cons x✝ xs✝ → n = n✝ ∧ x = x✝ ∧ xs ≍ xs✝
+info: Vec.cons.hinj.{u} {α : Type u} {n : Nat} {x : α} {xs : Vec α n} {α✝ : Type u} {n✝ : Nat} {x✝ : α✝} {xs✝ : Vec α✝ n✝} :
+  α = α✝ → n + 1 = n✝ + 1 → Vec.cons x xs ≍ Vec.cons x✝ xs✝ → α = α✝ ∧ n = n✝ ∧ x ≍ x✝ ∧ xs ≍ xs✝
 -/
 #guard_msgs in
 #check Vec.cons.hinj

tests/lean/run/issue11560.lean

@@ -9,7 +9,7 @@ example
  (h2 : d.succ < b)
  (hab : a = b)
  (hcd : @Fin'.mk a c.succ h1 ≍ @Fin'.mk b d.succ h2) :
- c = d := Fin'.mk.noConfusion hab hcd (fun h => Nat.succ.noConfusion h fun h' => h')
+ c = d := Fin'.noConfusion hab hcd (fun h => Nat.succ.noConfusion h fun h' => h')
 
 example
  (a b c d : Nat)

tests/lean/run/linearNoConfusion.lean

@@ -20,30 +20,31 @@ inductive Vec.{u} (α : Type) : Nat → Type u where
   | cons1 {n} : α → Vec α n → Vec α (n + 1)
   | cons2 {n} : α → Vec α n → Vec α (n + 1)
 
-@[reducible] protected def Vec.noConfusionType'.{u_1, u} : {α : Type} →
-  Sort u_1 → {a : Nat} → Vec.{u} α a → {a : Nat} → Vec α a → Sort u_1 :=
-fun P _ x1 _ x2 =>
+@[reducible] protected def Vec.noConfusionType'.{u_1, u} : Sort u_1 →
+  {α : Type} → {a : Nat} → Vec.{u} α a →
+  {α : Type} → {a : Nat} → Vec α a → Sort u_1 :=
+fun P _ _ x1 _ _ x2 =>
   Vec.casesOn x1
     (if h : x2.ctorIdx = 0 then
       Vec.nil.elim (motive := fun _ _ => Sort u_1) x2 h (P → P)
     else P)
     (fun {n} a_1 a_2 => if h : x2.ctorIdx = 1 then
-      Vec.cons1.elim (motive := fun _ _ => Sort u_1) x2 h fun {n_1} a a_3 => (n = n_1 → a_1 = a → a_2 ≍ a_3 → P) → P
+      Vec.cons1.elim (motive := fun _ _ => Sort u_1) x2 h fun {n_1} a a_3 => (n = n_1 → a_1 ≍ a → a_2 ≍ a_3 → P) → P
      else P)
     (fun {n} a_1 a_2 => if h : x2.ctorIdx = 2 then
-      Vec.cons2.elim (motive := fun _ _ => Sort u_1) x2 h fun {n_1} a a_3 => (n = n_1 → a_1 = a → a_2 ≍ a_3 → P) → P
+      Vec.cons2.elim (motive := fun _ _ => Sort u_1) x2 h fun {n_1} a a_3 => (n = n_1 → a_1 ≍ a → a_2 ≍ a_3 → P) → P
      else P)
 
 /--
-info: @[reducible] protected def Vec.noConfusionType.{u_1, u} : {α : Type} →
-  Sort u_1 → {a : Nat} → Vec α a → {a' : Nat} → Vec α a' → Sort u_1 :=
-fun {α} P {a} t {a'} t' =>
+info: @[reducible] protected def Vec.noConfusionType.{u_1, u} : Sort u_1 →
+  {α : Type} → {a : Nat} → Vec α a → {α' : Type} → {a' : Nat} → Vec α' a' → Sort u_1 :=
+fun P {α} {a} t {α'} {a'} t' =>
   Vec.casesOn t (if h : t'.ctorIdx = 0 then Vec.nil.elim t' h (P → P) else P)
     (fun {n} a a_1 =>
-      if h : t'.ctorIdx = 1 then Vec.cons1.elim t' h fun {n_1} a_2 a_3 => (n = n_1 → a = a_2 → a_1 ≍ a_3 → P) → P
+      if h : t'.ctorIdx = 1 then Vec.cons1.elim t' h fun {n_1} a_2 a_3 => (n = n_1 → a ≍ a_2 → a_1 ≍ a_3 → P) → P
       else P)
     fun {n} a a_1 =>
-    if h : t'.ctorIdx = 2 then Vec.cons2.elim t' h fun {n_1} a_2 a_3 => (n = n_1 → a = a_2 → a_1 ≍ a_3 → P) → P else P
+    if h : t'.ctorIdx = 2 then Vec.cons2.elim t' h fun {n_1} a_2 a_3 => (n = n_1 → a ≍ a_2 → a_1 ≍ a_3 → P) → P else P
 -/
 #guard_msgs in
 #print Vec.noConfusionType

tests/lean/run/listDecEq.lean

@@ -31,15 +31,15 @@ end
 -- List decidable equality using `withPtrEqDecEq`
 def listDecEqAux {α} [s : DecidableEq α] : ∀ (as bs : List α), Decidable (as = bs)
 | [],    []    => isTrue rfl
-| [],    b::bs => isFalse $ fun h => List.noConfusion h
-| a::as, []    => isFalse $ fun h => List.noConfusion h
+| [],    b::bs => isFalse $ fun h => List.noConfusion rfl (heq_of_eq h)
+| a::as, []    => isFalse $ fun h => List.noConfusion rfl (heq_of_eq h)
 | a::as, b::bs =>
   match s a b with
   | isTrue h₁  =>
     match withPtrEqDecEq as bs (fun _ => listDecEqAux as bs) with
     | isTrue h₂  => isTrue $ h₁ ▸ h₂ ▸ rfl
-    | isFalse h₂ => isFalse $ fun h => List.noConfusion h $ fun _ h₃ => absurd h₃ h₂
-  | isFalse h₁ => isFalse $ fun h => List.noConfusion h $ fun h₂ _ => absurd h₂ h₁
+    | isFalse h₂ => isFalse $ fun h => List.noConfusion rfl (heq_of_eq h) (fun _ h₃ => absurd (eq_of_heq h₃) h₂)
+  | isFalse h₁ => isFalse $ fun h => List.noConfusion rfl (heq_of_eq h) (fun h₂ _ => absurd (eq_of_heq h₂) h₁)
 
 instance List.optimizedDecEq {α} [DecidableEq α] : DecidableEq (List α) :=
 fun a b => withPtrEqDecEq a b (fun _ => listDecEqAux a b)

tests/lean/run/noConfusionCtorInjection.lean

@@ -6,8 +6,7 @@ inductive L (α : Type u) : Type u where
 /--
 info: theorem L.cons.inj.{u} : ∀ {α : Type u} {x : α} {xs : L α} {x_1 : α} {xs_1 : L α},
   L.cons x xs = L.cons x_1 xs_1 → x = x_1 ∧ xs = xs_1 :=
-fun {α} {x} {xs} {x_1} {xs_1} x_2 =>
-  L.cons.noConfusion (Eq.refl α) (heq_of_eq x_2) fun x_eq xs_eq => ⟨eq_of_heq x_eq, eq_of_heq xs_eq⟩
+fun {α} {x} {xs} {x_1} {xs_1} x_2 => L.cons.noConfusion x_2 fun x_eq xs_eq => ⟨eq_of_heq x_eq, eq_of_heq xs_eq⟩
 -/
 #guard_msgs in
 #print L.cons.inj
@@ -21,8 +20,7 @@ theorem ex1 (h : L.cons x xs = L.cons y ys) : x = y ∧ xs = ys := by
 /--
 info: theorem ex1.{u_1} : ∀ {α : Type u_1} {x : α} {xs : L α} {y : α} {ys : L α},
   L.cons x xs = L.cons y ys → x = y ∧ xs = ys :=
-fun {α} {x} {xs} {y} {ys} h =>
-  L.cons.noConfusion (Eq.refl α) (heq_of_eq h) fun x_eq xs_eq => ⟨eq_of_heq x_eq, eq_of_heq xs_eq⟩
+fun {α} {x} {xs} {y} {ys} h => L.cons.noConfusion h fun x_eq xs_eq => ⟨eq_of_heq x_eq, eq_of_heq xs_eq⟩
 -/
 #guard_msgs in #print ex1