sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 10:24:07 +00:00
Code Issues Packages Projects Releases Wiki Activity

fix: remove unused length simp argument in TakeDrop

Browse Source 
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
This commit is contained in:
Leonardo de Moura
2026-03-15 01:41:44 +00:00
parent 9661c3ab67
commit 8d13eabc30
1 changed files with 1 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
src/Init/Data/List/Nat/TakeDrop.lean
View File

@@ -311,7 +311,7 @@ theorem drop_length_cons {l : List α} (h : l ≠ []) (a : α) :
| nil =>
cases h rfl
| cons y l ih =>
simp only [drop, length]
simp only [drop]
by_cases h₁ : l = []
· simp [h₁]
rw [getLast_cons h₁]