greg/NNG
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Fix typos.

Browse Source
This commit is contained in:
Marco Colombo
2024-07-03 17:18:39 +02:00
parent bfaf1259a2
commit 281d35e200
2 changed files with 2 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
Game/Levels/AdvMultiplication/L06mul_right_eq_one.lean
View File

@@ -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

2
Game/Levels/Tutorial/L02rw.lean
View File

@@ -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