chore(Data/Finsupp/Defs): rename instances (#10976)

This adds the `inst` prefix that is expected in Lean 4.

Performed using the F2 shortcut (renaming `foo` to `Finsupp.instFoo`, then deleting the redundant `Finsupp`)

All the changes to downstream files are fallout, no names have been changed there.

Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean

@@ -285,7 +285,7 @@ section
 -- accordingly
 
 instance : Preadditive (Free R C) where
-  homGroup X Y := Finsupp.addCommGroup
+  homGroup X Y := Finsupp.instAddCommGroup
   add_comp X Y Z f f' g := by
     dsimp [CategoryTheory.categoryFree]
     rw [Finsupp.sum_add_index'] <;> · simp [add_mul]

Mathlib/Algebra/MonoidAlgebra/Basic.lean

@@ -92,7 +92,7 @@ instance MonoidAlgebra.instIsCancelAdd [IsCancelAdd k] : IsCancelAdd (MonoidAlge
   inferInstanceAs (IsCancelAdd (G →₀ k))
 
 instance MonoidAlgebra.coeFun : CoeFun (MonoidAlgebra k G) fun _ => G → k :=
-  Finsupp.coeFun
+  Finsupp.instCoeFun
 #align monoid_algebra.has_coe_to_fun MonoidAlgebra.coeFun
 
 end
@@ -174,7 +174,7 @@ theorem mul_def {f g : MonoidAlgebra k G} :
 #align monoid_algebra.mul_def MonoidAlgebra.mul_def
 
 instance nonUnitalNonAssocSemiring : NonUnitalNonAssocSemiring (MonoidAlgebra k G) :=
-  { Finsupp.addCommMonoid with
+  { Finsupp.instAddCommMonoid with
     -- Porting note: `refine` & `exact` are required because `simp` behaves differently.
     left_distrib := fun f g h => by
       haveI := Classical.decEq G
@@ -307,7 +307,7 @@ instance nonUnitalCommSemiring [CommSemiring k] [CommSemigroup G] :
 #align monoid_algebra.non_unital_comm_semiring MonoidAlgebra.nonUnitalCommSemiring
 
 instance nontrivial [Semiring k] [Nontrivial k] [Nonempty G] : Nontrivial (MonoidAlgebra k G) :=
-  Finsupp.nontrivial
+  Finsupp.instNontrivial
 #align monoid_algebra.nontrivial MonoidAlgebra.nontrivial
 
 /-! #### Derived instances -/
@@ -324,7 +324,7 @@ instance unique [Semiring k] [Subsingleton k] : Unique (MonoidAlgebra k G) :=
 #align monoid_algebra.unique MonoidAlgebra.unique
 
 instance addCommGroup [Ring k] : AddCommGroup (MonoidAlgebra k G) :=
-  Finsupp.addCommGroup
+  Finsupp.instAddCommGroup
 #align monoid_algebra.add_comm_group MonoidAlgebra.addCommGroup
 
 instance nonUnitalNonAssocRing [Ring k] [Mul G] : NonUnitalNonAssocRing (MonoidAlgebra k G) :=
@@ -1223,7 +1223,7 @@ instance instIsCancelAdd [IsCancelAdd k] : IsCancelAdd (AddMonoidAlgebra k G) :=
   inferInstanceAs (IsCancelAdd (G →₀ k))
 
 instance coeFun : CoeFun k[G] fun _ => G → k :=
-  Finsupp.coeFun
+  Finsupp.instCoeFun
 #align add_monoid_algebra.has_coe_to_fun AddMonoidAlgebra.coeFun
 
 end AddMonoidAlgebra
@@ -1312,7 +1312,7 @@ theorem mul_def {f g : k[G]} :
 #align add_monoid_algebra.mul_def AddMonoidAlgebra.mul_def
 
 instance nonUnitalNonAssocSemiring : NonUnitalNonAssocSemiring k[G] :=
-  { Finsupp.addCommMonoid with
+  { Finsupp.instAddCommMonoid with
     -- Porting note: `refine` & `exact` are required because `simp` behaves differently.
     left_distrib := fun f g h => by
       haveI := Classical.decEq G
@@ -1456,7 +1456,7 @@ instance nonUnitalCommSemiring [CommSemiring k] [AddCommSemigroup G] :
 #align add_monoid_algebra.non_unital_comm_semiring AddMonoidAlgebra.nonUnitalCommSemiring
 
 instance nontrivial [Semiring k] [Nontrivial k] [Nonempty G] : Nontrivial k[G] :=
-  Finsupp.nontrivial
+  Finsupp.instNontrivial
 #align add_monoid_algebra.nontrivial AddMonoidAlgebra.nontrivial
 
 /-! #### Derived instances -/
@@ -1473,7 +1473,7 @@ instance unique [Semiring k] [Subsingleton k] : Unique k[G] :=
 #align add_monoid_algebra.unique AddMonoidAlgebra.unique
 
 instance addCommGroup [Ring k] : AddCommGroup k[G] :=
-  Finsupp.addCommGroup
+  Finsupp.instAddCommGroup
 #align add_monoid_algebra.add_comm_group AddMonoidAlgebra.addCommGroup
 
 instance nonUnitalNonAssocRing [Ring k] [Add G] : NonUnitalNonAssocRing k[G] :=

Mathlib/Data/Finsupp/Defs.lean

@@ -125,9 +125,9 @@ instance instFunLike : FunLike (α →₀ M) α M :=
 
 /-- Helper instance for when there are too many metavariables to apply the `DFunLike` instance
 directly. -/
-instance coeFun : CoeFun (α →₀ M) fun _ => α → M :=
+instance instCoeFun : CoeFun (α →₀ M) fun _ => α → M :=
   inferInstance
-#align finsupp.has_coe_to_fun Finsupp.coeFun
+#align finsupp.has_coe_to_fun Finsupp.instCoeFun
 
 @[ext]
 theorem ext {f g : α →₀ M} (h : ∀ a, f a = g a) : f = g :=
@@ -161,9 +161,9 @@ theorem coe_mk (f : α → M) (s : Finset α) (h : ∀ a, a ∈ s ↔ f a ≠ 0)
   rfl
 #align finsupp.coe_mk Finsupp.coe_mk
 
-instance zero : Zero (α →₀ M) :=
+instance instZero : Zero (α →₀ M) :=
   ⟨⟨∅, 0, fun _ => ⟨fun h ↦ (not_mem_empty _ h).elim, fun H => (H rfl).elim⟩⟩⟩
-#align finsupp.has_zero Finsupp.zero
+#align finsupp.has_zero Finsupp.instZero
 
 @[simp, norm_cast] lemma coe_zero : ⇑(0 : α →₀ M) = 0 := rfl
 #align finsupp.coe_zero Finsupp.coe_zero
@@ -177,9 +177,9 @@ theorem support_zero : (0 : α →₀ M).support = ∅ :=
   rfl
 #align finsupp.support_zero Finsupp.support_zero
 
-instance inhabited : Inhabited (α →₀ M) :=
+instance instInhabited : Inhabited (α →₀ M) :=
   ⟨0⟩
-#align finsupp.inhabited Finsupp.inhabited
+#align finsupp.inhabited Finsupp.instInhabited
 
 @[simp]
 theorem mem_support_iff {f : α →₀ M} : ∀ {a : α}, a ∈ f.support ↔ f a ≠ 0 :=
@@ -223,9 +223,9 @@ theorem support_nonempty_iff {f : α →₀ M} : f.support.Nonempty ↔ f ≠ 0
 theorem card_support_eq_zero {f : α →₀ M} : card f.support = 0 ↔ f = 0 := by simp
 #align finsupp.card_support_eq_zero Finsupp.card_support_eq_zero
 
-instance decidableEq [DecidableEq α] [DecidableEq M] : DecidableEq (α →₀ M) := fun f g =>
+instance instDecidableEq [DecidableEq α] [DecidableEq M] : DecidableEq (α →₀ M) := fun f g =>
   decidable_of_iff (f.support = g.support ∧ ∀ a ∈ f.support, f a = g a) ext_iff'.symm
-#align finsupp.decidable_eq Finsupp.decidableEq
+#align finsupp.decidable_eq Finsupp.instDecidableEq
 
 theorem finite_support (f : α →₀ M) : Set.Finite (Function.support f) :=
   f.fun_support_eq.symm ▸ f.support.finite_toSet
@@ -440,11 +440,11 @@ theorem single_swap (a₁ a₂ : α) (b : M) : single a₁ b a₂ = single a₂
   classical simp only [single_apply, eq_comm]
 #align finsupp.single_swap Finsupp.single_swap
 
-instance nontrivial [Nonempty α] [Nontrivial M] : Nontrivial (α →₀ M) := by
+instance instNontrivial [Nonempty α] [Nontrivial M] : Nontrivial (α →₀ M) := by
   inhabit α
   rcases exists_ne (0 : M) with ⟨x, hx⟩
   exact nontrivial_of_ne (single default x) 0 (mt single_eq_zero.1 hx)
-#align finsupp.nontrivial Finsupp.nontrivial
+#align finsupp.nontrivial Finsupp.instNontrivial
 
 theorem unique_single [Unique α] (x : α →₀ M) : x = single default (x default) :=
   ext <| Unique.forall_iff.2 single_eq_same.symm
@@ -771,9 +771,9 @@ theorem ofSupportFinite_coe {f : α → M} {hf : (Function.support f).Finite} :
   rfl
 #align finsupp.of_support_finite_coe Finsupp.ofSupportFinite_coe
 
-instance canLift : CanLift (α → M) (α →₀ M) (⇑) fun f => (Function.support f).Finite where
+instance instCanLift : CanLift (α → M) (α →₀ M) (⇑) fun f => (Function.support f).Finite where
   prf f hf := ⟨ofSupportFinite f hf, rfl⟩
-#align finsupp.can_lift Finsupp.canLift
+#align finsupp.can_lift Finsupp.instCanLift
 
 end OfSupportFinite
 
@@ -1009,9 +1009,9 @@ section AddZeroClass
 
 variable [AddZeroClass M]
 
-instance add : Add (α →₀ M) :=
+instance instAdd : Add (α →₀ M) :=
   ⟨zipWith (· + ·) (add_zero 0)⟩
-#align finsupp.has_add Finsupp.add
+#align finsupp.has_add Finsupp.instAdd
 
 @[simp, norm_cast] lemma coe_add (f g : α →₀ M) : ⇑(f + g) = f + g := rfl
 #align finsupp.coe_add Finsupp.coe_add
@@ -1042,9 +1042,9 @@ theorem single_add (a : α) (b₁ b₂ : M) : single a (b₁ + b₂) = single a
   (zipWith_single_single _ _ _ _ _).symm
 #align finsupp.single_add Finsupp.single_add
 
-instance addZeroClass : AddZeroClass (α →₀ M) :=
+instance instAddZeroClass : AddZeroClass (α →₀ M) :=
   DFunLike.coe_injective.addZeroClass _ coe_zero coe_add
-#align finsupp.add_zero_class Finsupp.addZeroClass
+#align finsupp.add_zero_class Finsupp.instAddZeroClass
 
 instance instIsLeftCancelAdd [IsLeftCancelAdd M] : IsLeftCancelAdd (α →₀ M) where
   add_left_cancel _ _ _ h := ext fun x => add_left_cancel <| DFunLike.congr_fun h x
@@ -1270,25 +1270,25 @@ variable [AddMonoid M]
 
 /-- Note the general `SMul` instance for `Finsupp` doesn't apply as `ℕ` is not distributive
 unless `β i`'s addition is commutative. -/
-instance hasNatScalar : SMul ℕ (α →₀ M) :=
+instance instNatSMul : SMul ℕ (α →₀ M) :=
   ⟨fun n v => v.mapRange (n • ·) (nsmul_zero _)⟩
-#align finsupp.has_nat_scalar Finsupp.hasNatScalar
+#align finsupp.has_nat_scalar Finsupp.instNatSMul
 
-instance addMonoid : AddMonoid (α →₀ M) :=
+instance instAddMonoid : AddMonoid (α →₀ M) :=
   DFunLike.coe_injective.addMonoid _ coe_zero coe_add fun _ _ => rfl
-#align finsupp.add_monoid Finsupp.addMonoid
+#align finsupp.add_monoid Finsupp.instAddMonoid
 
 end AddMonoid
 
-instance addCommMonoid [AddCommMonoid M] : AddCommMonoid (α →₀ M) :=
+instance instAddCommMonoid [AddCommMonoid M] : AddCommMonoid (α →₀ M) :=
   --TODO: add reference to library note in PR #7432
   { DFunLike.coe_injective.addCommMonoid (↑) coe_zero coe_add (fun _ _ => rfl) with
-    toAddMonoid := Finsupp.addMonoid }
-#align finsupp.add_comm_monoid Finsupp.addCommMonoid
+    toAddMonoid := Finsupp.instAddMonoid }
+#align finsupp.add_comm_monoid Finsupp.instAddCommMonoid
 
-instance neg [NegZeroClass G] : Neg (α →₀ G) :=
+instance instNeg [NegZeroClass G] : Neg (α →₀ G) :=
   ⟨mapRange Neg.neg neg_zero⟩
-#align finsupp.has_neg Finsupp.neg
+#align finsupp.has_neg Finsupp.instNeg
 
 @[simp, norm_cast] lemma coe_neg [NegZeroClass G] (g : α →₀ G) : ⇑(-g) = -g := rfl
 #align finsupp.coe_neg Finsupp.coe_neg
@@ -1308,9 +1308,9 @@ theorem mapRange_neg' [AddGroup G] [SubtractionMonoid H] [FunLike β G H] [AddMo
   mapRange_neg (map_neg f) v
 #align finsupp.map_range_neg' Finsupp.mapRange_neg'
 
-instance sub [SubNegZeroMonoid G] : Sub (α →₀ G) :=
+instance instSub [SubNegZeroMonoid G] : Sub (α →₀ G) :=
   ⟨zipWith Sub.sub (sub_zero _)⟩
-#align finsupp.has_sub Finsupp.sub
+#align finsupp.has_sub Finsupp.instSub
 
 @[simp, norm_cast] lemma coe_sub [SubNegZeroMonoid G] (g₁ g₂ : α →₀ G) : ⇑(g₁ - g₂) = g₁ - g₂ := rfl
 #align finsupp.coe_sub Finsupp.coe_sub
@@ -1333,23 +1333,23 @@ theorem mapRange_sub' [AddGroup G] [SubtractionMonoid H] [FunLike β G H] [AddMo
 
 /-- Note the general `SMul` instance for `Finsupp` doesn't apply as `ℤ` is not distributive
 unless `β i`'s addition is commutative. -/
-instance hasIntScalar [AddGroup G] : SMul ℤ (α →₀ G) :=
+instance instIntSMul [AddGroup G] : SMul ℤ (α →₀ G) :=
   ⟨fun n v => v.mapRange (n • ·) (zsmul_zero _)⟩
-#align finsupp.has_int_scalar Finsupp.hasIntScalar
+#align finsupp.has_int_scalar Finsupp.instIntSMul
 
-instance addGroup [AddGroup G] : AddGroup (α →₀ G) :=
+instance instAddGroup [AddGroup G] : AddGroup (α →₀ G) :=
   --TODO: add reference to library note in PR #7432
   { DFunLike.coe_injective.addGroup (↑) coe_zero coe_add coe_neg coe_sub (fun _ _ => rfl)
       fun _ _ => rfl with
-    toAddMonoid := Finsupp.addMonoid }
-#align finsupp.add_group Finsupp.addGroup
+    toAddMonoid := Finsupp.instAddMonoid }
+#align finsupp.add_group Finsupp.instAddGroup
 
-instance addCommGroup [AddCommGroup G] : AddCommGroup (α →₀ G) :=
+instance instAddCommGroup [AddCommGroup G] : AddCommGroup (α →₀ G) :=
   --TODO: add reference to library note in PR #7432
   { DFunLike.coe_injective.addCommGroup (↑) coe_zero coe_add coe_neg coe_sub (fun _ _ => rfl)
       fun _ _ => rfl with
-    toAddGroup := Finsupp.addGroup }
-#align finsupp.add_comm_group Finsupp.addCommGroup
+    toAddGroup := Finsupp.instAddGroup }
+#align finsupp.add_comm_group Finsupp.instAddCommGroup
 
 theorem single_add_single_eq_single_add_single [AddCommMonoid M] {k l m n : α} {u v : M}
     (hu : u ≠ 0) (hv : v ≠ 0) :

Mathlib/Data/Finsupp/Order.lean

@@ -138,7 +138,7 @@ end Zero
 
 
 instance orderedAddCommMonoid [OrderedAddCommMonoid α] : OrderedAddCommMonoid (ι →₀ α) :=
-  { Finsupp.addCommMonoid, Finsupp.partialorder with
+  { Finsupp.instAddCommMonoid, Finsupp.partialorder with
     add_le_add_left := fun _a _b h c s => add_le_add_left (h s) (c s) }
 
 instance orderedCancelAddCommMonoid [OrderedCancelAddCommMonoid α] :

Mathlib/Data/Finsupp/ToDFinsupp.lean

@@ -334,7 +334,7 @@ theorem sigmaFinsuppEquivDFinsupp_single [DecidableEq ι] [Zero N] (a : Σi, η
 #align sigma_finsupp_equiv_dfinsupp_single sigmaFinsuppEquivDFinsupp_single
 
 -- Without this Lean fails to find the `AddZeroClass` instance on `Π₀ i, (η i →₀ N)`.
-attribute [-instance] Finsupp.zero
+attribute [-instance] Finsupp.instZero
 
 @[simp]
 theorem sigmaFinsuppEquivDFinsupp_add [AddZeroClass N] (f g : (Σi, η i) →₀ N) :
@@ -353,7 +353,7 @@ def sigmaFinsuppAddEquivDFinsupp [AddZeroClass N] : ((Σi, η i) →₀ N) ≃+
     map_add' := sigmaFinsuppEquivDFinsupp_add }
 #align sigma_finsupp_add_equiv_dfinsupp sigmaFinsuppAddEquivDFinsupp
 
-attribute [-instance] Finsupp.addZeroClass
+attribute [-instance] Finsupp.instAddZeroClass
 
 --tofix: r • (sigma_finsupp_equiv_dfinsupp f) doesn't work.
 @[simp]
@@ -365,7 +365,7 @@ theorem sigmaFinsuppEquivDFinsupp_smul {R} [Monoid R] [AddMonoid N] [DistribMulA
   rfl
 #align sigma_finsupp_equiv_dfinsupp_smul sigmaFinsuppEquivDFinsupp_smul
 
-attribute [-instance] Finsupp.addMonoid
+attribute [-instance] Finsupp.instAddMonoid
 
 /-- `Finsupp.split` is a linear equivalence between `(Σ i, η i) →₀ N` and `Π₀ i, (η i →₀ N)`. -/
 @[simps]

Mathlib/Data/MvPolynomial/Basic.lean

@@ -101,7 +101,7 @@ section Instances
 
 instance decidableEqMvPolynomial [CommSemiring R] [DecidableEq σ] [DecidableEq R] :
     DecidableEq (MvPolynomial σ R) :=
-  Finsupp.decidableEq
+  Finsupp.instDecidableEq
 #align mv_polynomial.decidable_eq_mv_polynomial MvPolynomial.decidableEqMvPolynomial
 
 instance commSemiring [CommSemiring R] : CommSemiring (MvPolynomial σ R) :=

Mathlib/Data/Polynomial/Basic.lean

@@ -383,7 +383,7 @@ def toFinsuppIso : R[X] ≃+* R[ℕ] where
 #align polynomial.to_finsupp_iso_symm_apply Polynomial.toFinsuppIso_symm_apply
 
 instance [DecidableEq R] : DecidableEq R[X] :=
-  @Equiv.decidableEq R[X] _ (toFinsuppIso R).toEquiv (Finsupp.decidableEq)
+  @Equiv.decidableEq R[X] _ (toFinsuppIso R).toEquiv (Finsupp.instDecidableEq)
 
 end AddMonoidAlgebra
 

Mathlib/Data/Polynomial/Module/Basic.lean

@@ -209,8 +209,8 @@ def PolynomialModule (R M : Type*) [CommRing R] [AddCommGroup M] [Module R M] :=
 variable (R M : Type*) [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R)
 
 --porting note: stated instead of deriving
-noncomputable instance : Inhabited (PolynomialModule R M) := Finsupp.inhabited
-noncomputable instance : AddCommGroup (PolynomialModule R M) := Finsupp.addCommGroup
+noncomputable instance : Inhabited (PolynomialModule R M) := Finsupp.instInhabited
+noncomputable instance : AddCommGroup (PolynomialModule R M) := Finsupp.instAddCommGroup
 
 variable {M}
 
@@ -227,7 +227,7 @@ instance instFunLike : FunLike (PolynomialModule R M) ℕ M :=
   Finsupp.instFunLike
 
 instance : CoeFun (PolynomialModule R M) fun _ => ℕ → M :=
-  Finsupp.coeFun
+  Finsupp.instCoeFun
 
 theorem zero_apply (i : ℕ) : (0 : PolynomialModule R M) i = 0 :=
   Finsupp.zero_apply