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 37e16df commit baa988eCopy full SHA for baa988e
src/Init/Data/List/Nat/Range.lean
@@ -176,7 +176,7 @@ theorem pairwise_le_range (n : Nat) : Pairwise (· ≤ ·) (range n) :=
176
theorem take_range (m n : Nat) : take m (range n) = range (min m n) := by
177
apply List.ext_getElem
178
· simp
179
- · simp (config := { contextual := true }) [← getElem_take, Nat.lt_min]
+ · simp (config := { contextual := true }) [getElem_take, Nat.lt_min]
180
181
theorem nodup_range (n : Nat) : Nodup (range n) := by
182
simp (config := {decide := true}) only [range_eq_range', nodup_range']
0 commit comments