fix

leanprover · Jul 28, 2024 · c73ab6f · c73ab6f
1 parent 8d1b1ce
commit c73ab6f
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 4 deletions.
diff --git a/src/Init/Data/Subtype.lean b/src/Init/Data/Subtype.lean
@@ -9,7 +9,7 @@ import Init.Ext
 namespace Subtype
 
 universe u
-variable {α : Type u} {p q : α → Prop}
+variable {α : Sort u} {p q : α → Prop}
 
 @[ext]
 protected theorem ext : ∀ {a1 a2 : { x // p x }}, (a1 : α) = (a2 : α) → a1 = a2

diff --git a/tests/lean/run/binop_binrel_perf_issue.lean b/tests/lean/run/binop_binrel_perf_issue.lean
@@ -58,9 +58,6 @@ section Mathlib.Data.Subtype
 
 variable {α : Sort _} {p : α → Prop}
 
-protected theorem Subtype.ext : ∀ {a1 a2 : { x // p x }}, (a1 : α) = (a2 : α) → a1 = a2
-  | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
-
 theorem Subtype.coe_injective : Function.Injective (fun (a : Subtype p) ↦ (a : α)) := fun _ _ ↦ Subtype.ext
 
 end Mathlib.Data.Subtype