bump to nightly-2023-04-24-06

mathlib commit leanprover-community/mathlib@0907952

Mathbin/Algebra/AddTorsor.lean

@@ -60,7 +60,7 @@ class AddTorsor (G : outParam (Type _)) (P : Type _) [outParam <| AddGroup G] ex
 #align add_torsor AddTorsor
 -/
 
-attribute [instance, nolint dangerous_instance] AddTorsor.nonempty
+attribute [instance 100, nolint dangerous_instance] AddTorsor.nonempty
 
 attribute [nolint dangerous_instance] AddTorsor.toHasVsub
 

Mathbin/Algebra/Algebra/Basic.lean

@@ -148,7 +148,7 @@ def coeHTCT (R A : Type _) [CommSemiring R] [Semiring A] [Algebra R A] : HasLift
   ⟨fun r => algebraMap R A r⟩
 #align algebra_map.has_lift_t algebraMap.coeHTCT
 
-attribute [instance] algebraMap.coeHTCT
+attribute [instance 900] algebraMap.coeHTCT
 
 section CommSemiringSemiring
 
@@ -433,7 +433,7 @@ instance (priority := 200) toModule : Module R A
 
 -- From now on, we don't want to use the following instance anymore.
 -- Unfortunately, leaving it in place causes deterministic timeouts later in mathlib.
-attribute [instance] Algebra.toHasSmul
+attribute [instance 0] Algebra.toHasSmul
 
 /- warning: algebra.smul_def -> Algebra.smul_def is a dubious translation:
 lean 3 declaration is

Mathbin/Algebra/Category/Algebra/Limits.lean

@@ -130,7 +130,7 @@ end HasLimits
 
 open HasLimits
 
