chore: bump to nightly-2022-11-19 (#658)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: kim-em

Mathlib/Data/List/Range.lean

@@ -34,14 +34,14 @@ theorem mem_range' {m : ℕ} : ∀ {s n : ℕ}, m ∈ range' s n ↔ s ≤ m ∧
     mem_cons.trans <| by
       simp only [mem_range', or_and_left, or_iff_right_of_imp this, l, Nat.add_right_comm]; rfl
 
-theorem rangeAux_range' : ∀ s n : ℕ, rangeAux s (range' s n) = range' 0 (n + s)
+theorem range_loop_range' : ∀ s n : ℕ, range.loop s (range' s n) = range' 0 (n + s)
   | 0, n => rfl
   | s + 1, n => by
     rw [show n + (s + 1) = n + 1 + s from Nat.add_right_comm n s 1]
-    exact rangeAux_range' s (n + 1)
+    exact range_loop_range' s (n + 1)
 
 theorem range_eq_range' (n : ℕ) : range n = range' 0 n :=
-  (rangeAux_range' n 0).trans <| by rw [Nat.zero_add]
+  (range_loop_range' n 0).trans <| by rw [Nat.zero_add]
 
 @[simp]
 theorem mem_range {m n : ℕ} : m ∈ range n ↔ m < n := by

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2022-11-17
+leanprover/lean4:nightly-2022-11-19

lean_packages/manifest.json

@@ -21,7 +21,7 @@
    "name": "Unicode",
    "inputRev": "main"},
   {"url": "https://github.com/leanprover/std4",
-   "rev": "006a0357c5d5bde9ee1898c1da1382e341d6c7f2",
+   "rev": "4261f9bcb56ada27ad9307beaf8c4dba5a0a6883",
    "name": "std",
    "inputRev": "main"},
   {"url": "https://github.com/leanprover/lake",