chore: avoid automatically generated instance names (#12270)

leanprover-community · Apr 19, 2024 · 47e1ef4 · 47e1ef4
1 parent e8ccef9
commit 47e1ef4
Show file tree

Hide file tree

Showing 8 changed files with 13 additions and 13 deletions.
diff --git a/Mathlib/Algebra/Group/Conj.lean b/Mathlib/Algebra/Group/Conj.lean
@@ -244,7 +244,7 @@ the instance priority should be even lower, see Note [lower instance priority].
 
 -- see Note [slow-failing instance priority]
 instance (priority := 900) [DecidableRel (IsConj : α → α → Prop)] : DecidableEq (ConjClasses α) :=
-  instDecidableEqQuotient
+  inferInstanceAs <| DecidableEq <| Quotient (IsConj.setoid α)
 
 end Monoid
 

diff --git a/Mathlib/Data/Finset/Sym.lean b/Mathlib/Data/Finset/Sym.lean
@@ -168,7 +168,8 @@ section Sym
 variable {n : ℕ}
 
 -- Porting note: instance needed
-instance : DecidableEq (Sym α n) := Subtype.instDecidableEqSubtype
+instance : DecidableEq (Sym α n) :=
+  inferInstanceAs <| DecidableEq <| Subtype _
 
 /-- Lifts a finset to `Sym α n`. `s.sym n` is the finset of all unordered tuples of cardinality `n`
 with elements in `s`. -/

diff --git a/Mathlib/Data/Matrix/Basic.lean b/Mathlib/Data/Matrix/Basic.lean
@@ -175,9 +175,7 @@ def conjTranspose [Star α] (M : Matrix m n α) : Matrix n m α :=
 scoped postfix:1024 "ᴴ" => Matrix.conjTranspose
 
 instance inhabited [Inhabited α] : Inhabited (Matrix m n α) :=
-  -- Porting note: this instance was called `Pi.inhabited` in lean3-core, which is much
-  -- nicer than the name `instInhabitedForAll_1` it got in lean4-core...
-  instInhabitedForAll_1 _
+  inferInstanceAs <| Inhabited <| m → n → α
 
 -- Porting note: new, Lean3 found this automatically
 instance decidableEq [DecidableEq α] [Fintype m] [Fintype n] : DecidableEq (Matrix m n α) :=
@@ -226,8 +224,7 @@ instance unique [Unique α] : Unique (Matrix m n α) :=
   Pi.unique
 
 instance subsingleton [Subsingleton α] : Subsingleton (Matrix m n α) :=
-  instSubsingletonForAll
--- Porting note: this instance was `Pi.subsingleton` in lean3-core
+  inferInstanceAs <| Subsingleton <| m → n → α
 
 instance nonempty [Nonempty m] [Nonempty n] [Nontrivial α] : Nontrivial (Matrix m n α) :=
   Function.nontrivial

diff --git a/Mathlib/Data/Matrix/DMatrix.lean b/Mathlib/Data/Matrix/DMatrix.lean
@@ -115,7 +115,7 @@ instance [∀ i j, Unique (α i j)] : Unique (DMatrix m n α) :=
   Pi.unique
 
 instance [∀ i j, Subsingleton (α i j)] : Subsingleton (DMatrix m n α) :=
-  instSubsingletonForAll
+  inferInstanceAs <| Subsingleton <| ∀ i j, α i j
 
 @[simp]
 theorem zero_apply [∀ i j, Zero (α i j)] (i j) : (0 : DMatrix m n α) i j = 0 := rfl

diff --git a/Mathlib/Data/Sym/Basic.lean b/Mathlib/Data/Sym/Basic.lean
@@ -53,7 +53,8 @@ instance Sym.hasCoe (α : Type*) (n : ℕ) : CoeOut (Sym α n) (Multiset α) :=
 #align sym.has_coe Sym.hasCoe
 
 -- Porting note: instance needed for Data.Finset.Sym
-instance [DecidableEq α] : DecidableEq (Sym α n) := Subtype.instDecidableEqSubtype
+instance [DecidableEq α] : DecidableEq (Sym α n) :=
+  inferInstanceAs <| DecidableEq <| Subtype _
 
 /-- This is the `List.Perm` setoid lifted to `Vector`.
 

diff --git a/Mathlib/GroupTheory/SchurZassenhaus.lean b/Mathlib/GroupTheory/SchurZassenhaus.lean
@@ -122,7 +122,8 @@ theorem isComplement'_stabilizer_of_coprime {α : H.QuotientDiff}
 /-- Do not use this lemma: It is made obsolete by `exists_right_complement'_of_coprime` -/
 private theorem exists_right_complement'_of_coprime_aux (hH : Nat.Coprime (Nat.card H) H.index) :
     ∃ K : Subgroup G, IsComplement' H K :=
-  instNonempty.elim fun α => ⟨stabilizer G α, isComplement'_stabilizer_of_coprime hH⟩
+  have ne : Nonempty (QuotientDiff H) := inferInstance
+  ne.elim fun α => ⟨stabilizer G α, isComplement'_stabilizer_of_coprime hH⟩
 
 end SchurZassenhausAbelian
 

diff --git a/Mathlib/ModelTheory/Ultraproducts.lean b/Mathlib/ModelTheory/Ultraproducts.lean
@@ -162,7 +162,7 @@ theorem sentence_realize (φ : L.Sentence) :
 
 nonrec instance Product.instNonempty : Nonempty ((u : Filter α).Product M) :=
   letI : ∀ a, Inhabited (M a) := fun _ => Classical.inhabited_of_nonempty'
-  instNonempty
+  inferInstance
 #align first_order.language.ultraproduct.product.nonempty FirstOrder.Language.Ultraproduct.Product.instNonempty
 
 end Ultraproduct

diff --git a/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean b/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
@@ -168,10 +168,10 @@ instance [Nonempty β] : Nonempty (α →ᵤ β) := Pi.instNonempty
 instance [Nonempty β] : Nonempty (α →ᵤ[𝔖] β) := Pi.instNonempty
 
 instance [Subsingleton β] : Subsingleton (α →ᵤ β) :=
-  instSubsingletonForAll
+  inferInstanceAs <| Subsingleton <| α → β
 
 instance [Subsingleton β] : Subsingleton (α →ᵤ[𝔖] β) :=
-  instSubsingletonForAll
+  inferInstanceAs <| Subsingleton <| α → β
 
 /-- Reinterpret `f : α → β` as an element of `α →ᵤ β`. -/
 def UniformFun.ofFun : (α → β) ≃ (α →ᵤ β) :=