another adaptation note

Author: kim-em

Mathlib/Analysis/Normed/Operator/Banach.lean

@@ -130,7 +130,13 @@ theorem exists_approx_preimage_norm_le (surj : Surjective f) :
           simp only [x, f.map_sub]
           abel
         _ ≤ ‖f x₁ - (a + d • y)‖ + ‖f x₂ - a‖ := norm_sub_le _ _
-        _ ≤ 2 * δ := by grind [dist_eq_norm']
+        #adaptation_note
+        /--
+        These next two steps were `_ ≤ 2 * δ := by grind [dist_eq_norm']` until nightly-2025-11-28.
+        The problem is https://github.com/leanprover/lean4/pull/11410
+        -/
+        _ ≤ δ + δ := by rw [dist_eq_norm'] at h₁ h₂; gcongr
+        _ = 2 * δ := (two_mul _).symm
     have J : ‖f (σ' d⁻¹ • x) - y‖ ≤ 1 / 2 * ‖y‖ :=
       calc
         ‖f (σ' d⁻¹ • x) - y‖ = ‖d⁻¹ • f x - (d⁻¹ * d) • y‖ := by