From 6b0d4e50c0bb462ad86a2d19caad477ced1ebe37 Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Tue, 24 Sep 2024 14:12:51 +1000
Subject: [PATCH] chore: update Pi instance names (#5447)

Override instance names for nonempty / inhabited / subsingleton arrows,
per
[zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Pi.20instance.20names.20in.20Lean.204.20core/near/466248246).
---
 src/Init/Core.lean    | 3 ++-
 src/Init/Prelude.lean | 6 ++++--
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index a2b97ecc67..86b8489ae6 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -1897,7 +1897,8 @@ theorem funext {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x}
   show extfunApp (Quot.mk eqv f) = extfunApp (Quot.mk eqv g)
   exact congrArg extfunApp (Quot.sound h)
 
-instance {α : Sort u} {β : α → Sort v} [∀ a, Subsingleton (β a)] : Subsingleton (∀ a, β a) where
+instance Pi.instSubsingleton {α : Sort u} {β : α → Sort v} [∀ a, Subsingleton (β a)] :
+    Subsingleton (∀ a, β a) where
   allEq f g := funext fun a => Subsingleton.elim (f a) (g a)
 
 /-! # Squash -/
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 31405ebeb5..18b3d1aa26 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -757,7 +757,8 @@ noncomputable def Classical.ofNonempty {α : Sort u} [Nonempty α] : α :=
 instance (α : Sort u) {β : Sort v} [Nonempty β] : Nonempty (α → β) :=
   Nonempty.intro fun _ => Classical.ofNonempty
 
-instance (α : Sort u) {β : α → Sort v} [(a : α) → Nonempty (β a)] : Nonempty ((a : α) → β a) :=
+instance Pi.instNonempty (α : Sort u) {β : α → Sort v} [(a : α) → Nonempty (β a)] :
+    Nonempty ((a : α) → β a) :=
   Nonempty.intro fun _ => Classical.ofNonempty
 
 instance : Inhabited (Sort u) where
@@ -766,7 +767,8 @@ instance : Inhabited (Sort u) where
 instance (α : Sort u) {β : Sort v} [Inhabited β] : Inhabited (α → β) where
   default := fun _ => default
 
-instance (α : Sort u) {β : α → Sort v} [(a : α) → Inhabited (β a)] : Inhabited ((a : α) → β a) where
+instance Pi.instInhabited (α : Sort u) {β : α → Sort v} [(a : α) → Inhabited (β a)] :
+    Inhabited ((a : α) → β a) where
   default := fun _ => default
 
 deriving instance Inhabited for Bool