From c10d255b159e1ea7ee512f3a18ad49b30a3ccfba Mon Sep 17 00:00:00 2001 From: jaredcosulich Date: Wed, 19 Jun 2024 15:36:11 -0400 Subject: [PATCH] I got confused with how `use` works, assuming it required an explicit natural number (e.g. 37). Tweaking the docs to make it more clear that `use` accepts more than just natural numbers. --- Game/Levels/LessOrEqual/L01le_refl.lean | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/Game/Levels/LessOrEqual/L01le_refl.lean b/Game/Levels/LessOrEqual/L01le_refl.lean index a27e6b5..609cb70 100644 --- a/Game/Levels/LessOrEqual/L01le_refl.lean +++ b/Game/Levels/LessOrEqual/L01le_refl.lean @@ -18,7 +18,13 @@ that `x = 37` will work, then `use 37` will make progress. Because `a ≤ b` is notation for \"there exists `c` such that `b = a + c`\", you can make progress on goals of the form `a ≤ b` by `use`ing the -number which is morally `b - a`. +number which is morally `b - a` (i.e. `use b - a`) + +Any of the following examples is possible assuming the type of the argument passed to the `use` function is accurate: + +- `use 37` +- `use a` +- `use a * a + 1` -/ TacticDoc use