chore: discharge porting note about 'change ... at' (#9018)

`RingTheory.Adjoin.Basic` was ported in #2817.
`change ... at` was added in #2836.

Mathlib/RingTheory/Adjoin/Basic.lean

@@ -364,8 +364,7 @@ variable {R}
 theorem pow_smul_mem_of_smul_subset_of_mem_adjoin [CommSemiring B] [Algebra R B] [Algebra A B]
     [IsScalarTower R A B] (r : A) (s : Set B) (B' : Subalgebra R B) (hs : r • s ⊆ B') {x : B}
     (hx : x ∈ adjoin R s) (hr : algebraMap A B r ∈ B') : ∃ n₀ : ℕ, ∀ n ≥ n₀, r ^ n • x ∈ B' := by
-  -- porting note: use `replace` because we don't have `change ... at` yet
-  replace hx : x ∈ Subalgebra.toSubmodule (adjoin R s) := hx
+  change x ∈ Subalgebra.toSubmodule (adjoin R s) at hx
   rw [adjoin_eq_span, Finsupp.mem_span_iff_total] at hx
   rcases hx with ⟨l, rfl : (l.sum fun (i : Submonoid.closure s) (c : R) => c • (i : B)) = x⟩
   choose n₁ n₂ using fun x : Submonoid.closure s => Submonoid.pow_smul_mem_closure_smul r s x.prop