-/- ./././Mathport/Syntax/Translate/Command.lean:317:38: unsupported irreducible non-definition -/
+/- ./././Mathport/Syntax/Translate/Command.lean:322:38: unsupported irreducible non-definition -/
 /-- The category of R-algebras has all limits. -/
 irreducible_def hasLimitsOfSize : HasLimitsOfSize.{v, v} (AlgebraCat.{max v w} R) :=
   {

Mathbin/Algebra/Category/Module/Limits.lean

@@ -128,7 +128,7 @@ end HasLimits
 
 open HasLimits
 
-/- ./././Mathport/Syntax/Translate/Command.lean:317:38: unsupported irreducible non-definition -/
+/- ./././Mathport/Syntax/Translate/Command.lean:322:38: unsupported irreducible non-definition -/
 /-- The category of R-modules has all limits. -/
 irreducible_def hasLimitsOfSize : HasLimitsOfSize.{v, v} (ModuleCat.{max v w} R) :=
   {

Mathbin/Algebra/Category/Ring/Limits.lean

@@ -104,7 +104,7 @@ end HasLimits
 
 open HasLimits
 
-/- ./././Mathport/Syntax/Translate/Command.lean:317:38: unsupported irreducible non-definition -/
+/- ./././Mathport/Syntax/Translate/Command.lean:322:38: unsupported irreducible non-definition -/
 /-- The category of rings has all limits. -/
 irreducible_def hasLimitsOfSize : HasLimitsOfSize.{v} SemiRing.{max v u} :=
   {
@@ -233,7 +233,7 @@ def limitConeIsLimit (F : J ⥤ CommSemiRing.{max v u}) : IsLimit (limitCone F)
   liftedLimitIsLimit _
 #align CommSemiRing.limit_cone_is_limit CommSemiRing.limitConeIsLimit
 
-/- ./././Mathport/Syntax/Translate/Command.lean:317:38: unsupported irreducible non-definition -/
+/- ./././Mathport/Syntax/Translate/Command.lean:322:38: unsupported irreducible non-definition -/
 /-- The category of rings has all limits. -/
 irreducible_def hasLimitsOfSize : HasLimitsOfSize.{v, v} CommSemiRing.{max v u} :=
   {
@@ -331,7 +331,7 @@ def limitConeIsLimit (F : J ⥤ RingCat.{max v u}) : IsLimit (limitCone F) :=
   liftedLimitIsLimit _
 #align Ring.limit_cone_is_limit RingCat.limitConeIsLimit
 
-/- ./././Mathport/Syntax/Translate/Command.lean:317:38: unsupported irreducible non-definition -/
+/- ./././Mathport/Syntax/Translate/Command.lean:322:38: unsupported irreducible non-definition -/
 /-- The category of rings has all limits. -/
 irreducible_def hasLimitsOfSize : HasLimitsOfSize.{v, v} RingCat.{max v u} :=
   {
@@ -458,7 +458,7 @@ def limitConeIsLimit (F : J ⥤ CommRingCat.{max v u}) : IsLimit (limitCone F) :
   liftedLimitIsLimit _
 #align CommRing.limit_cone_is_limit CommRingCat.limitConeIsLimit
 
-/- ./././Mathport/Syntax/Translate/Command.lean:317:38: unsupported irreducible non-definition -/
+/- ./././Mathport/Syntax/Translate/Command.lean:322:38: unsupported irreducible non-definition -/
 /-- The category of commutative rings has all limits. -/
 irreducible_def hasLimitsOfSize : HasLimitsOfSize.{v, v} CommRingCat.{max v u} :=
   {

Mathbin/Algebra/CharP/Basic.lean

@@ -148,7 +148,7 @@ end CommSemiring
 variable (R)
 
 #print CharP /-
-/- ./././Mathport/Syntax/Translate/Command.lean:388:30: infer kinds are unsupported in Lean 4: #[`cast_eq_zero_iff] [] -/
+/- ./././Mathport/Syntax/Translate/Command.lean:393:30: infer kinds are unsupported in Lean 4: #[`cast_eq_zero_iff] [] -/
 /-- The generator of the kernel of the unique homomorphism ℕ → R for a semiring R.
 
 *Warning*: for a semiring `R`, `char_p R 0` and `char_zero R` need not coincide.

Mathbin/Algebra/ContinuedFractions/Basic.lean

@@ -60,7 +60,7 @@ protected structure GeneralizedContinuedFraction.Pair where
 
 open GeneralizedContinuedFraction
 
-/- ./././Mathport/Syntax/Translate/Command.lean:224:11: unsupported: unusual advanced open style -/
+/- ./././Mathport/Syntax/Translate/Command.lean:229:11: unsupported: unusual advanced open style -/
 /-! Interlude: define some expected coercions and instances. -/
 
 

Mathbin/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean

@@ -36,7 +36,7 @@ rational, continued fraction, termination
 
 namespace GeneralizedContinuedFraction
 
-/- ./././Mathport/Syntax/Translate/Command.lean:224:11: unsupported: unusual advanced open style -/
+/- ./././Mathport/Syntax/Translate/Command.lean:229:11: unsupported: unusual advanced open style -/
 open GeneralizedContinuedFraction (of)
 
 variable {K : Type _} [LinearOrderedField K] [FloorRing K]

Mathbin/Algebra/ContinuedFractions/Computation/Translations.lean

@@ -47,7 +47,7 @@ namespace GeneralizedContinuedFraction
 
 open GeneralizedContinuedFraction (of)
 
-/- ./././Mathport/Syntax/Translate/Command.lean:224:11: unsupported: unusual advanced open style -/
+/- ./././Mathport/Syntax/Translate/Command.lean:229:11: unsupported: unusual advanced open style -/
 -- Fix a discrete linear ordered floor field and a value `v`.
 variable {K : Type _} [LinearOrderedField K] [FloorRing K] {v : K}
 

Mathbin/Algebra/ContinuedFractions/ConvergentsEquiv.lean

@@ -73,7 +73,7 @@ variable {K : Type _} {n : ℕ}
 
 namespace GeneralizedContinuedFraction
 
-/- ./././Mathport/Syntax/Translate/Command.lean:224:11: unsupported: unusual advanced open style -/
+/- ./././Mathport/Syntax/Translate/Command.lean:229:11: unsupported: unusual advanced open style -/
 variable {g : GeneralizedContinuedFraction K} {s : Seq <| Pair K}
 
 section Squash

Mathbin/Algebra/ContinuedFractions/TerminatedStable.lean

@@ -21,7 +21,7 @@ We show that the continuants and convergents of a gcf stabilise once the gcf ter
 
 namespace GeneralizedContinuedFraction
 
-/- ./././Mathport/Syntax/Translate/Command.lean:224:11: unsupported: unusual advanced open style -/
+/- ./././Mathport/Syntax/Translate/Command.lean:229:11: unsupported: unusual advanced open style -/
 variable {K : Type _} {g : GeneralizedContinuedFraction K} {n m : ℕ}
 
 /-- If a gcf terminated at position `n`, it also terminated at `m ≥ n`.-/

Mathbin/Algebra/ContinuedFractions/Translations.lean

@@ -22,7 +22,7 @@ Some simple translation lemmas between the different definitions of functions de
 
 namespace GeneralizedContinuedFraction
 
-/- ./././Mathport/Syntax/Translate/Command.lean:224:11: unsupported: unusual advanced open style -/
+/- ./././Mathport/Syntax/Translate/Command.lean:229:11: unsupported: unusual advanced open style -/
 section General
 
 /-!

Mathbin/Algebra/DirectLimit.lean

@@ -47,8 +47,8 @@ variable [dec_ι : DecidableEq ι] [Preorder ι]
 
 variable (G : ι → Type w)
 
-/- ./././Mathport/Syntax/Translate/Command.lean:388:30: infer kinds are unsupported in Lean 4: #[`map_self] [] -/
-/- ./././Mathport/Syntax/Translate/Command.lean:388:30: infer kinds are unsupported in Lean 4: #[`map_map] [] -/
+/- ./././Mathport/Syntax/Translate/Command.lean:393:30: infer kinds are unsupported in Lean 4: #[`map_self] [] -/
+/- ./././Mathport/Syntax/Translate/Command.lean:393:30: infer kinds are unsupported in Lean 4: #[`map_map] [] -/
 /-- A directed system is a functor from a category (directed poset) to another category. -/
 class DirectedSystem (f : ∀ i j, i ≤ j → G i → G j) : Prop where
   map_self : ∀ i x h, f i i h x = x

Mathbin/Algebra/Group/Conj.lean

@@ -234,7 +234,7 @@ protected def setoid (α : Type _) [Monoid α] : Setoid α
 
 end IsConj
 
-attribute [local instance] IsConj.setoid
+attribute [local instance 100] IsConj.setoid
 
 #print ConjClasses /-
 /-- The quotient type of conjugacy classes of a group. -/

Mathbin/Algebra/Group/ConjFinite.lean

@@ -22,7 +22,7 @@ import Mathbin.Data.Fintype.Units
 
 variable {α : Type _} [Monoid α]
 
-attribute [local instance] IsConj.setoid
+attribute [local instance 100] IsConj.setoid
 
 instance [Fintype α] [DecidableRel (IsConj : α → α → Prop)] : Fintype (ConjClasses α) :=
   Quotient.fintype (IsConj.setoid α)

Mathbin/Algebra/Group/Defs.lean

@@ -1527,7 +1527,7 @@ class AddCommGroup (G : Type u) extends AddGroup G, AddCommMonoid G
 
 attribute [to_additive] CommGroup
 
-attribute [instance] AddCommGroup.toAddCommMonoid
+attribute [instance 300] AddCommGroup.toAddCommMonoid
 
 #print CommGroup.toGroup_injective /-
 @[to_additive]

Mathbin/Algebra/Module/LocalizedModule.lean

@@ -581,9 +581,9 @@ variable {M M' M'' : Type _} [AddCommMonoid M] [AddCommMonoid M'] [AddCommMonoid
 
 variable [Module R M] [Module R M'] [Module R M''] (f : M →ₗ[R] M') (g : M →ₗ[R] M'')
 
-/- ./././Mathport/Syntax/Translate/Command.lean:388:30: infer kinds are unsupported in Lean 4: #[`map_units] [] -/
-/- ./././Mathport/Syntax/Translate/Command.lean:388:30: infer kinds are unsupported in Lean 4: #[`surj] [] -/
-/- ./././Mathport/Syntax/Translate/Command.lean:388:30: infer kinds are unsupported in Lean 4: #[`eq_iff_exists] [] -/
+/- ./././Mathport/Syntax/Translate/Command.lean:393:30: infer kinds are unsupported in Lean 4: #[`map_units] [] -/
+/- ./././Mathport/Syntax/Translate/Command.lean:393:30: infer kinds are unsupported in Lean 4: #[`surj] [] -/
+/- ./././Mathport/Syntax/Translate/Command.lean:393:30: infer kinds are unsupported in Lean 4: #[`eq_iff_exists] [] -/
 /-- The characteristic predicate for localized module.
 `is_localized_module S f` describes that `f : M ⟶ M'` is the localization map identifying `M'` as
 `localized_module S M`.

Mathbin/Algebra/Order/AbsoluteValue.lean

@@ -460,10 +460,10 @@ end LinearOrderedCommRing
 end AbsoluteValue
 
 #print IsAbsoluteValue /-
-/- ./././Mathport/Syntax/Translate/Command.lean:388:30: infer kinds are unsupported in Lean 4: #[`abv_nonneg] [] -/
-/- ./././Mathport/Syntax/Translate/Command.lean:388:30: infer kinds are unsupported in Lean 4: #[`abv_eq_zero] [] -/
-/- ./././Mathport/Syntax/Translate/Command.lean:388:30: infer kinds are unsupported in Lean 4: #[`abv_add] [] -/
-/- ./././Mathport/Syntax/Translate/Command.lean:388:30: infer kinds are unsupported in Lean 4: #[`abv_mul] [] -/
+/- ./././Mathport/Syntax/Translate/Command.lean:393:30: infer kinds are unsupported in Lean 4: #[`abv_nonneg] [] -/
+/- ./././Mathport/Syntax/Translate/Command.lean:393:30: infer kinds are unsupported in Lean 4: #[`abv_eq_zero] [] -/
+/- ./././Mathport/Syntax/Translate/Command.lean:393:30: infer kinds are unsupported in Lean 4: #[`abv_add] [] -/
+/- ./././Mathport/Syntax/Translate/Command.lean:393:30: infer kinds are unsupported in Lean 4: #[`abv_mul] [] -/
 /-- A function `f` is an absolute value if it is nonnegative, zero only at 0, additive, and
 multiplicative.
 

Mathbin/Algebra/Order/CompleteField.lean

@@ -56,12 +56,12 @@ open Function Rat Real Set
 
 open Classical Pointwise
 
-/- ./././Mathport/Syntax/Translate/Command.lean:417:11: unsupported: advanced extends in structure -/
+/- ./././Mathport/Syntax/Translate/Command.lean:422:11: unsupported: advanced extends in structure -/
 /-- A field which is both linearly ordered and conditionally complete with respect to the order.
 This axiomatizes the reals. -/
 @[protect_proj]
 class ConditionallyCompleteLinearOrderedField (α : Type _) extends
-  "./././Mathport/Syntax/Translate/Command.lean:417:11: unsupported: advanced extends in structure",
+  "./././Mathport/Syntax/Translate/Command.lean:422:11: unsupported: advanced extends in structure",
   ConditionallyCompleteLinearOrder α
 #align conditionally_complete_linear_ordered_field ConditionallyCompleteLinearOrderedField
 

Mathbin/Algebra/Quaternion.lean

@@ -55,7 +55,7 @@ quaternion
 -/
 
 
-/- ./././Mathport/Syntax/Translate/Command.lean:424:34: infer kinds are unsupported in Lean 4: mk {} -/
+/- ./././Mathport/Syntax/Translate/Command.lean:429:34: infer kinds are unsupported in Lean 4: mk {} -/
 /-- Quaternion algebra over a type with fixed coefficients $a=i^2$ and $b=j^2$.
 Implemented as a structure with four fields: `re`, `im_i`, `im_j`, and `im_k`. -/
 @[nolint unused_arguments, ext]

Mathbin/Algebra/Ring/BooleanRing.lean

@@ -191,9 +191,9 @@ def hasInf : Inf α :=
 #align boolean_ring.has_inf BooleanRing.hasInf
 
 scoped[-- Note [lower instance priority]
-BooleanAlgebraOfBooleanRing] attribute [instance] BooleanRing.hasSup
+BooleanAlgebraOfBooleanRing] attribute [instance 100] BooleanRing.hasSup
 
-scoped[BooleanAlgebraOfBooleanRing] attribute [instance] BooleanRing.hasInf
+scoped[BooleanAlgebraOfBooleanRing] attribute [instance 100] BooleanRing.hasInf
 
 theorem sup_comm (a b : α) : a ⊔ b = b ⊔ a :=
   by
@@ -279,7 +279,7 @@ def toBooleanAlgebra : BooleanAlgebra α :=
       rw [← add_assoc, add_self] }
 #align boolean_ring.to_boolean_algebra BooleanRing.toBooleanAlgebra
 
-scoped[BooleanAlgebraOfBooleanRing] attribute [instance] BooleanRing.toBooleanAlgebra
+scoped[BooleanAlgebraOfBooleanRing] attribute [instance 100] BooleanRing.toBooleanAlgebra
 
 end BooleanRing
 
@@ -499,7 +499,8 @@ def BooleanAlgebra.toBooleanRing : BooleanRing α :=
 #align boolean_algebra.to_boolean_ring BooleanAlgebra.toBooleanRing
 
 scoped[BooleanRingOfBooleanAlgebra]
-  attribute [instance] GeneralizedBooleanAlgebra.toNonUnitalCommRing BooleanAlgebra.toBooleanRing
+  attribute [instance 100]
+    GeneralizedBooleanAlgebra.toNonUnitalCommRing BooleanAlgebra.toBooleanRing
 
 instance : BooleanRing (AsBoolring α) :=
   @BooleanAlgebra.toBooleanRing α _

Mathbin/AlgebraicGeometry/Scheme.lean

@@ -35,15 +35,15 @@ open Opposite
 
 namespace AlgebraicGeometry
 
-/- ./././Mathport/Syntax/Translate/Command.lean:417:11: unsupported: advanced extends in structure -/
+/- ./././Mathport/Syntax/Translate/Command.lean:422:11: unsupported: advanced extends in structure -/
 /-- We define `Scheme` as a `X : LocallyRingedSpace`,
 along with a proof that every point has an open neighbourhood `U`
 so that that the restriction of `X` to `U` is isomorphic,
 as a locally ringed space, to `Spec.to_LocallyRingedSpace.obj (op R)`
 for some `R : CommRing`.
 -/
 structure Scheme extends
-  "./././Mathport/Syntax/Translate/Command.lean:417:11: unsupported: advanced extends in structure" where
+  "./././Mathport/Syntax/Translate/Command.lean:422:11: unsupported: advanced extends in structure" where
   local_affine :
     ∀ x : to_LocallyRingedSpace,
       ∃ (U : OpenNhds x)(R : CommRingCat),

Mathbin/AlgebraicTopology/FundamentalGroupoid/SimplyConnected.lean

@@ -34,7 +34,7 @@ open ContinuousMap
 
 open ContinuousMap
 
-/- ./././Mathport/Syntax/Translate/Command.lean:388:30: infer kinds are unsupported in Lean 4: #[`equiv_unit] [] -/
+/- ./././Mathport/Syntax/Translate/Command.lean:393:30: infer kinds are unsupported in Lean 4: #[`equiv_unit] [] -/
 /-- A simply connected space is one whose fundamental groupoid is equivalent to `discrete unit` -/
 class SimplyConnectedSpace (X : Type _) [TopologicalSpace X] : Prop where
   equiv_unit : Nonempty (FundamentalGroupoid X ≌ Discrete Unit)

Mathbin/AlgebraicTopology/SimplexCategory.lean

@@ -43,7 +43,7 @@ universe v
 
 open CategoryTheory CategoryTheory.Limits
 
-/- ./././Mathport/Syntax/Translate/Command.lean:318:31: unsupported: @[derive, irreducible] def -/
+/- ./././Mathport/Syntax/Translate/Command.lean:323:31: unsupported: @[derive, irreducible] def -/
 #print SimplexCategory /-
 /-- The simplex category:
 * objects are natural numbers `n : ℕ`

Mathbin/Analysis/Calculus/ContDiff.lean

@@ -40,7 +40,7 @@ local notation "∞" => (⊤ : ℕ∞)
 
 universe u v w uD uE uF uG
 
-attribute [local instance]
+attribute [local instance 1001]
   NormedAddCommGroup.toAddCommGroup NormedSpace.toModule' AddCommGroup.toAddCommMonoid
 
 namespace Finset

Mathbin/Analysis/Calculus/ContDiffDef.lean

@@ -167,7 +167,7 @@ open Classical BigOperators NNReal Topology
 -- mathport name: «expr∞»
 local notation "∞" => (⊤ : ℕ∞)
 
-attribute [local instance]
+attribute [local instance 1001]
   NormedAddCommGroup.toAddCommGroup NormedSpace.toModule' AddCommGroup.toAddCommMonoid
 
 open Set Fin Filter Function

Mathbin/Analysis/InnerProductSpace/Adjoint.lean

@@ -371,7 +371,7 @@ namespace LinearMap
 
 variable [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] [FiniteDimensional 𝕜 G]
 
-attribute [local instance] FiniteDimensional.complete
+attribute [local instance 20] FiniteDimensional.complete
 
 /-- The adjoint of an operator from the finite-dimensional inner product space E to the finite-
 dimensional inner product space F. -/

Mathbin/Analysis/NormedSpace/Enorm.lean

@@ -38,7 +38,7 @@ normed space, extended norm
 
 noncomputable section
 
-attribute [local instance] Classical.propDecidable
+attribute [local instance 1001] Classical.propDecidable
 
 open ENNReal
 

Mathbin/Analysis/NormedSpace/Multilinear.lean

@@ -65,7 +65,7 @@ open BigOperators NNReal
 
 open Finset Metric
 
-attribute [local instance]
+attribute [local instance 1001]
   AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule'
 
 /-!

Mathbin/CategoryTheory/Abelian/Basic.lean

@@ -120,9 +120,9 @@ class Abelian extends Preadditive C, NormalMonoCategory C, NormalEpiCategory C w
 #align category_theory.abelian CategoryTheory.Abelian
 -/
 
-attribute [instance] abelian.has_finite_products
+attribute [instance 100] abelian.has_finite_products
 
-attribute [instance] abelian.has_kernels abelian.has_cokernels
+attribute [instance 100] abelian.has_kernels abelian.has_cokernels
 
 end CategoryTheory
 

Mathbin/CategoryTheory/Bicategory/Basic.lean

@@ -54,11 +54,11 @@ universe w v u
 open Category Iso
 
 #print CategoryTheory.Bicategory /-
-/- ./././Mathport/Syntax/Translate/Command.lean:401:24: unsupported: (notation) in structure -/
-/- ./././Mathport/Syntax/Translate/Command.lean:401:24: unsupported: (notation) in structure -/
-/- ./././Mathport/Syntax/Translate/Command.lean:401:24: unsupported: (notation) in structure -/
-/- ./././Mathport/Syntax/Translate/Command.lean:401:24: unsupported: (notation) in structure -/
-/- ./././Mathport/Syntax/Translate/Command.lean:401:24: unsupported: (notation) in structure -/
+/- ./././Mathport/Syntax/Translate/Command.lean:406:24: unsupported: (notation) in structure -/
+/- ./././Mathport/Syntax/Translate/Command.lean:406:24: unsupported: (notation) in structure -/
+/- ./././Mathport/Syntax/Translate/Command.lean:406:24: unsupported: (notation) in structure -/
+/- ./././Mathport/Syntax/Translate/Command.lean:406:24: unsupported: (notation) in structure -/
+/- ./././Mathport/Syntax/Translate/Command.lean:406:24: unsupported: (notation) in structure -/
 /- ./././Mathport/Syntax/Translate/Expr.lean:207:4: warning: unsupported notation `«expr ◁ » -/
 /- ./././Mathport/Syntax/Translate/Expr.lean:207:4: warning: unsupported notation `«expr ◁ » -/
 /- ./././Mathport/Syntax/Translate/Expr.lean:207:4: warning: unsupported notation `«expr ◁ » -/

Mathbin/CategoryTheory/Bicategory/CoherenceTactic.lean

@@ -103,7 +103,7 @@ instance liftHom₂WhiskerRight {f g : a ⟶ b} (η : f ⟶ g) [LiftHom f] [Lift
     {h : b ⟶ c} [LiftHom h] : LiftHom₂ (η ▷ h) where lift := LiftHom₂.lift η ▷ LiftHom.lift h
 #align category_theory.bicategory.lift_hom₂_whisker_right CategoryTheory.Bicategory.liftHom₂WhiskerRight
 
-/- ./././Mathport/Syntax/Translate/Command.lean:388:30: infer kinds are unsupported in Lean 4: #[`Hom] [] -/
+/- ./././Mathport/Syntax/Translate/Command.lean:393:30: infer kinds are unsupported in Lean 4: #[`Hom] [] -/
 /-- A typeclass carrying a choice of bicategorical structural isomorphism between two objects.
 Used by the `⊗≫` bicategorical composition operator, and the `coherence` tactic.
 -/

Mathbin/CategoryTheory/Closed/Ideal.lean

@@ -115,7 +115,7 @@ theorem reflective_products [HasFiniteProducts C] [Reflective i] : HasFiniteProd
   ⟨fun n => hasLimitsOfShape_of_reflective i⟩
 #align category_theory.reflective_products CategoryTheory.reflective_products
 
-attribute [local instance] reflective_products
+attribute [local instance 10] reflective_products
 
 open CartesianClosed