Update tests

Author: nomeata

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