Martin Leduc
bc07e36688
Fix terminology in L02rw.lean ( #81 )
...
According to TPIL we "rewrite the goal using a hypothesis".
2025-09-27 14:40:47 +01:00
Jon Eugster
aaac232f5c
Merge pull request #117 from dharmatech/patch-1
...
Typo: remove extra word `to`
2025-09-27 09:47:52 +02:00
dharmatech
e6e15d8b07
Typo: remove extra word to
2025-09-26 22:17:35 -07:00
Yu-Ting Hsiung
ad57f687c0
Fix typo in Game
2025-09-27 11:57:21 +08:00
Jon Eugster
869e254313
Merge pull request #112 from leanprover-community/fix/adjust-hint
...
fix: adjust hint text
2025-09-23 22:57:12 +02:00
Jon Eugster
1e99f52a29
Merge pull request #100 from cjl8zf/cjl8zf-L07or_symm.lean-made-to-make
...
Small Typo Fix In L07or_symm.lean
2025-09-23 22:57:03 +02:00
Jon Eugster
a1375414fa
Merge pull request #107 from arnbod/small-typo
...
Remove extra space, that prevent translation
2025-09-23 22:56:36 +02:00
Jon Eugster
65829e27da
fix: adjust hint text
2025-09-23 22:44:17 +02:00
Jon Eugster
3558f5bfb6
bump v4.22.0
2025-08-30 00:44:07 +02:00
Arnaud
71e5424a17
Remove extra space, that prevent translation
2025-07-11 14:00:36 +02:00
Chris Lloyd
2f04b8be63
Small Typo Fix In L07or_symm.lean
...
If you have an "or" statement in the goal, then two tactics make (instead of "made") progress: left and right.
2025-06-15 17:13:25 -04:00
Kevin Buzzard
36a82b7cfd
doc: add conclusion for adv multn L8
2025-02-17 10:09:59 +00:00
Kevin Buzzard
a59282f10b
docs: more tauto docstring
2025-02-15 16:52:55 +00:00
Kevin Buzzard
88021db205
docs: more hints in advanced multiplication L5
2025-02-15 16:48:31 +00:00
Kevin Buzzard
7fef0ec666
docs: add to tauto docstring
2025-02-15 16:38:19 +00:00
Kevin Buzzard
f4611f9bc2
docs: add snarky comment about even/odd world
2025-02-15 16:32:27 +00:00
Kevin Buzzard
cdb7060ad1
chore: tinker with some wording in Implication world
2025-02-15 15:03:16 +00:00
Kevin Buzzard
49f1a33406
more realistic claims about prime number world
2025-02-01 23:24:33 +00:00
Hans Christian Schmitz
47e9945ff9
Fix typo in contrapose! h explainer in Algo L7
...
The explainer mistakenly swapped an n for an m, possibly causing
confusion with the explainer mentioning a different hypothesis than the one
resulting from the tactic, and one from which alone one cannot derive
the new goal.
2025-01-17 08:02:52 +01:00
Jon Eugster
66b27f382a
Merge pull request #64 from yannickseurin/add_right_eq_self
...
alternate proof for `add_right_eq_self`
2024-08-28 23:51:30 +02:00
Marco Colombo
8a563cf6f4
Fix hint.
2024-07-04 17:02:25 +02:00
Marco Colombo
281d35e200
Fix typos.
2024-07-03 17:18:39 +02:00
Ughur Alakbarov
0d828eda14
Fix quoting
2024-06-29 12:37:32 +02:00
jaredcosulich
c10d255b15
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.
2024-06-19 15:36:11 -04:00
Yannick Seurin
5d25d0f598
typo in L06mul_right_eq_one.lean
2024-06-14 12:08:33 +02:00
Yannick Seurin
9bc59952a8
typo in L05le_mul_right.lean
2024-06-14 11:47:56 +02:00
Yannick Seurin
08b488b32b
typo in L03eq_succ_of_ne_zero.lean
2024-06-14 11:41:47 +02:00
Yannick Seurin
2ba1b7084b
alternate proof for add_right_eq_self
2024-06-12 14:40:24 +02:00
Yannick Seurin
47e143cd67
Update L08pow_pow.lean
2024-06-12 14:38:20 +02:00
Yannick Seurin
fb90bad32c
typo in L07mul_pow.lean
2024-06-12 14:37:49 +02:00
Yannick Seurin
fbf69505fb
typo in L08ne.lean
2024-06-11 10:35:14 +02:00
Jon Eugster
49dcef91bc
add text suggestion leanprover-community/lean4game#222
2024-04-29 13:19:14 +02:00
Jon Eugster
7d02ff3b38
adding a hint
2024-04-18 12:04:45 +02:00
Jon Eugster
2dde9482d2
bump to v4.7.0
2024-04-10 17:07:22 +02:00
Jon Eugster
ad44c4fb21
add solutions to induction on other vars. #58
2024-03-24 12:36:58 +01:00
Jon Eugster
e462673c77
fix variable escaping
2024-03-24 12:25:59 +01:00
Jon Eugster
4a55822bbb
typo #57
2024-03-24 12:22:24 +01:00
Jon Eugster
18e0aec41d
use variable escaping in hints in LE-world
2024-03-18 16:40:56 +01:00
Jon Eugster
0353657b3e
improve hints in Implication lvl 2. #45
2024-03-18 16:33:57 +01:00
Jon Eugster
c35d29dcf4
make simp_add available in the entire game #54
2024-03-18 16:21:49 +01:00
Kevin Buzzard
61ce8321ef
fix typo in implication world
2024-03-17 22:15:35 +00:00
Jon Eugster
46dbb0e7f6
fix escaped backspaces
2024-03-11 19:10:20 +01:00
Jon Eugster
381a729f3e
bump to v4.6.0
2024-02-29 17:19:01 +01:00
Kevin Buzzard
26d8cf5395
typo
2024-02-27 10:14:09 +00:00
Kevin Buzzard
69cca24efd
fix accidentally commented-out NewTactic induction
2024-02-27 09:15:19 +00:00
Jon Eugster
6658392838
disable succ_inj. #50
2024-02-20 15:02:06 +01:00
Jon Eugster
d24f07df62
Merge pull request #47 from Not-Abram/ReturnToTypewriterModeSuggestion
...
Return to typewriter mode suggestion
2024-02-02 13:02:12 +01:00
Kevin Buzzard
923c4fb175
update docstrings in implication world
2024-01-24 17:50:18 +00:00
Kevin Buzzard
c5b9473978
algorithm world fix docstrings
2024-01-24 17:45:59 +00:00
Kevin Buzzard
e2ab764f90
missed one in power world
2024-01-24 17:45:50 +00:00
