Porting note: was `infer_instance`

[pitmonticone]

Classifies porting notes claiming:

was infer_instance

Examples

mathlib4/Mathlib/Algebra/Category/FGModuleCat/Basic.lean

Lines 186 to 202 in 2a65c8d

	instance forget₂Monoidal_faithful : Faithful (forget₂Monoidal R).toFunctor := by
	dsimp [forget₂Monoidal]
	-- Porting note: was `infer_instance`
	exact FullSubcategory.faithful _
	#align fgModule.forget₂_monoidal_faithful FGModuleCat.forget₂Monoidal_faithful
	instance forget₂Monoidal_additive : (forget₂Monoidal R).toFunctor.Additive := by
	dsimp [forget₂Monoidal]
	-- Porting note: was `infer_instance`
	exact Functor.fullSubcategoryInclusion_additive _
	#align fgModule.forget₂_monoidal_additive FGModuleCat.forget₂Monoidal_additive
	instance forget₂Monoidal_linear : (forget₂Monoidal R).toFunctor.Linear R := by
	dsimp [forget₂Monoidal]
	-- Porting note: was `infer_instance`
	exact Functor.fullSubcategoryInclusionLinear _ _
	#align fgModule.forget₂_monoidal_linear FGModuleCat.forget₂Monoidal_linear

[YaelDillies]

This issue is not referred to explicitly anywhere, but it actually is still relevant: See pullback_snd_isIso_of_range_subset.