chore: fix universe in PSigma.exists (#4862)

leanprover · Jul 29, 2024 · a845a00 · a845a00
1 parent abf4206
commit a845a00
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Init/Core.lean b/src/Init/Core.lean
@@ -1204,7 +1204,7 @@ def Prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂
 
 /-! # Dependent products -/
 
-theorem PSigma.exists {α : Type u} {p : α → Prop} : (PSigma (fun x => p x)) → Exists (fun x => p x)
+theorem PSigma.exists {α : Sort u} {p : α → Prop} : (PSigma (fun x => p x)) → Exists (fun x => p x)
   | ⟨x, hx⟩ => ⟨x, hx⟩
 
 @[deprecated PSigma.exists (since := "2024-07-27")]