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

chore: tinker with some wording in Implication world

Browse Source
This commit is contained in:
Kevin Buzzard
2025-02-15 15:03:16 +00:00
parent 49f1a33406
commit cdb7060ad1
2 changed files with 6 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files

7
Game/Levels/Implication/L03apply.lean
View File

@@ -39,8 +39,11 @@ NewTactic apply
Introduction
"
In this level one of our hypotheses is an *implication*. We can use this
hypothesis with the `apply` tactic.
In this level, the hypotheses `h2` is an *implication*. It says
that *if* `x = 37` *then* `y = 42`. We can use this
hypothesis with the `apply` tactic. Remember you can click on
`apply` or any other tactic on the right to see a detailed explanation
of what it does, with examples.
"
/-- If $x=37$ and we know that $x=37\implies y=42$ then we can deduce $y=42$. -/

2
Game/Levels/Implication/L07intro2.lean
View File

@@ -16,7 +16,7 @@ Statement (x : ℕ) : x + 1 = y + 1 → x = y := by
Hint (hidden := true) "Start with `intro h` to assume the hypothesis."
intro h
Hint (hidden := true) "Now `repeat rw [← succ_eq_add_one] at h` is the quickest way to
change `succ x = succ y`."
change `h` to `succ x = succ y`."
repeat rw [← succ_eq_add_one] at h
Hint (hidden := true) "Now `apply succ_inj at h` to cancel the `succ`s."
apply succ_inj at h