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

Merge pull request #112 from leanprover-community/fix/adjust-hint

Browse Source 
fix: adjust hint text
This commit is contained in:
Jon Eugster
2025-09-23 22:57:12 +02:00
committed by GitHub
parent 1e99f52a29 65829e27da
commit 869e254313
2 changed files with 591 additions and 104 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
Game/Levels/Algorithm/L03add_algo2.lean
View File

@@ -33,7 +33,7 @@ Get the simplifier to solve it for you.
$(d + f) + (h + (a + c)) + (g + e + b) = a + b + c + d + e + f + g + h$. -/
Statement (a b c d e f g h : ℕ) :
(d + f) + (h + (a + c)) + (g + e + b) = a + b + c + d + e + f + g + h := by
Hint "Solve this level in one line with `simp only [add_assoc, add_left_comm, add_comm]`"
Hint "Solve this level in one line with `simp only [add_left_comm, add_comm]`"
simp only [add_left_comm, add_comm]
Conclusion