diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index 26b71f6180..1517f65795 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -1752,7 +1752,7 @@ attribute @[simp ←] and_assoc
 ```
 
 When multiple simp theorems are applicable, the simplifier uses the one with highest priority.
-The equational theorems of function are applied at very low priority (100 and below).
+The equational theorems of functions are applied at very low priority (100 and below).
 If there are several with the same priority, it is uses the "most recent one". Example:
 ```lean
 @[simp high] theorem cond_true (a b : α) : cond true a b = a := rfl