doc: fix case syntax in mvcgen docs (#13745)

frangio · web-flow · commit df865dfccae2 · 2026-05-30T08:44:43.000Z
This PR fixes a syntax error in `mvcgen` documentation.
diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
@@ -2300,8 +2300,8 @@ options. Of particular note is `stepLimit = some 42`, which is useful for bisect
 Often, `mvcgen` will be used like this:
 ```
 mvcgen [...]
-case inv1 => by exact I1
-case inv2 => by exact I2
+case inv1 => exact I1
+case inv2 => exact I2
 all_goals (mleave; try grind)
 ```
 There is special syntax for this:
