doc: swap sides of equality in grind (#841)

This PR update's @adomani's bug fix in #512 to the current manual, and
corrects a related bug — the mentions of `grind` should be `grind!`,
given that grind now has minimal-indexing and maximal-indexing variants.

Author: robsimmons

Manual/Grind/EMatching.lean

@@ -685,18 +685,18 @@ axiom q : Nat → Nat
 ```
 
 ```lean (name := h1)
-@[grind!? →] theorem h₁ (w : 7 = p (q x)) : p (x + 1) = q x := sorry
+@[grind!? →] theorem h₁ (w : p (q x) = 7) : p (x + 1) = q x := sorry
 ```
 ```leanOutput h1
 h₁: [q #1]
 ```
 The pattern is `q x`.
 Counting from the right, parameter `#0` is the premise `w` and parameter `#1` is the implicit parameter `x`.
 
-Why did `@[grind →]`? select `q #1`?
-The attribute `@[grind →]` finds patterns by traversing the hypotheses (that is, parameters whose types are propositions) from left to right.
-In this case, there's only a single hypothesis: `7 = p (q x)`.
-The heuristic described above says that {attr}`grind` will search for a minimal {tech}[indexable] subexpression which {tech}[covers] a previously uncovered parameter.
+Why did `@[grind! →]`? select `q #1`?
+The attribute `@[grind! →]` finds patterns by traversing the hypotheses (that is, parameters whose types are propositions) from left to right.
+In this case, there's only a single hypothesis: `p (q x) = 7`.
+The heuristic described above says that {attr}`grind!` will search for a minimal {tech}[indexable] subexpression which {tech}[covers] a previously uncovered parameter.
 There's just one uncovered parameter, namely `x`.
 The whole hypothesis `p (q x) = 7` can't be used because {tactic}`grind` will not index on equality.
 The right-hand side `7` is not helpful, because it doesn't determine the value of `x`.