fix nth_rewrite warning

leanprover-community · Jan 24, 2024 · 270a98c · 270a98c
1 parent e180fc9
commit 270a98c
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 16 deletions.
diff --git a/Game/Levels/Tutorial/L02rw.lean b/Game/Levels/Tutorial/L02rw.lean
@@ -138,6 +138,20 @@ will change the goal to `succ 1 + succ 1 = 4`.
 -/
 TacticDoc «repeat»
 
+/--
+## Summary
+
+If `h : X = Y` and there are several `X`s in the goal, then
+`nth_rewrite 3 [h]` will just change the third `X` to a `Y`.
+
+## Example
+
+If the goal is `2 + 2 = 4` then `nth_rewrite 2 [two_eq_succ_one]`
+will change the goal to `2 + succ 1 = 4`. In contrast, `rw [two_eq_succ_one]`
+will change the goal to `succ 1 + succ 1 = 4`.
+-/
+TacticDoc nth_rewrite
+
 NewTactic rw
 
 NewHiddenTactic «repeat» nth_rewrite

diff --git a/Game/Levels/Tutorial/L08twoaddtwo.lean b/Game/Levels/Tutorial/L08twoaddtwo.lean
@@ -10,22 +10,6 @@ TheoremTab "012"
 
 namespace MyNat
 
-/--
-## Summary
-
-If `h : X = Y` and there are several `X`s in the goal, then
-`nth_rewrite 3 [h]` will just change the third `X` to a `Y`.
-
-## Example
-
-If the goal is `2 + 2 = 4` then `nth_rewrite 2 [two_eq_succ_one]`
-will change the goal to `2 + succ 1 = 4`. In contrast, `rw [two_eq_succ_one]`
-will change the goal to `succ 1 + succ 1 = 4`.
--/
-TacticDoc nth_rewrite
-
-NewHiddenTactic nth_rewrite
-
 Introduction
 " Good luck!