chore: fix grammar in abel,field_simp error message (leanprover-community#37898)

Extracted from leanprover-community#31597.

Author: grunweg

Mathlib/Util/AtLocation.lean

@@ -56,7 +56,7 @@ def transformAtTarget (m : Expr → ReaderT Simp.Context MetaM Simp.Result) (pro
   -- we use expression equality here (rather than defeq) to be consistent with, e.g.,
   -- `applySimpResultToTarget`
   let unchanged := tgt.cleanupAnnotations == r.expr.cleanupAnnotations
-  if failIfUnchanged && unchanged then throwError "{proc} made no progress on goal"
+  if failIfUnchanged && unchanged then throwError "{proc} made no progress on the goal"
   if r.expr.isTrue then
     goal.assign (← mkOfEqTrue (← r.getProof))
     pure none

MathlibTest/FieldSimp.lean

@@ -29,7 +29,7 @@ section
 
 variable {P : ℚ → Prop} {x y z : ℚ}
 
-/-- error: `field_simp` made no progress on goal -/
+/-- error: `field_simp` made no progress on the goal -/
 #guard_msgs in
 example : P (1 : ℚ) := by test_field_simp
 
@@ -43,7 +43,7 @@ example : P (x ^ 0) := by test_field_simp
 #guard_msgs in
 example : P (x ^ 1) := by test_field_simp
 
-/-- error: `field_simp` made no progress on goal -/
+/-- error: `field_simp` made no progress on the goal -/
 #guard_msgs in
 example : P x := by test_field_simp
 
@@ -181,7 +181,7 @@ example {a : Nat} : P (a* x - a * x) := by test_field_simp
 
 /-! ### Two atoms -/
 
-/-- error: `field_simp` made no progress on goal -/
+/-- error: `field_simp` made no progress on the goal -/
 #guard_msgs in
 example : P (x + y) := by test_field_simp
 
@@ -959,7 +959,7 @@ example {K : Type} [Semifield K] {x y : K} (h : x + y ≠ 0) : x / (x + y) + y /
 -- Extracted from `Mathlib/Analysis/SpecificLimits/Basic.lean`
 
 -- `field_simp` assumes commutativity: in its absence, it does nothing.
-/-- error: `field_simp` made no progress on goal -/
+/-- error: `field_simp` made no progress on the goal -/
 #guard_msgs in
 example {K : Type*} [DivisionRing K] {n' x : K} (h : n' ≠ 0) (h' : n' + x ≠ 0) :
     1 / (1 + x / n') = n' / (n' + x) := by

MathlibTest/abel.lean

@@ -58,7 +58,7 @@ example [AddCommGroup α] (a b c : α) :
 def MyTrue := True
 
 /--
-error: `abel_nf` made no progress on goal
+error: `abel_nf` made no progress on the goal
 -/
 #guard_msgs in
 example : MyTrue := by
@@ -87,14 +87,14 @@ example [AddCommGroup α] (x y z : α) : y = x + z - (x - y + z) := by
 example [AddCommGroup α] (a b s : α) : -b + (s - a) = s - b - a := by abel_nf
 
 -- inspired by automated testing
-/-- error: `abel_nf` made no progress on goal -/
+/-- error: `abel_nf` made no progress on the goal -/
 #guard_msgs in
 example : True := by
   have := 0
   abel_nf
 
 /--
-error: `abel_nf` made no progress on goal
+error: `abel_nf` made no progress on the goal
 -/
 #guard_msgs in
 example : False := by abel_nf
@@ -149,7 +149,7 @@ example [AddCommGroup α] (x y z : α) (w : x = y + z) : x - x = 0 := by
   abel_nf at w ⊢
 
 /--
-error: `abel_nf` made no progress on goal
+error: `abel_nf` made no progress on the goal
 -/
 #guard_msgs in
 example [AddCommGroup α] (x y z : α) (w : x - x = y + z) : x = 0 := by