Porting note: added `instance`

[pitmonticone]

Classifies porting notes claiming anything semantically equivalent to:

• "added instance"
• "new instance"
• "adding instance"
• "had to add this instance manually"

Examples

mathlib4/Mathlib/RingTheory/Valuation/ValuationSubring.lean

Lines 309 to 316 in 4c3321a

	instance ofPrime_scalar_tower (A : ValuationSubring K) (P : Ideal A) [P.IsPrime] :
	-- Porting note: added instance
	letI : SMul A (A.ofPrime P) := SMulZeroClass.toSMul
	IsScalarTower A (A.ofPrime P) K :=
	IsScalarTower.subalgebra' A K K
	-- Porting note: filled in the argument
	(Localization.subalgebra.ofField K _ P.primeCompl_le_nonZeroDivisors)
	#align valuation_subring.of_prime_scalar_tower ValuationSubring.ofPrime_scalar_tower

mathlib4/Archive/Arithcc.lean

Lines 252 to 254 in 4c3321a

	-- Porting note: added
	instance (t : Register) : Trans (StateEq (t + 1)) (StateEq (t + 1)) (StateEq (t + 1)) :=
	⟨@StateEq.trans _⟩

mathlib4/Archive/Arithcc.lean

Lines 264 to 266 in 4c3321a

	-- Porting note: added
	instance (t : Register) : Trans (StateEq (t + 1)) (StateEqRs (t + 1)) (StateEqRs (t + 1)) :=
	⟨@StateEqStateEqRs.trans _⟩