chore: post-stage0 update fixes

Author: nomeata

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,31 +99,31 @@ 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.
 -/
 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,32 +2943,32 @@ 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.
 -/
 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.
 -/
 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