Porting note: removed @[nolint has_nonempty_instance]

[pitmonticone]

Classifies porting notes claiming removed @[nolint has_nonempty_instance].

Examples

mathlib4/Mathlib/AlgebraicTopology/SimplicialObject.lean

Lines 39 to 44 in d3dbfd9

	-- porting note: removed @[nolint has_nonempty_instance]
	/-- The category of simplicial objects valued in a category `C`.
	This is the category of contravariant functors from `SimplexCategory` to `C`. -/
	def SimplicialObject :=
	SimplexCategoryᵒᵖ ⥤ C
	#align category_theory.simplicial_object CategoryTheory.SimplicialObject

mathlib4/Mathlib/AlgebraicTopology/SimplicialObject.lean

Lines 411 to 415 in d3dbfd9

	-- porting note: removed @[nolint has_nonempty_instance]
	/-- Cosimplicial objects. -/
	def CosimplicialObject :=
	SimplexCategory ⥤ C
	#align category_theory.cosimplicial_object CategoryTheory.CosimplicialObject

mathlib4/Mathlib/CategoryTheory/CommSq.lean

Lines 112 to 121 in d3dbfd9

	-- Porting note: removed @[nolint has_nonempty_instance]
	@[ext]
	structure LiftStruct (sq : CommSq f i p g) where
	/-- The lift. -/
	l : B ⟶ X
	/-- The upper left triangle commutes. -/
	fac_left : i ≫ l = f
	/-- The lower right triangle commutes. -/
	fac_right: l ≫ p = g
	#align category_theory.comm_sq.lift_struct CategoryTheory.CommSq.LiftStruct

[grunweg]

This is a special case of porting notes caused by #5171; does it make sense to reference that issue instead?

[grunweg]

I have changed all references to point to #5171 instead; let me close this issue. Thanks for classifying all these!