chore: remove some duplicate instances (#25410)

JovanGerb · JovanGerb · commit 553449ccc081 · 2025-07-31T23:59:21.000Z
I have a program that finds duplicate instances, as described at [#mathlib4 > duplicate declarations](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/duplicate.20declarations/with/518941841) This PR is a start at fixing these in Mathlib.
diff --git a/Mathlib/Algebra/Category/Grp/Adjunctions.lean b/Mathlib/Algebra/Category/Grp/Adjunctions.lean
@@ -79,9 +79,6 @@ instance : free.{u}.IsLeftAdjoint :=
 instance : (forget AddCommGrp.{u}).IsRightAdjoint :=
   ⟨_, ⟨adj⟩⟩
 
-instance : AddCommGrp.free.{u}.IsLeftAdjoint :=
-  ⟨_, ⟨adj⟩⟩
-
 /-- As an example, we now give a high-powered proof that
 the monomorphisms in `AddCommGroup` are just the injective functions.
 
diff --git a/Mathlib/Algebra/Category/ModuleCat/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Basic.lean
@@ -186,9 +186,6 @@ def homEquiv {M N : ModuleCat.{v} R} : (M ⟶ N) ≃ (M →ₗ[R] N) where
 
 end
 
-instance : Inhabited (ModuleCat R) :=
-  ⟨of R R⟩
-
 /- Not a `@[simp]` lemma since it will rewrite the (co)domain of maps and cause
 definitional equality issues. -/
 lemma forget_obj {M : ModuleCat.{v} R} : (forget (ModuleCat.{v} R)).obj M = M := rfl
diff --git a/Mathlib/Algebra/Group/Fin/Basic.lean b/Mathlib/Algebra/Group/Fin/Basic.lean
@@ -29,10 +29,6 @@ instance addCommSemigroup (n : ℕ) : AddCommSemigroup (Fin n) where
   add_assoc := by simp [add_def, Nat.add_assoc]
   add_comm := by simp [add_def, Nat.add_comm]
 
-instance (n) : AddCommSemigroup (Fin n) where
-  add_assoc := by simp [add_def, Nat.add_assoc]
-  add_comm := by simp [add_def, add_comm]
-
 instance addCommMonoid (n : ℕ) [NeZero n] : AddCommMonoid (Fin n) where
   zero_add := Fin.zero_add
   add_zero := Fin.add_zero
diff --git a/Mathlib/Algebra/Homology/Embedding/IsSupported.lean b/Mathlib/Algebra/Homology/Embedding/IsSupported.lean
@@ -57,8 +57,7 @@ lemma isStrictlySupported_op_iff :
   ⟨(fun _ ↦ ⟨fun i' hi' ↦ (K.op.isZero_X_of_isStrictlySupported e.op i' hi').unop⟩),
     (fun _ ↦ ⟨fun i' hi' ↦ (K.isZero_X_of_isStrictlySupported e i' hi').op⟩)⟩
 
-instance [K.IsStrictlySupported e] :
-    K.op.IsStrictlySupported e.op := by
+instance [K.IsStrictlySupported e] : K.op.IsStrictlySupported e.op := by
   rw [isStrictlySupported_op_iff]
   infer_instance
 
@@ -137,9 +136,6 @@ lemma isZero_iff_isStrictlySupported_and_isStrictlySupportedOutside :
       exact h₂.isZero i
     · exact K.isZero_X_of_isStrictlySupported e _ (by simpa using hn)
 
-instance [K.IsStrictlySupported e] : K.op.IsStrictlySupported e.op where
-  isZero j hj' := (K.isZero_X_of_isStrictlySupported e j hj').op
-
 end
 
 section
diff --git a/Mathlib/Algebra/Order/Hom/Monoid.lean b/Mathlib/Algebra/Order/Hom/Monoid.lean
@@ -164,13 +164,6 @@ def OrderMonoidIsoClass.toOrderMonoidIso [EquivLike F α β] [OrderIsoClass F α
     α ≃*o β :=
   { (f : α ≃* β) with map_le_map_iff' := OrderIsoClass.map_le_map_iff f }
 
-/-- Any type satisfying `OrderMonoidHomClass` can be cast into `OrderMonoidHom` via
-  `OrderMonoidHomClass.toOrderMonoidHom`. -/
-@[to_additive "Any type satisfying `OrderAddMonoidHomClass` can be cast into `OrderAddMonoidHom` via
-  `OrderAddMonoidHomClass.toOrderAddMonoidHom`"]
-instance [OrderHomClass F α β] [MonoidHomClass F α β] : CoeTC F (α →*o β) :=
-  ⟨OrderMonoidHomClass.toOrderMonoidHom⟩
-
 /-- Any type satisfying `OrderMonoidIsoClass` can be cast into `OrderMonoidIso` via
   `OrderMonoidIsoClass.toOrderMonoidIso`. -/
 @[to_additive "Any type satisfying `OrderAddMonoidIsoClass` can be cast into `OrderAddMonoidIso` via
diff --git a/Mathlib/Algebra/Ring/Divisibility/Basic.lean b/Mathlib/Algebra/Ring/Divisibility/Basic.lean
@@ -6,7 +6,6 @@ Authors: Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Yury Kudryashov, Ne
 import Mathlib.Algebra.Divisibility.Hom
 import Mathlib.Algebra.Group.Equiv.Basic
 import Mathlib.Algebra.Ring.Defs
-import Mathlib.Data.Nat.Basic
 
 /-!
 # Lemmas about divisibility in rings
diff --git a/Mathlib/Algebra/Ring/Subsemiring/Basic.lean b/Mathlib/Algebra/Ring/Subsemiring/Basic.lean
@@ -917,11 +917,6 @@ instance distribMulAction [AddMonoid α] [DistribMulAction R' α] (S : Subsemiri
     DistribMulAction S α :=
   inferInstance
 
-instance (priority := low) [AddCommMonoid α] [Module R' α] {S' : Type*} [SetLike S' R']
-    [SubsemiringClass S' R'] (s : S') : Module s α where
-  add_smul r₁ r₂ := add_smul (r₁ : R') r₂
-  zero_smul := zero_smul R'
-
 /-- The action by a subsemiring is the action by the underlying semiring. -/
 instance mulDistribMulAction [Monoid α] [MulDistribMulAction R' α] (S : Subsemiring R') :
     MulDistribMulAction S α :=
diff --git a/Mathlib/AlgebraicGeometry/Limits.lean b/Mathlib/AlgebraicGeometry/Limits.lean
@@ -457,10 +457,6 @@ instance : PreservesColimitsOfShape (Discrete PEmpty.{1}) Scheme.Spec.{u} := by
 instance {J : Type*} [Finite J] : PreservesColimitsOfShape (Discrete J) Scheme.Spec.{u} :=
   preservesFiniteCoproductsOfPreservesBinaryAndInitial _ _
 
-instance {J : Type*} [Finite J] : PreservesColimitsOfShape (Discrete J) Scheme.Spec.{u} :=
-  letI := (nonempty_fintype J).some
-  preservesColimitsOfShape_of_equiv (Discrete.equivalence (Fintype.equivFin _).symm) _
-
 /-- The canonical map `∐ Spec Rᵢ ⟶ Spec (Π Rᵢ)`.
 This is an isomorphism when the product is finite. -/
 noncomputable
diff --git a/Mathlib/AlgebraicGeometry/OpenImmersion.lean b/Mathlib/AlgebraicGeometry/OpenImmersion.lean
@@ -34,9 +34,6 @@ of LocallyRingedSpaces
 abbrev IsOpenImmersion : MorphismProperty (Scheme.{u}) :=
   fun _ _ f ↦ LocallyRingedSpace.IsOpenImmersion f.toLRSHom
 
-instance : IsOpenImmersion.IsStableUnderComposition where
-  comp_mem f g := fun _ _ ↦ LocallyRingedSpace.IsOpenImmersion.comp f.toLRSHom g.toLRSHom
-
 instance IsOpenImmersion.comp {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)
     [IsOpenImmersion f] [IsOpenImmersion g] : IsOpenImmersion (f ≫ g) :=
   LocallyRingedSpace.IsOpenImmersion.comp f.toLRSHom g.toLRSHom
diff --git a/Mathlib/CategoryTheory/Countable.lean b/Mathlib/CategoryTheory/Countable.lean
@@ -79,8 +79,6 @@ end CountableCategory
 
 instance (α : Type*) [Category α] [FinCategory α] : CountableCategory α where
 
-instance : CountableCategory ℕ where
-
 open Opposite
 
 /-- The opposite of a countable category is countable. -/
diff --git a/Mathlib/CategoryTheory/EffectiveEpi/Preserves.lean b/Mathlib/CategoryTheory/EffectiveEpi/Preserves.lean
@@ -206,9 +206,6 @@ instance (F : C ⥤ D) [ReflectsFiniteEffectiveEpiFamilies F] : ReflectsEffectiv
     have := F.finite_effectiveEpiFamily_of_map _ _ h
     infer_instance
 
-instance (F : C ⥤ D) [IsEquivalence F] : F.PreservesEffectiveEpiFamilies where
-  preserves _ _ := inferInstance
-
 instance (F : C ⥤ D) [IsEquivalence F] : F.ReflectsEffectiveEpiFamilies where
   reflects {α B} X π _ := by
     let i : (a : α) → X a ⟶ (inv F).obj (F.obj (X a)) := fun a ↦ (asEquivalence F).unit.app _
diff --git a/Mathlib/CategoryTheory/ObjectProperty/FullSubcategory.lean b/Mathlib/CategoryTheory/ObjectProperty/FullSubcategory.lean
@@ -141,12 +141,6 @@ instance [F.Faithful] : (P.lift F hF).Faithful :=
 instance [F.Full] : (P.lift F hF).Full :=
   Functor.Full.of_comp_faithful_iso (P.liftCompιIso F hF)
 
-instance [F.Faithful] : (P.lift F hF).Faithful :=
-  Functor.Faithful.of_comp_iso (P.liftCompιIso F hF)
-
-instance [F.Full] : (P.lift F hF).Full :=
-  Functor.Full.of_comp_faithful_iso (P.liftCompιIso F hF)
-
 variable {Q}
 
 /-- When `h : P ≤ Q`, this is the canonical isomorphism
diff --git a/Mathlib/Computability/TuringDegree.lean b/Mathlib/Computability/TuringDegree.lean
@@ -119,8 +119,6 @@ theorem partrec_iff_forall_turingReducible : Nat.Partrec f ↔ ∀ g, f ≤ᵀ g
 protected theorem TuringReducible.refl (f : ℕ →. ℕ) : f ≤ᵀ f := .oracle _ <| by simp
 protected theorem TuringReducible.rfl : f ≤ᵀ f := .refl _
 
-instance : IsRefl (ℕ →. ℕ) TuringReducible where refl _ := .rfl
-
 theorem TuringReducible.trans (hg : f ≤ᵀ g) (hh : g ≤ᵀ h) : f ≤ᵀ h := by
   induction hg with repeat {constructor}
   | oracle _ hg => rw [Set.mem_singleton_iff] at hg; rw [hg]; exact hh
@@ -129,11 +127,9 @@ theorem TuringReducible.trans (hg : f ≤ᵀ g) (hh : g ≤ᵀ h) : f ≤ᵀ h :
   | prec _ _ ih₁ ih₂ => exact RecursiveIn.prec ih₁ ih₂
   | rfind _ ih => exact RecursiveIn.rfind ih
 
-instance : IsTrans (ℕ →. ℕ) TuringReducible :=
-  ⟨@TuringReducible.trans⟩
-
 instance : IsPreorder (ℕ →. ℕ) TuringReducible where
-  refl := .refl
+  refl _ := .rfl
+  trans := @TuringReducible.trans
 
 theorem TuringEquivalent.equivalence : Equivalence TuringEquivalent :=
   (AntisymmRel.setoid _ _).iseqv
@@ -150,13 +146,6 @@ theorem TuringEquivalent.symm {f g : ℕ →. ℕ} (h : f ≡ᵀ g) : g ≡ᵀ f
 theorem TuringEquivalent.trans (f g h : ℕ →. ℕ) (h₁ : f ≡ᵀ g) (h₂ : g ≡ᵀ h) : f ≡ᵀ h :=
   Equivalence.trans equivalence h₁ h₂
 
-/--
-Instance declaring that `RecursiveIn` is a preorder.
--/
-instance : IsPreorder (ℕ →. ℕ) TuringReducible where
-  refl := TuringReducible.refl
-  trans := @TuringReducible.trans
-
 /--
 Turing degrees are the equivalence classes of partial functions under Turing equivalence.
 -/
diff --git a/Mathlib/Data/ENat/Basic.lean b/Mathlib/Data/ENat/Basic.lean
@@ -38,7 +38,7 @@ assert_not_exists Field
 
 deriving instance Zero, CommSemiring, Nontrivial,
   LinearOrder, Bot, Sub,
-  LinearOrderedAddCommMonoidWithTop, WellFoundedRelation
+  LinearOrderedAddCommMonoidWithTop
   for ENat
 -- The `CanonicallyOrderedAdd, OrderBot, OrderTop, OrderedSub, SuccOrder, WellFoundedLT, CharZero`
 -- instances should be constructed by a deriving handler.
diff --git a/Mathlib/Data/Fintype/EquivFin.lean b/Mathlib/Data/Fintype/EquivFin.lean
@@ -217,8 +217,6 @@ theorem card_eq_one_iff_nonempty_unique : card α = 1 ↔ Nonempty (Unique α) :
         uniq := h }⟩,
     fun ⟨_h⟩ => Fintype.card_unique⟩
 
-instance [Nonempty α] : NeZero (card α) := ⟨card_ne_zero⟩
-
 theorem card_le_one_iff : card α ≤ 1 ↔ ∀ a b : α, a = b :=
   let n := card α
   have hn : n = card α := rfl
diff --git a/Mathlib/Data/List/TakeDrop.lean b/Mathlib/Data/List/TakeDrop.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
 -/
 import Mathlib.Data.List.Defs
-import Mathlib.Data.Nat.Basic
 import Mathlib.Tactic.Common
 
 /-!
diff --git a/Mathlib/Data/Matroid/Constructions.lean b/Mathlib/Data/Matroid/Constructions.lean
@@ -106,8 +106,8 @@ theorem eq_loopyOn_iff : M = loopyOn E ↔ M.E = E ∧ ∀ X ⊆ M.E, M.Indep X
   ⟨fun h ↦ ⟨loopyOn_indep_iff.mp h.indep, h.subset_ground⟩,
     by rintro ⟨rfl, hX⟩; rw [isBasis_iff]; simp⟩
 
-instance : RankFinite (loopyOn E) :=
-  ⟨⟨∅, loopyOn_isBase_iff.2 rfl, finite_empty⟩⟩
+instance loopyOn_rankFinite : RankFinite (loopyOn E) :=
+  ⟨∅, by simp⟩
 
 theorem Finite.loopyOn_finite (hE : E.Finite) : Matroid.Finite (loopyOn E) :=
   ⟨hE⟩
@@ -129,9 +129,6 @@ theorem eq_loopyOn_or_rankPos (M : Matroid α) : M = loopyOn M.E ∨ RankPos M :
 theorem not_rankPos_iff : ¬RankPos M ↔ M = loopyOn M.E := by
   rw [rankPos_iff, not_iff_comm, empty_isBase_iff]
 
-instance loopyOn_rankFinite : RankFinite (loopyOn E) :=
-  ⟨∅, by simp⟩
-
 end LoopyOn
 
 section FreeOn
diff --git a/Mathlib/Data/Nat/Basic.lean b/Mathlib/Data/Nat/Basic.lean
@@ -42,9 +42,6 @@ instance instLinearOrder : LinearOrder ℕ where
 -- Shortcut instances
 instance : Preorder ℕ := inferInstance
 instance : PartialOrder ℕ := inferInstance
-instance : Min ℕ := inferInstance
-instance : Max ℕ := inferInstance
-instance : Ord ℕ := inferInstance
 
 instance instNontrivial : Nontrivial ℕ := ⟨⟨0, 1, Nat.zero_ne_one⟩⟩
 
diff --git a/Mathlib/Data/Option/Defs.lean b/Mathlib/Data/Option/Defs.lean
@@ -51,21 +51,20 @@ abbrev iget [Inhabited α] : Option α → α
 theorem iget_some [Inhabited α] {a : α} : (some a).iget = a :=
   rfl
 
-instance merge_isCommutative (f : α → α → α) [Std.Commutative f] :
-    Std.Commutative (merge f) :=
-  ⟨fun a b ↦ by cases a <;> cases b <;> simp [merge, Std.Commutative.comm]⟩
+@[deprecated commutative_merge (since := "2025-06-03")]
+theorem merge_isCommutative (f : α → α → α) [Std.Commutative f] :
+    Std.Commutative (merge f) := commutative_merge f
 
-instance merge_isAssociative (f : α → α → α) [Std.Associative f] :
-    Std.Associative (merge f) :=
-  ⟨fun a b c ↦ by cases a <;> cases b <;> cases c <;> simp [merge, Std.Associative.assoc]⟩
+@[deprecated associative_merge (since := "2025-06-03")]
+theorem merge_isAssociative (f : α → α → α) [Std.Associative f] :
+    Std.Associative (merge f) := associative_merge f
 
-instance merge_isIdempotent (f : α → α → α) [Std.IdempotentOp f] :
-    Std.IdempotentOp (merge f) :=
-  ⟨fun a ↦ by cases a <;> simp [merge, Std.IdempotentOp.idempotent]⟩
+@[deprecated idempotentOp_merge (since := "2025-06-03")]
+theorem merge_isIdempotent (f : α → α → α) [Std.IdempotentOp f] :
+    Std.IdempotentOp (merge f) := idempotentOp_merge f
 
-instance merge_isId (f : α → α → α) : Std.LawfulIdentity (merge f) none where
-  left_id a := by cases a <;> simp [merge]
-  right_id a := by cases a <;> simp [merge]
+@[deprecated lawfulIdentity_merge (since := "2025-06-03")]
+theorem merge_isId (f : α → α → α) : Std.LawfulIdentity (merge f) none := lawfulIdentity_merge f
 
 @[deprecated (since := "2025-04-04")] alias liftOrGet_isCommutative :=
   merge_isCommutative
diff --git a/Mathlib/Data/Ordering/Basic.lean b/Mathlib/Data/Ordering/Basic.lean
@@ -13,8 +13,6 @@ import Mathlib.Tactic.TypeStar
 
 universe u
 
-deriving instance Repr for Ordering
-
 namespace Ordering
 
 variable {α : Type*}
diff --git a/Mathlib/Data/Sign/Defs.lean b/Mathlib/Data/Sign/Defs.lean
@@ -69,9 +69,6 @@ instance : LE SignType :=
 instance LE.decidableRel : DecidableRel SignType.LE := fun a b => by
   cases a <;> cases b <;> first | exact isTrue (by constructor)| exact isFalse (by rintro ⟨_⟩)
 
-instance decidableEq : DecidableEq SignType := fun a b => by
-  cases a <;> cases b <;> first | exact isTrue (by constructor)| exact isFalse (by rintro ⟨_⟩)
-
 private lemma mul_comm : ∀ (a b : SignType), a * b = b * a := by rintro ⟨⟩ ⟨⟩ <;> rfl
 private lemma mul_assoc : ∀ (a b c : SignType), (a * b) * c = a * (b * c) := by
   rintro ⟨⟩ ⟨⟩ ⟨⟩ <;> rfl
@@ -106,7 +103,6 @@ instance : LinearOrder SignType where
   le_antisymm := le_antisymm
   le_trans := le_trans
   toDecidableLE := LE.decidableRel
-  toDecidableEq := SignType.decidableEq
 
 instance : BoundedOrder SignType where
   top := 1
diff --git a/Mathlib/GroupTheory/Perm/Sign.lean b/Mathlib/GroupTheory/Perm/Sign.lean
@@ -13,7 +13,6 @@ import Mathlib.Data.Fintype.Prod
 import Mathlib.Data.Fintype.Sum
 import Mathlib.Data.Int.Order.Units
 import Mathlib.GroupTheory.Perm.Support
-import Mathlib.Logic.Equiv.Fin.Basic
 import Mathlib.Logic.Equiv.Fintype
 import Mathlib.Tactic.NormNum.Ineq
 import Mathlib.Data.Finset.Sigma
diff --git a/Mathlib/Logic/Embedding/Basic.lean b/Mathlib/Logic/Embedding/Basic.lean
@@ -42,9 +42,6 @@ theorem exists_surjective_iff {α β : Sort*} :
   ⟨fun ⟨f, h⟩ ↦ ⟨⟨f⟩, ⟨⟨_, injective_surjInv h⟩⟩⟩, fun ⟨h, ⟨e⟩⟩ ↦ (nonempty_fun.mp h).elim
     (fun _ ↦ ⟨isEmptyElim, (isEmptyElim <| e ·)⟩) fun _ ↦ ⟨_, invFun_surjective e.inj'⟩⟩
 
-instance {α β : Sort*} : CanLift (α → β) (α ↪ β) (↑) Injective where
-  prf _ h := ⟨⟨_, h⟩, rfl⟩
-
 end Function
 
 section Equiv
diff --git a/Mathlib/Logic/Equiv/Fin/Basic.lean b/Mathlib/Logic/Equiv/Fin/Basic.lean
@@ -394,13 +394,13 @@ def Fin.castLEquiv {n m : ℕ} (h : n ≤ m) : Fin n ≃ { i : Fin m // (i : ℕ
   left_inv _ := by simp
   right_inv _ := by simp
 
-/-- `Fin 0` is a subsingleton. -/
-instance subsingleton_fin_zero : Subsingleton (Fin 0) :=
-  finZeroEquiv.subsingleton
+@[deprecated Fin.subsingleton_zero (since := "2025-06-03")]
+theorem subsingleton_fin_zero : Subsingleton (Fin 0) :=
+  Fin.subsingleton_zero
 
-/-- `Fin 1` is a subsingleton. -/
-instance subsingleton_fin_one : Subsingleton (Fin 1) :=
-  finOneEquiv.subsingleton
+@[deprecated Fin.subsingleton_one (since := "2025-06-03")]
+theorem subsingleton_fin_one : Subsingleton (Fin 1) :=
+  Fin.subsingleton_one
 
 /-- The natural `Equiv` between `(Fin m → α) × (Fin n → α)` and `Fin (m + n) → α` -/
 @[simps]
diff --git a/Mathlib/ModelTheory/Basic.lean b/Mathlib/ModelTheory/Basic.lean
@@ -3,7 +3,6 @@ Copyright (c) 2021 Aaron Anderson, Jesse Michael Han, Floris van Doorn. All righ
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson, Jesse Michael Han, Floris van Doorn
 -/
-import Mathlib.Data.Fin.VecNotation
 import Mathlib.SetTheory.Cardinal.Basic
 
 /-!
diff --git a/Mathlib/Order/Monotone/Basic.lean b/Mathlib/Order/Monotone/Basic.lean
@@ -50,33 +50,9 @@ decreasing, strictly decreasing
 
 open Function OrderDual
 
-universe u v w
+universe u v
 
-variable {ι : Type*} {α : Type u} {β : Type v} {γ : Type w} {δ : Type*} {π : ι → Type*}
-
-section Decidable
-
-variable [Preorder α] [Preorder β] {f : α → β} {s : Set α}
-
-instance [i : Decidable (∀ a b, a ≤ b → f a ≤ f b)] : Decidable (Monotone f) := i
-instance [i : Decidable (∀ a b, a ≤ b → f b ≤ f a)] : Decidable (Antitone f) := i
-
-instance [i : Decidable (∀ a ∈ s, ∀ b ∈ s, a ≤ b → f a ≤ f b)] :
-    Decidable (MonotoneOn f s) := i
-
-instance [i : Decidable (∀ a ∈ s, ∀ b ∈ s, a ≤ b → f b ≤ f a)] :
-    Decidable (AntitoneOn f s) := i
-
-instance [i : Decidable (∀ a b, a < b → f a < f b)] : Decidable (StrictMono f) := i
-instance [i : Decidable (∀ a b, a < b → f b < f a)] : Decidable (StrictAnti f) := i
-
-instance [i : Decidable (∀ a ∈ s, ∀ b ∈ s, a < b → f a < f b)] :
-    Decidable (StrictMonoOn f s) := i
-
-instance [i : Decidable (∀ a ∈ s, ∀ b ∈ s, a < b → f b < f a)] :
-    Decidable (StrictAntiOn f s) := i
-
-end Decidable
+variable {ι : Type*} {α : Type u} {β : Type v}
 
 /-! ### Monotonicity on the dual order
 
diff --git a/Mathlib/SetTheory/Cardinal/Basic.lean b/Mathlib/SetTheory/Cardinal/Basic.lean
@@ -8,7 +8,6 @@ import Mathlib.Data.Fintype.BigOperators
 import Mathlib.Data.Fintype.Powerset
 import Mathlib.Data.Nat.Cast.Order.Basic
 import Mathlib.Data.Set.Countable
-import Mathlib.Logic.Equiv.Fin.Basic
 import Mathlib.Logic.Small.Set
 import Mathlib.Logic.UnivLE
 import Mathlib.SetTheory.Cardinal.Order
diff --git a/Mathlib/Tactic/Polyrith.lean b/Mathlib/Tactic/Polyrith.lean
@@ -75,7 +75,7 @@ inductive Poly
   | div : Poly → Poly → Poly
   | pow : Poly → Poly → Poly
   | neg : Poly → Poly
-  deriving BEq, Repr
+  deriving BEq
 
 /--
 This converts a poly object into a string representing it. The string
diff --git a/Mathlib/Topology/Compactness/Lindelof.lean b/Mathlib/Topology/Compactness/Lindelof.lean
