Merge pull request #73 from mcol/typos

Fix typos.
leanprover-community · Jul 4, 2024 · 7400b12 · 7400b12
2 parents bfaf125 + 8a563cf
commit 7400b12
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/Game/Levels/AdvMultiplication/L06mul_right_eq_one.lean b/Game/Levels/AdvMultiplication/L06mul_right_eq_one.lean
@@ -74,7 +74,7 @@ Statement mul_right_eq_one (x y : ℕ) (h : x * y = 1) : x = 1 := by
   exact one_ne_zero
   Hint (hidden := true) "Now you can `apply le_mul_right at h2`."
   apply le_mul_right at h2
-  Hint (hidden := true) "Now `rw [h] at h2` so you can `apply le_one at hx`."
+  Hint (hidden := true) "Now `rw [{h}] at {h2}` so you can `apply le_one at {h2}`."
   rw [h] at h2
   apply le_one at h2
   Hint (hidden := true) "Now `cases h2 with h0 h1` and deal with the two

diff --git a/Game/Levels/Tutorial/L02rw.lean b/Game/Levels/Tutorial/L02rw.lean
@@ -77,7 +77,7 @@ are two distinct situations where you can use this tactic.
 
 1) Basic usage: if `h : A = B` is an assumption or
 the proof of a theorem, and if the goal contains one or more `A`s, then `rw [h]`
-will change them all to `B`'s. The tactic will error
+will change them all to `B`s. The tactic will error
 if there are no `A`s in the goal.
 
 2) Advanced usage: Assumptions coming from theorem proofs