We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 9b18262 commit 87ade2dCopy full SHA for 87ade2d
src/Init/Data/List/Nat/Modify.lean
@@ -125,7 +125,7 @@ theorem modifyTailIdx_modifyTailIdx_le {f g : List α → List α} (m n : Nat) (
125
rcases Nat.exists_eq_add_of_le h with ⟨m, rfl⟩
126
rw [Nat.add_comm, modifyTailIdx_modifyTailIdx, Nat.add_sub_cancel]
127
128
-theorem modifyTailIdx_modifyTailIdx_eq {f g : List α → List α} (n : Nat) (l : List α) :
+theorem modifyTailIdx_modifyTailIdx_self {f g : List α → List α} (n : Nat) (l : List α) :
129
(l.modifyTailIdx f n).modifyTailIdx g n = l.modifyTailIdx (g ∘ f) n := by
130
rw [modifyTailIdx_modifyTailIdx_le n n l (Nat.le_refl n), Nat.sub_self]; rfl
131
0 commit comments