chore: cleanup a change at porting note (#5243)

Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>

Mathlib/Algebra/Order/AbsoluteValue.lean

@@ -16,9 +16,6 @@ import Mathlib.Algebra.Ring.Regular
 /-!
 # Absolute values
 
-> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
-> Any changes to this file require a corresponding PR to mathlib4.
-
 This file defines a bundled type of absolute values `AbsoluteValue R S`.
 
 ## Main definitions

Mathlib/LinearAlgebra/Basis.lean

@@ -1103,9 +1103,7 @@ theorem maximal [Nontrivial R] (b : Basis ι R M) : b.linearIndependent.Maximal
     ⟨fun i => ⟨b i, h ⟨i, rfl⟩⟩, fun i i' r =>
       b.injective (by simpa only [Subtype.mk_eq_mk] using r)⟩
   simp_rw [Finsupp.total_apply] at e
-  -- Porting note: `change at` doesn't work
-  replace e : ((b.repr x).sum fun (i : ι) (a : R) ↦ a • (u i : M)) =
-      ((⟨x, p⟩ : w) : M) := e
+  change ((b.repr x).sum fun (i : ι) (a : R) ↦ a • (u i : M)) = ((⟨x, p⟩ : w) : M) at e
   rw [← Finsupp.sum_embDomain (f := u) (g := fun x r ↦ r • (x : M)), ← Finsupp.total_apply] at e
   -- Now we can contradict the linear independence of `hi`
   refine' hi.total_ne_of_not_mem_support _ _ e

Mathlib/NumberTheory/Padics/PadicNumbers.lean

@@ -663,7 +663,8 @@ theorem rat_dense' (q : ℚ_[p]) {ε : ℚ} (hε : 0 < ε) : ∃ r : ℚ, padicN
     let ⟨N, hN⟩ := this
     ⟨q' N, by
       dsimp [padicNormE]
-      -- Porting note: `change` → `convert_to` and `PadicSeq p` type annotation
+      -- Porting note: `change` → `convert_to` (`change` times out!)
+      -- and add `PadicSeq p` type annotation
       convert_to PadicSeq.norm (q' - const _ (q' N) : PadicSeq p) < ε
       cases' Decidable.em (q' - const (padicNorm p) (q' N) ≈ 0) with heq hne'
       · simpa only [heq, PadicSeq.norm, dif_pos]