From 23b4216d1e3a2064058bb415c11e5f6df0417c99 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 19 Nov 2024 10:59:33 +1100
Subject: [PATCH 1/7] fixes to linter

---
 Batteries/Tactic/Lint/Frontend.lean |  4 ++--
 Batteries/Tactic/Lint/Simp.lean     |  2 +-
 BatteriesTest/lint_simpNF.lean      | 13 +++++++++++++
 3 files changed, 16 insertions(+), 3 deletions(-)

diff --git a/Batteries/Tactic/Lint/Frontend.lean b/Batteries/Tactic/Lint/Frontend.lean
index 3b6198f897..7f39e6759c 100644
--- a/Batteries/Tactic/Lint/Frontend.lean
+++ b/Batteries/Tactic/Lint/Frontend.lean
@@ -53,7 +53,7 @@ sanity check, lint, cleanup, command, tactic
 -/
 
 namespace Batteries.Tactic.Lint
-open Lean
+open Lean Elab Command
 
 /-- Verbosity for the linter output. -/
 inductive LintVerbosity
@@ -104,7 +104,7 @@ def lintCore (decls : Array Name) (linters : Array NamedLinter) :
       (linter, ·) <$> decls.mapM fun decl => (decl, ·) <$> do
         BaseIO.asTask do
           match ← withCurrHeartbeats (linter.test decl)
-              |>.run' {}
+              |>.run' mkMetaContext -- We use the context used by `Command.liftTermElabM`
               |>.run' {options, fileName := "", fileMap := default} {env}
               |>.toBaseIO with
           | Except.ok msg? => pure msg?
diff --git a/Batteries/Tactic/Lint/Simp.lean b/Batteries/Tactic/Lint/Simp.lean
index ba9eaf4405..3e83431dcc 100644
--- a/Batteries/Tactic/Lint/Simp.lean
+++ b/Batteries/Tactic/Lint/Simp.lean
@@ -108,7 +108,7 @@ see note [simp-normal form] for tips how to debug this.
 https://leanprover-community.github.io/mathlib_docs/notes.html#simp-normal%20form"
   test := fun declName => do
     unless ← isSimpTheorem declName do return none
-    let ctx := ← Simp.Context.mkDefault
+    let ctx ← Simp.Context.mkDefault
     checkAllSimpTheoremInfos (← getConstInfo declName).type fun {lhs, rhs, isConditional, ..} => do
       let isRfl ← isRflTheorem declName
       let ({ expr := lhs', proof? := prf1, .. }, prf1Stats) ←
diff --git a/BatteriesTest/lint_simpNF.lean b/BatteriesTest/lint_simpNF.lean
index c9c8f9d307..771e47c65a 100644
--- a/BatteriesTest/lint_simpNF.lean
+++ b/BatteriesTest/lint_simpNF.lean
@@ -38,4 +38,17 @@ theorem foo_eq_ite (n : Nat) : foo n = if n = n then n else 0 := by
 
 end Equiv
 
+namespace List
+
+private axiom test_sorry : ∀ {α}, α
+
+@[simp]
+theorem ofFn_getElem_eq_map {β : Type _} (l : List α) (f : α → β) :
+    ofFn (fun i : Fin l.length => f <| l[(i : Nat)]) = l.map f := test_sorry
+
+example {β : Type _} (l : List α) (f : α → β) :
+    ofFn (fun i : Fin l.length => f <| l[(i : Nat)]) = l.map f := by simp only [ofFn_getElem_eq_map]
+
+end List
+
 #lint- only simpNF

From 922825a3fa019deafbf4f61ed7c70fbdeebc9206 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 19 Nov 2024 15:29:38 +1100
Subject: [PATCH 2/7] remove redundant ext attributes

---
 Batteries/Classes/SatisfiesM.lean | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/Batteries/Classes/SatisfiesM.lean b/Batteries/Classes/SatisfiesM.lean
index 834cbbea68..9e4a7d0f09 100644
--- a/Batteries/Classes/SatisfiesM.lean
+++ b/Batteries/Classes/SatisfiesM.lean
@@ -247,9 +247,6 @@ instance : MonadSatisfying (Except ε) where
     | .error e => .error e
   val_eq {α p x?} h := by cases x? <;> simp
 
--- This will be redundant after nightly-2024-11-08.
-attribute [ext] ReaderT.ext
-
 instance [Monad m] [LawfulMonad m][MonadSatisfying m] : MonadSatisfying (ReaderT ρ m) where
   satisfying {α p x} h :=
     have h' := SatisfiesM_ReaderT_eq.mp h
@@ -263,9 +260,6 @@ instance [Monad m] [LawfulMonad m][MonadSatisfying m] : MonadSatisfying (ReaderT
 instance [Monad m] [LawfulMonad m] [MonadSatisfying m] : MonadSatisfying (StateRefT' ω σ m) :=
   inferInstanceAs <| MonadSatisfying (ReaderT _ _)
 
--- This will be redundant after nightly-2024-11-08.
-attribute [ext] StateT.ext
-
 instance [Monad m] [LawfulMonad m] [MonadSatisfying m] : MonadSatisfying (StateT ρ m) where
   satisfying {α p x} h :=
     have h' := SatisfiesM_StateT_eq.mp h

From d99ff6205f5d87394c824868fb493fcdcc4debb5 Mon Sep 17 00:00:00 2001
From: leanprover-community-mathlib4-bot
 <leanprover-community-mathlib4-bot@users.noreply.github.com>
Date: Tue, 19 Nov 2024 09:06:07 +0000
Subject: [PATCH 3/7] chore: bump to nightly-2024-11-19

---
 lean-toolchain | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lean-toolchain b/lean-toolchain
index 585547139e..80611d83b2 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-11-18
+leanprover/lean4:nightly-2024-11-19

From 485efbc439ee0ebdeae8afb0acd24a5e82e2f771 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 19 Nov 2024 20:53:19 +1100
Subject: [PATCH 4/7] chore: remove @[simp] attributes from monad-specific
 SatisfiesM lemmas (#1054)

---
 Batteries/Classes/SatisfiesM.lean | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/Batteries/Classes/SatisfiesM.lean b/Batteries/Classes/SatisfiesM.lean
index 834cbbea68..9b34cf475b 100644
--- a/Batteries/Classes/SatisfiesM.lean
+++ b/Batteries/Classes/SatisfiesM.lean
@@ -185,14 +185,15 @@ theorem SatisfiesM_EStateM_eq :
       rw [EStateM.run_map, EStateM.run]
       split <;> simp_all
 
-@[simp] theorem SatisfiesM_ReaderT_eq [Monad m] :
+theorem SatisfiesM_ReaderT_eq [Monad m] :
     SatisfiesM (m := ReaderT ρ m) p x ↔ ∀ s, SatisfiesM p (x.run s) :=
   (exists_congr fun a => by exact ⟨fun eq _ => eq ▸ rfl, funext⟩).trans Classical.skolem.symm
 
 theorem SatisfiesM_StateRefT_eq [Monad m] :
-    SatisfiesM (m := StateRefT' ω σ m) p x ↔ ∀ s, SatisfiesM p (x s) := by simp [ReaderT.run]
+    SatisfiesM (m := StateRefT' ω σ m) p x ↔ ∀ s, SatisfiesM p (x s) := by
+  simp [SatisfiesM_ReaderT_eq, ReaderT.run]
 
-@[simp] theorem SatisfiesM_StateT_eq [Monad m] [LawfulMonad m] :
+theorem SatisfiesM_StateT_eq [Monad m] [LawfulMonad m] :
     SatisfiesM (m := StateT ρ m) (α := α) p x ↔ ∀ s, SatisfiesM (m := m) (p ·.1) (x.run s) := by
   change SatisfiesM (m := StateT ρ m) (α := α) p x ↔ ∀ s, SatisfiesM (m := m) (p ·.1) (x s)
   refine .trans ⟨fun ⟨f, eq⟩ => eq ▸ ?_, fun ⟨f, h⟩ => ?_⟩ Classical.skolem.symm
@@ -201,7 +202,7 @@ theorem SatisfiesM_StateRefT_eq [Monad m] :
   · refine ⟨fun s => (fun ⟨⟨a, s'⟩, h⟩ => ⟨⟨a, h⟩, s'⟩) <$> f s, funext fun s => ?_⟩
     show _ >>= _ = _; simp [← h]
 
-@[simp] theorem SatisfiesM_ExceptT_eq [Monad m] [LawfulMonad m] :
+theorem SatisfiesM_ExceptT_eq [Monad m] [LawfulMonad m] :
     SatisfiesM (m := ExceptT ρ m) (α := α) p x ↔
       SatisfiesM (m := m) (∀ a, · = .ok a → p a) x.run := by
   change _ ↔ SatisfiesM (m := m) (∀ a, · = .ok a → p a) x

From 9762792852464bf9591f6cccfe44f14b3ef54b25 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 19 Nov 2024 21:26:26 +1100
Subject: [PATCH 5/7] fix test

---
 BatteriesTest/show_term.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/BatteriesTest/show_term.lean b/BatteriesTest/show_term.lean
index 7288c369e9..1986fc06ee 100644
--- a/BatteriesTest/show_term.lean
+++ b/BatteriesTest/show_term.lean
@@ -11,7 +11,7 @@ Authors: Kim Morrison
     exact n
     exact 37
 
-/-- info: Try this: refine (?fst, ?snd) -/
+/-- info: Try this: refine (?_, ?_) -/
 #guard_msgs in example : Nat × Nat := by
   show_term constructor
   repeat exact 42

From 58b15585c1480b5e9afcded83a36b8ea0a7d4a24 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Thu, 21 Nov 2024 08:31:05 +1100
Subject: [PATCH 6/7] fix, mostly by commenting out

---
 Batteries/Data/Array/Basic.lean     |  20 +--
 Batteries/Data/Array/Lemmas.lean    | 198 ++++++++++++++--------------
 Batteries/Data/Range/Lemmas.lean    | 105 ++++++++-------
 Batteries/Data/UnionFind/Basic.lean |   2 +-
 Batteries/Data/Vector/Basic.lean    |  53 ++++----
 lean-toolchain                      |   2 +-
 6 files changed, 184 insertions(+), 196 deletions(-)

diff --git a/Batteries/Data/Array/Basic.lean b/Batteries/Data/Array/Basic.lean
index 8be0bc967d..5631aa3628 100644
--- a/Batteries/Data/Array/Basic.lean
+++ b/Batteries/Data/Array/Basic.lean
@@ -155,25 +155,7 @@ Automatically generates proof of `i < a.size` with `get_elem_tactic` where feasi
 abbrev swapAtN (a : Array α) (i : Nat) (x : α) (h : i < a.size := by get_elem_tactic) :
     α × Array α := swapAt a ⟨i,h⟩ x
 
-/--
-`eraseIdxN a i h` Removes the element at position `i` from a vector of length `n`.
-`h : i < a.size` has a default argument `by get_elem_tactic` which tries to supply a proof
-that the index is valid.
-This function takes worst case O(n) time because it has to backshift all elements at positions
-greater than i.
--/
-abbrev eraseIdxN (a : Array α) (i : Nat) (h : i < a.size := by get_elem_tactic) : Array α :=
-  a.feraseIdx ⟨i, h⟩
-
-/--
-Remove the element at a given index from an array, panics if index is out of bounds.
--/
-def eraseIdx! (a : Array α) (i : Nat) : Array α :=
-  if h : i < a.size then
-    a.feraseIdx ⟨i, h⟩
-  else
-    have : Inhabited (Array α) := ⟨a⟩
-    panic! s!"index {i} out of bounds"
+@[deprecated (since := "2024-11-20")] alias eraseIdxN := eraseIdx
 
 end Array
 
diff --git a/Batteries/Data/Array/Lemmas.lean b/Batteries/Data/Array/Lemmas.lean
index 2613cbc4f3..7b17fc17fb 100644
--- a/Batteries/Data/Array/Lemmas.lean
+++ b/Batteries/Data/Array/Lemmas.lean
@@ -71,12 +71,9 @@ where
 @[simp] proof_wanted toList_erase [BEq α] {l : Array α} {a : α} :
     (l.erase a).toList = l.toList.erase a
 
-@[simp] theorem eraseIdx!_eq_eraseIdx (a : Array α) (i : Nat) :
-    a.eraseIdx! i = a.eraseIdx i := rfl
-
-@[simp] theorem size_eraseIdx (a : Array α) (i : Nat) :
-    (a.eraseIdx i).size = if i < a.size then a.size-1 else a.size := by
-  simp only [eraseIdx]; split; simp; rfl
+@[simp] theorem size_eraseIdxIfInBounds (a : Array α) (i : Nat) :
+    (a.eraseIdxIfInBounds i).size = if i < a.size then a.size-1 else a.size := by
+  simp only [eraseIdxIfInBounds]; split; simp; rfl
 
 /-! ### set -/
 
@@ -93,96 +90,99 @@ theorem map_empty (f : α → β) : map f #[] = #[] := mapM_empty f
 
 theorem mem_singleton : a ∈ #[b] ↔ a = b := by simp
 
-/-! ### insertAt -/
-
-private theorem size_insertAt_loop (as : Array α) (i : Fin (as.size+1)) (j : Fin bs.size) :
-    (insertAt.loop as i bs j).size = bs.size := by
-  unfold insertAt.loop
-  split
-  · rw [size_insertAt_loop, size_swap]
-  · rfl
-
-@[simp] theorem size_insertAt (as : Array α) (i : Fin (as.size+1)) (v : α) :
-    (as.insertAt i v).size = as.size + 1 := by
-  rw [insertAt, size_insertAt_loop, size_push]
-
-private theorem get_insertAt_loop_lt (as : Array α) (i : Fin (as.size+1)) (j : Fin bs.size)
-    (k) (hk : k < (insertAt.loop as i bs j).size) (h : k < i) :
-    (insertAt.loop as i bs j)[k] = bs[k]'(size_insertAt_loop .. ▸ hk) := by
-  unfold insertAt.loop
-  split
-  · have h1 : k ≠ j - 1 := by omega
-    have h2 : k ≠ j := by omega
-    rw [get_insertAt_loop_lt, getElem_swap, if_neg h1, if_neg h2]
-    exact h
-  · rfl
-
-private theorem get_insertAt_loop_gt (as : Array α) (i : Fin (as.size+1)) (j : Fin bs.size)
-    (k) (hk : k < (insertAt.loop as i bs j).size) (hgt : j < k) :
-    (insertAt.loop as i bs j)[k] = bs[k]'(size_insertAt_loop .. ▸ hk) := by
-  unfold insertAt.loop
-  split
-  · have h1 : k ≠ j - 1 := by omega
-    have h2 : k ≠ j := by omega
-    rw [get_insertAt_loop_gt, getElem_swap, if_neg h1, if_neg h2]
-    exact Nat.lt_of_le_of_lt (Nat.pred_le _) hgt
-  · rfl
-
-private theorem get_insertAt_loop_eq (as : Array α) (i : Fin (as.size+1)) (j : Fin bs.size)
-    (k) (hk : k < (insertAt.loop as i bs j).size) (heq : i = k) (h : i.val ≤ j.val) :
-    (insertAt.loop as i bs j)[k] = bs[j] := by
-  unfold insertAt.loop
-  split
-  · next h =>
-    rw [get_insertAt_loop_eq, Fin.getElem_fin, getElem_swap, if_pos rfl]
-    exact heq
-    exact Nat.le_pred_of_lt h
-  · congr; omega
-
-private theorem get_insertAt_loop_gt_le (as : Array α) (i : Fin (as.size+1)) (j : Fin bs.size)
-    (k) (hk : k < (insertAt.loop as i bs j).size) (hgt : i < k) (hle : k ≤ j) :
-    (insertAt.loop as i bs j)[k] = bs[k-1] := by
-  unfold insertAt.loop
-  split
-  · next h =>
-    if h0 : k = j then
-      cases h0
-      have h1 : j.val ≠ j - 1 := by omega
-      rw [get_insertAt_loop_gt, getElem_swap, if_neg h1, if_pos rfl]; rfl
-      exact Nat.pred_lt_of_lt hgt
-    else
-      have h1 : k - 1 ≠ j - 1 := by omega
-      have h2 : k - 1 ≠ j := by omega
-      rw [get_insertAt_loop_gt_le, getElem_swap, if_neg h1, if_neg h2]
-      apply Nat.le_of_lt_add_one
-      rw [Nat.sub_one_add_one]
-      exact Nat.lt_of_le_of_ne hle h0
-      exact Nat.not_eq_zero_of_lt h
-      exact hgt
-  · next h =>
-    absurd h
-    exact Nat.lt_of_lt_of_le hgt hle
-
-theorem getElem_insertAt_lt (as : Array α) (i : Fin (as.size+1)) (v : α)
-    (k) (hlt : k < i.val) {hk : k < (as.insertAt i v).size} {hk' : k < as.size} :
-    (as.insertAt i v)[k] = as[k] := by
-  simp only [insertAt]
-  rw [get_insertAt_loop_lt, getElem_push, dif_pos hk']
-  exact hlt
-
-theorem getElem_insertAt_gt (as : Array α) (i : Fin (as.size+1)) (v : α)
-    (k) (hgt : k > i.val) {hk : k < (as.insertAt i v).size} {hk' : k - 1 < as.size} :
-    (as.insertAt i v)[k] = as[k - 1] := by
-  simp only [insertAt]
-  rw [get_insertAt_loop_gt_le, getElem_push, dif_pos hk']
-  exact hgt
-  rw [size_insertAt] at hk
-  exact Nat.le_of_lt_succ hk
-
-theorem getElem_insertAt_eq (as : Array α) (i : Fin (as.size+1)) (v : α)
-    (k) (heq : i.val = k) {hk : k < (as.insertAt i v).size} :
-    (as.insertAt i v)[k] = v := by
-  simp only [insertAt]
-  rw [get_insertAt_loop_eq, Fin.getElem_fin, getElem_push_eq]
-  exact heq
-  exact Nat.le_of_lt_succ i.is_lt
+-- FIXME: temporarily commented out; I've broken this on nightly-2024-11-20,
+-- and am hoping it is not necessary to get Mathlib working again
+
+-- /-! ### insertAt -/
+
+-- private theorem size_insertAt_loop (as : Array α) (i : Fin (as.size+1)) (j : Fin bs.size) :
+--     (insertAt.loop as i bs j).size = bs.size := by
+--   unfold insertAt.loop
+--   split
+--   · rw [size_insertAt_loop, size_swap]
+--   · rfl
+
+-- @[simp] theorem size_insertAt (as : Array α) (i : Fin (as.size+1)) (v : α) :
+--     (as.insertAt i v).size = as.size + 1 := by
+--   rw [insertAt, size_insertAt_loop, size_push]
+
+-- private theorem get_insertAt_loop_lt (as : Array α) (i : Fin (as.size+1)) (j : Fin bs.size)
+--     (k) (hk : k < (insertAt.loop as i bs j).size) (h : k < i) :
+--     (insertAt.loop as i bs j)[k] = bs[k]'(size_insertAt_loop .. ▸ hk) := by
+--   unfold insertAt.loop
+--   split
+--   · have h1 : k ≠ j - 1 := by omega
+--     have h2 : k ≠ j := by omega
+--     rw [get_insertAt_loop_lt, getElem_swap, if_neg h1, if_neg h2]
+--     exact h
+--   · rfl
+
+-- private theorem get_insertAt_loop_gt (as : Array α) (i : Fin (as.size+1)) (j : Fin bs.size)
+--     (k) (hk : k < (insertAt.loop as i bs j).size) (hgt : j < k) :
+--     (insertAt.loop as i bs j)[k] = bs[k]'(size_insertAt_loop .. ▸ hk) := by
+--   unfold insertAt.loop
+--   split
+--   · have h1 : k ≠ j - 1 := by omega
+--     have h2 : k ≠ j := by omega
+--     rw [get_insertAt_loop_gt, getElem_swap, if_neg h1, if_neg h2]
+--     exact Nat.lt_of_le_of_lt (Nat.pred_le _) hgt
+--   · rfl
+
+-- private theorem get_insertAt_loop_eq (as : Array α) (i : Fin (as.size+1)) (j : Fin bs.size)
+--     (k) (hk : k < (insertAt.loop as i bs j).size) (heq : i = k) (h : i.val ≤ j.val) :
+--     (insertAt.loop as i bs j)[k] = bs[j] := by
+--   unfold insertAt.loop
+--   split
+--   · next h =>
+--     rw [get_insertAt_loop_eq, Fin.getElem_fin, getElem_swap, if_pos rfl]
+--     exact heq
+--     exact Nat.le_pred_of_lt h
+--   · congr; omega
+
+-- private theorem get_insertAt_loop_gt_le (as : Array α) (i : Fin (as.size+1)) (j : Fin bs.size)
+--     (k) (hk : k < (insertAt.loop as i bs j).size) (hgt : i < k) (hle : k ≤ j) :
+--     (insertAt.loop as i bs j)[k] = bs[k-1] := by
+--   unfold insertAt.loop
+--   split
+--   · next h =>
+--     if h0 : k = j then
+--       cases h0
+--       have h1 : j.val ≠ j - 1 := by omega
+--       rw [get_insertAt_loop_gt, getElem_swap, if_neg h1, if_pos rfl]; rfl
+--       exact Nat.pred_lt_of_lt hgt
+--     else
+--       have h1 : k - 1 ≠ j - 1 := by omega
+--       have h2 : k - 1 ≠ j := by omega
+--       rw [get_insertAt_loop_gt_le, getElem_swap, if_neg h1, if_neg h2]
+--       apply Nat.le_of_lt_add_one
+--       rw [Nat.sub_one_add_one]
+--       exact Nat.lt_of_le_of_ne hle h0
+--       exact Nat.not_eq_zero_of_lt h
+--       exact hgt
+--   · next h =>
+--     absurd h
+--     exact Nat.lt_of_lt_of_le hgt hle
+
+-- theorem getElem_insertAt_lt (as : Array α) (i : Fin (as.size+1)) (v : α)
+--     (k) (hlt : k < i.val) {hk : k < (as.insertAt i v).size} {hk' : k < as.size} :
+--     (as.insertAt i v)[k] = as[k] := by
+--   simp only [insertAt]
+--   rw [get_insertAt_loop_lt, getElem_push, dif_pos hk']
+--   exact hlt
+
+-- theorem getElem_insertAt_gt (as : Array α) (i : Fin (as.size+1)) (v : α)
+--     (k) (hgt : k > i.val) {hk : k < (as.insertAt i v).size} {hk' : k - 1 < as.size} :
+--     (as.insertAt i v)[k] = as[k - 1] := by
+--   simp only [insertAt]
+--   rw [get_insertAt_loop_gt_le, getElem_push, dif_pos hk']
+--   exact hgt
+--   rw [size_insertAt] at hk
+--   exact Nat.le_of_lt_succ hk
+
+-- theorem getElem_insertAt_eq (as : Array α) (i : Fin (as.size+1)) (v : α)
+--     (k) (heq : i.val = k) {hk : k < (as.insertAt i v).size} :
+--     (as.insertAt i v)[k] = v := by
+--   simp only [insertAt]
+--   rw [get_insertAt_loop_eq, Fin.getElem_fin, getElem_push_eq]
+--   exact heq
+--   exact Nat.le_of_lt_succ i.is_lt
diff --git a/Batteries/Data/Range/Lemmas.lean b/Batteries/Data/Range/Lemmas.lean
index a075e0b6b4..c25ace6c31 100644
--- a/Batteries/Data/Range/Lemmas.lean
+++ b/Batteries/Data/Range/Lemmas.lean
@@ -45,55 +45,58 @@ theorem mem_range'_elems (r : Range) (h : x ∈ List.range' r.start r.numElems r
     refine Nat.not_le.1 fun h =>
       Nat.not_le.2 h' <| (numElems_le_iff (Nat.pos_of_ne_zero step0)).2 h
 
-theorem forIn'_eq_forIn_range' [Monad m] (r : Std.Range)
-    (init : β) (f : (a : Nat) → a ∈ r → β → m (ForInStep β)) :
-    forIn' r init f =
-    forIn
-      ((List.range' r.start r.numElems r.step).pmap Subtype.mk fun _ => mem_range'_elems r)
-      init (fun ⟨a, h⟩ => f a h) := by
-  let ⟨start, stop, step⟩ := r
-  let L := List.range' start (numElems ⟨start, stop, step⟩) step
-  let f' : { a // start ≤ a ∧ a < stop } → _ := fun ⟨a, h⟩ => f a h
-  suffices ∀ H, forIn' [start:stop:step] init f = forIn (L.pmap Subtype.mk H) init f' from this _
-  intro H; dsimp only [forIn', Range.forIn']
-  if h : start < stop then
-    simp [numElems, Nat.not_le.2 h, L]; split
-    · subst step
-      suffices ∀ n H init,
-          forIn'.loop start stop 0 f n start (Nat.le_refl _) init =
-          forIn ((List.range' start n 0).pmap Subtype.mk H) init f' from this _ ..
-      intro n; induction n with (intro H init; unfold forIn'.loop; simp [*])
-      | succ n ih => simp [ih (List.forall_mem_cons.1 H).2]; rfl
-    · next step0 =>
-      have hstep := Nat.pos_of_ne_zero step0
-      suffices ∀ fuel l i hle H, l ≤ fuel →
-          (∀ j, stop ≤ i + step * j ↔ l ≤ j) → ∀ init,
-          forIn'.loop start stop step f fuel i hle init =
-          forIn ((List.range' i l step).pmap Subtype.mk H) init f' by
-        refine this _ _ _ _ _
-          ((numElems_le_iff hstep).2 (Nat.le_trans ?_ (Nat.le_add_left ..)))
-          (fun _ => (numElems_le_iff hstep).symm) _
-        conv => lhs; rw [← Nat.one_mul stop]
-        exact Nat.mul_le_mul_right stop hstep
-      intro fuel; induction fuel with intro l i hle H h1 h2 init
-      | zero => simp [forIn'.loop, Nat.le_zero.1 h1]
-      | succ fuel ih =>
-        cases l with
-        | zero => rw [forIn'.loop]; simp [Nat.not_lt.2 <| by simpa using (h2 0).2 (Nat.le_refl _)]
-        | succ l =>
-          have ih := ih _ _ (Nat.le_trans hle (Nat.le_add_right ..))
-            (List.forall_mem_cons.1 H).2 (Nat.le_of_succ_le_succ h1) fun i => by
-              rw [Nat.add_right_comm, Nat.add_assoc, ← Nat.mul_succ, h2, Nat.succ_le_succ_iff]
-          have := h2 0; simp at this
-          rw [forIn'.loop]; simp [this, ih]; rfl
-  else
-    simp [List.range', h, numElems_stop_le_start ⟨start, stop, step⟩ (Nat.not_lt.1 h), L]
-    cases stop <;> unfold forIn'.loop <;> simp [List.forIn', h]
+-- FIXME: temporarily commented out; I've broken this on nightly-2024-11-20,
+-- and am hoping it is not necessary to get Mathlib working again
+
+-- theorem forIn'_eq_forIn_range' [Monad m] (r : Std.Range)
+--     (init : β) (f : (a : Nat) → a ∈ r → β → m (ForInStep β)) :
+--     forIn' r init f =
+--     forIn
+--       ((List.range' r.start r.numElems r.step).pmap Subtype.mk fun _ => mem_range'_elems r)
+--       init (fun ⟨a, h⟩ => f a h) := by
+--   let ⟨start, stop, step⟩ := r
+--   let L := List.range' start (numElems ⟨start, stop, step⟩) step
+--   let f' : { a // start ≤ a ∧ a < stop } → _ := fun ⟨a, h⟩ => f a h
+--   suffices ∀ H, forIn' [start:stop:step] init f = forIn (L.pmap Subtype.mk H) init f' from this _
+--   intro H; dsimp only [forIn', Range.forIn']
+--   if h : start < stop then
+--     simp [numElems, Nat.not_le.2 h, L]; split
+--     · subst step
+--       suffices ∀ n H init,
+--           forIn'.loop start stop 0 f n start (Nat.le_refl _) init =
+--           forIn ((List.range' start n 0).pmap Subtype.mk H) init f' from this _ ..
+--       intro n; induction n with (intro H init; unfold forIn'.loop; simp [*])
+--       | succ n ih => simp [ih (List.forall_mem_cons.1 H).2]; rfl
+--     · next step0 =>
+--       have hstep := Nat.pos_of_ne_zero step0
+--       suffices ∀ fuel l i hle H, l ≤ fuel →
+--           (∀ j, stop ≤ i + step * j ↔ l ≤ j) → ∀ init,
+--           forIn'.loop start stop step f fuel i hle init =
+--           forIn ((List.range' i l step).pmap Subtype.mk H) init f' by
+--         refine this _ _ _ _ _
+--           ((numElems_le_iff hstep).2 (Nat.le_trans ?_ (Nat.le_add_left ..)))
+--           (fun _ => (numElems_le_iff hstep).symm) _
+--         conv => lhs; rw [← Nat.one_mul stop]
+--         exact Nat.mul_le_mul_right stop hstep
+--       intro fuel; induction fuel with intro l i hle H h1 h2 init
+--       | zero => simp [forIn'.loop, Nat.le_zero.1 h1]
+--       | succ fuel ih =>
+--         cases l with
+--         | zero => rw [forIn'.loop]; simp [Nat.not_lt.2 <| by simpa using (h2 0).2 (Nat.le_refl _)]
+--         | succ l =>
+--           have ih := ih _ _ (Nat.le_trans hle (Nat.le_add_right ..))
+--             (List.forall_mem_cons.1 H).2 (Nat.le_of_succ_le_succ h1) fun i => by
+--               rw [Nat.add_right_comm, Nat.add_assoc, ← Nat.mul_succ, h2, Nat.succ_le_succ_iff]
+--           have := h2 0; simp at this
+--           rw [forIn'.loop]; simp [this, ih]; rfl
+--   else
+--     simp [List.range', h, numElems_stop_le_start ⟨start, stop, step⟩ (Nat.not_lt.1 h), L]
+--     cases stop <;> unfold forIn'.loop <;> simp [List.forIn', h]
 
-theorem forIn_eq_forIn_range' [Monad m] (r : Std.Range)
-    (init : β) (f : Nat → β → m (ForInStep β)) :
-    forIn r init f = forIn (List.range' r.start r.numElems r.step) init f := by
-  refine Eq.trans ?_ <| (forIn'_eq_forIn_range' r init (fun x _ => f x)).trans ?_
-  · simp [forIn, forIn']
-  · suffices ∀ L H, forIn (List.pmap Subtype.mk L H) init (f ·.1) = forIn L init f from this _ ..
-    intro L; induction L generalizing init <;> intro H <;> simp [*]
+-- theorem forIn_eq_forIn_range' [Monad m] (r : Std.Range)
+--     (init : β) (f : Nat → β → m (ForInStep β)) :
+--     forIn r init f = forIn (List.range' r.start r.numElems r.step) init f := by
+--   refine Eq.trans ?_ <| (forIn'_eq_forIn_range' r init (fun x _ => f x)).trans ?_
+--   · simp [forIn, forIn']
+--   · suffices ∀ L H, forIn (List.pmap Subtype.mk L H) init (f ·.1) = forIn L init f from this _ ..
+--     intro L; induction L generalizing init <;> intro H <;> simp [*]
diff --git a/Batteries/Data/UnionFind/Basic.lean b/Batteries/Data/UnionFind/Basic.lean
index cefa85bf3c..3a523e4f9d 100644
--- a/Batteries/Data/UnionFind/Basic.lean
+++ b/Batteries/Data/UnionFind/Basic.lean
@@ -146,7 +146,7 @@ theorem rank'_lt_rankMax (self : UnionFind) (i : Nat) (h) : (self.arr[i]).rank <
     | a::l, _, List.Mem.head _ => by dsimp; apply Nat.le_max_left
     | a::l, _, .tail _ h => by dsimp; exact Nat.le_trans (go h) (Nat.le_max_right ..)
   simp only [Array.get_eq_getElem, rankMax, ← Array.foldr_toList]
-  exact Nat.lt_succ.2 <| go (self.arr.toList.get_mem i h)
+  exact Nat.lt_succ.2 <| go (self.arr.toList.getElem_mem h)
 
 theorem rankD_lt_rankMax (self : UnionFind) (i : Nat) :
     rankD self.arr i < self.rankMax := by
diff --git a/Batteries/Data/Vector/Basic.lean b/Batteries/Data/Vector/Basic.lean
index 73a4a41aee..7dd2abc78c 100644
--- a/Batteries/Data/Vector/Basic.lean
+++ b/Batteries/Data/Vector/Basic.lean
@@ -263,31 +263,34 @@ proof_wanted instLawfulBEq (α n) [BEq α] [LawfulBEq α] : LawfulBEq (Vector α
 @[inline] def reverse (v : Vector α n) : Vector α n :=
   ⟨v.toArray.reverse, by simp⟩
 
-/-- Delete an element of a vector using a `Fin` index. -/
-@[inline] def feraseIdx (v : Vector α n) (i : Fin n) : Vector α (n-1) :=
-  ⟨v.toArray.feraseIdx (Fin.cast v.size_toArray.symm i), by simp [Array.size_feraseIdx]⟩
-
-/-- Delete an element of a vector using a `Nat` index. Panics if the index is out of bounds. -/
-@[inline] def eraseIdx! (v : Vector α n) (i : Nat) : Vector α (n-1) :=
-  if _ : i < n then
-    ⟨v.toArray.eraseIdx i, by simp [*]⟩
-  else
-    have : Inhabited (Vector α (n-1)) := ⟨v.pop⟩
-    panic! "index out of bounds"
-
-/-- Delete the first element of a vector. Returns the empty vector if the input vector is empty. -/
-@[inline] def tail (v : Vector α n) : Vector α (n-1) :=
-  if _ : 0 < n then
-    ⟨v.toArray.eraseIdx 0, by simp [*]⟩
-  else
-    v.cast (by omega)
-
-/--
-Delete an element of a vector using a `Nat` index. By default, the `get_elem_tactic` is used to
-synthesise a proof that the index is within bounds.
--/
-@[inline] def eraseIdxN (v : Vector α n) (i : Nat) (h : i < n := by get_elem_tactic) :
-  Vector α (n - 1) := ⟨v.toArray.eraseIdxN i (by simp [*]), by simp⟩
+-- FIXME: temporarily commented out; I've broken this on nightly-2024-11-20,
+-- and am hoping it is not necessary to get Mathlib working again
+
+-- /-- Delete an element of a vector using a `Fin` index. -/
+-- @[inline] def feraseIdx (v : Vector α n) (i : Fin n) : Vector α (n-1) :=
+--   ⟨v.toArray.feraseIdx (Fin.cast v.size_toArray.symm i), by simp [Array.size_feraseIdx]⟩
+
+-- /-- Delete an element of a vector using a `Nat` index. Panics if the index is out of bounds. -/
+-- @[inline] def eraseIdx! (v : Vector α n) (i : Nat) : Vector α (n-1) :=
+--   if _ : i < n then
+--     ⟨v.toArray.eraseIdx i, by simp [*]⟩
+--   else
+--     have : Inhabited (Vector α (n-1)) := ⟨v.pop⟩
+--     panic! "index out of bounds"
+
+-- /-- Delete the first element of a vector. Returns the empty vector if the input vector is empty. -/
+-- @[inline] def tail (v : Vector α n) : Vector α (n-1) :=
+--   if _ : 0 < n then
+--     ⟨v.toArray.eraseIdx 0, by simp [*]⟩
+--   else
+--     v.cast (by omega)
+
+-- /--
+-- Delete an element of a vector using a `Nat` index. By default, the `get_elem_tactic` is used to
+-- synthesise a proof that the index is within bounds.
+-- -/
+-- @[inline] def eraseIdxN (v : Vector α n) (i : Nat) (h : i < n := by get_elem_tactic) :
+--   Vector α (n - 1) := ⟨v.toArray.eraseIdxN i (by simp [*]), by simp⟩
 
 /--
 Finds the first index of a given value in a vector using `==` for comparison. Returns `none` if the
diff --git a/lean-toolchain b/lean-toolchain
index 80611d83b2..118d9e578a 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-11-19
+leanprover/lean4:nightly-2024-11-20

From 9b9f4d0406d00baaae62d1a717b5aa854a2ae51d Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Thu, 21 Nov 2024 08:36:48 +1100
Subject: [PATCH 7/7] long lines

---
 Batteries/Data/Range/Lemmas.lean | 106 ++++++++++++++++---------------
 Batteries/Data/Vector/Basic.lean |  54 ++++++++--------
 2 files changed, 84 insertions(+), 76 deletions(-)

diff --git a/Batteries/Data/Range/Lemmas.lean b/Batteries/Data/Range/Lemmas.lean
index c25ace6c31..cba6bae84c 100644
--- a/Batteries/Data/Range/Lemmas.lean
+++ b/Batteries/Data/Range/Lemmas.lean
@@ -48,55 +48,59 @@ theorem mem_range'_elems (r : Range) (h : x ∈ List.range' r.start r.numElems r
 -- FIXME: temporarily commented out; I've broken this on nightly-2024-11-20,
 -- and am hoping it is not necessary to get Mathlib working again
 
--- theorem forIn'_eq_forIn_range' [Monad m] (r : Std.Range)
---     (init : β) (f : (a : Nat) → a ∈ r → β → m (ForInStep β)) :
---     forIn' r init f =
---     forIn
---       ((List.range' r.start r.numElems r.step).pmap Subtype.mk fun _ => mem_range'_elems r)
---       init (fun ⟨a, h⟩ => f a h) := by
---   let ⟨start, stop, step⟩ := r
---   let L := List.range' start (numElems ⟨start, stop, step⟩) step
---   let f' : { a // start ≤ a ∧ a < stop } → _ := fun ⟨a, h⟩ => f a h
---   suffices ∀ H, forIn' [start:stop:step] init f = forIn (L.pmap Subtype.mk H) init f' from this _
---   intro H; dsimp only [forIn', Range.forIn']
---   if h : start < stop then
---     simp [numElems, Nat.not_le.2 h, L]; split
---     · subst step
---       suffices ∀ n H init,
---           forIn'.loop start stop 0 f n start (Nat.le_refl _) init =
---           forIn ((List.range' start n 0).pmap Subtype.mk H) init f' from this _ ..
---       intro n; induction n with (intro H init; unfold forIn'.loop; simp [*])
---       | succ n ih => simp [ih (List.forall_mem_cons.1 H).2]; rfl
---     · next step0 =>
---       have hstep := Nat.pos_of_ne_zero step0
---       suffices ∀ fuel l i hle H, l ≤ fuel →
---           (∀ j, stop ≤ i + step * j ↔ l ≤ j) → ∀ init,
---           forIn'.loop start stop step f fuel i hle init =
---           forIn ((List.range' i l step).pmap Subtype.mk H) init f' by
---         refine this _ _ _ _ _
---           ((numElems_le_iff hstep).2 (Nat.le_trans ?_ (Nat.le_add_left ..)))
---           (fun _ => (numElems_le_iff hstep).symm) _
---         conv => lhs; rw [← Nat.one_mul stop]
---         exact Nat.mul_le_mul_right stop hstep
---       intro fuel; induction fuel with intro l i hle H h1 h2 init
---       | zero => simp [forIn'.loop, Nat.le_zero.1 h1]
---       | succ fuel ih =>
---         cases l with
---         | zero => rw [forIn'.loop]; simp [Nat.not_lt.2 <| by simpa using (h2 0).2 (Nat.le_refl _)]
---         | succ l =>
---           have ih := ih _ _ (Nat.le_trans hle (Nat.le_add_right ..))
---             (List.forall_mem_cons.1 H).2 (Nat.le_of_succ_le_succ h1) fun i => by
---               rw [Nat.add_right_comm, Nat.add_assoc, ← Nat.mul_succ, h2, Nat.succ_le_succ_iff]
---           have := h2 0; simp at this
---           rw [forIn'.loop]; simp [this, ih]; rfl
---   else
---     simp [List.range', h, numElems_stop_le_start ⟨start, stop, step⟩ (Nat.not_lt.1 h), L]
---     cases stop <;> unfold forIn'.loop <;> simp [List.forIn', h]
+/-
+
+theorem forIn'_eq_forIn_range' [Monad m] (r : Std.Range)
+    (init : β) (f : (a : Nat) → a ∈ r → β → m (ForInStep β)) :
+    forIn' r init f =
+    forIn
+      ((List.range' r.start r.numElems r.step).pmap Subtype.mk fun _ => mem_range'_elems r)
+      init (fun ⟨a, h⟩ => f a h) := by
+  let ⟨start, stop, step⟩ := r
+  let L := List.range' start (numElems ⟨start, stop, step⟩) step
+  let f' : { a // start ≤ a ∧ a < stop } → _ := fun ⟨a, h⟩ => f a h
+  suffices ∀ H, forIn' [start:stop:step] init f = forIn (L.pmap Subtype.mk H) init f' from this _
+  intro H; dsimp only [forIn', Range.forIn']
+  if h : start < stop then
+    simp [numElems, Nat.not_le.2 h, L]; split
+    · subst step
+      suffices ∀ n H init,
+          forIn'.loop start stop 0 f n start (Nat.le_refl _) init =
+          forIn ((List.range' start n 0).pmap Subtype.mk H) init f' from this _ ..
+      intro n; induction n with (intro H init; unfold forIn'.loop; simp [*])
+      | succ n ih => simp [ih (List.forall_mem_cons.1 H).2]; rfl
+    · next step0 =>
+      have hstep := Nat.pos_of_ne_zero step0
+      suffices ∀ fuel l i hle H, l ≤ fuel →
+          (∀ j, stop ≤ i + step * j ↔ l ≤ j) → ∀ init,
+          forIn'.loop start stop step f fuel i hle init =
+          forIn ((List.range' i l step).pmap Subtype.mk H) init f' by
+        refine this _ _ _ _ _
+          ((numElems_le_iff hstep).2 (Nat.le_trans ?_ (Nat.le_add_left ..)))
+          (fun _ => (numElems_le_iff hstep).symm) _
+        conv => lhs; rw [← Nat.one_mul stop]
+        exact Nat.mul_le_mul_right stop hstep
+      intro fuel; induction fuel with intro l i hle H h1 h2 init
+      | zero => simp [forIn'.loop, Nat.le_zero.1 h1]
+      | succ fuel ih =>
+        cases l with
+        | zero => rw [forIn'.loop]; simp [Nat.not_lt.2 <| by simpa using (h2 0).2 (Nat.le_refl _)]
+        | succ l =>
+          have ih := ih _ _ (Nat.le_trans hle (Nat.le_add_right ..))
+            (List.forall_mem_cons.1 H).2 (Nat.le_of_succ_le_succ h1) fun i => by
+              rw [Nat.add_right_comm, Nat.add_assoc, ← Nat.mul_succ, h2, Nat.succ_le_succ_iff]
+          have := h2 0; simp at this
+          rw [forIn'.loop]; simp [this, ih]; rfl
+  else
+    simp [List.range', h, numElems_stop_le_start ⟨start, stop, step⟩ (Nat.not_lt.1 h), L]
+    cases stop <;> unfold forIn'.loop <;> simp [List.forIn', h]
 
--- theorem forIn_eq_forIn_range' [Monad m] (r : Std.Range)
---     (init : β) (f : Nat → β → m (ForInStep β)) :
---     forIn r init f = forIn (List.range' r.start r.numElems r.step) init f := by
---   refine Eq.trans ?_ <| (forIn'_eq_forIn_range' r init (fun x _ => f x)).trans ?_
---   · simp [forIn, forIn']
---   · suffices ∀ L H, forIn (List.pmap Subtype.mk L H) init (f ·.1) = forIn L init f from this _ ..
---     intro L; induction L generalizing init <;> intro H <;> simp [*]
+theorem forIn_eq_forIn_range' [Monad m] (r : Std.Range)
+    (init : β) (f : Nat → β → m (ForInStep β)) :
+    forIn r init f = forIn (List.range' r.start r.numElems r.step) init f := by
+  refine Eq.trans ?_ <| (forIn'_eq_forIn_range' r init (fun x _ => f x)).trans ?_
+  · simp [forIn, forIn']
+  · suffices ∀ L H, forIn (List.pmap Subtype.mk L H) init (f ·.1) = forIn L init f from this _ ..
+    intro L; induction L generalizing init <;> intro H <;> simp [*]
+
+-/
diff --git a/Batteries/Data/Vector/Basic.lean b/Batteries/Data/Vector/Basic.lean
index 7dd2abc78c..f87dc73523 100644
--- a/Batteries/Data/Vector/Basic.lean
+++ b/Batteries/Data/Vector/Basic.lean
@@ -266,31 +266,35 @@ proof_wanted instLawfulBEq (α n) [BEq α] [LawfulBEq α] : LawfulBEq (Vector α
 -- FIXME: temporarily commented out; I've broken this on nightly-2024-11-20,
 -- and am hoping it is not necessary to get Mathlib working again
 
--- /-- Delete an element of a vector using a `Fin` index. -/
--- @[inline] def feraseIdx (v : Vector α n) (i : Fin n) : Vector α (n-1) :=
---   ⟨v.toArray.feraseIdx (Fin.cast v.size_toArray.symm i), by simp [Array.size_feraseIdx]⟩
-
--- /-- Delete an element of a vector using a `Nat` index. Panics if the index is out of bounds. -/
--- @[inline] def eraseIdx! (v : Vector α n) (i : Nat) : Vector α (n-1) :=
---   if _ : i < n then
---     ⟨v.toArray.eraseIdx i, by simp [*]⟩
---   else
---     have : Inhabited (Vector α (n-1)) := ⟨v.pop⟩
---     panic! "index out of bounds"
-
--- /-- Delete the first element of a vector. Returns the empty vector if the input vector is empty. -/
--- @[inline] def tail (v : Vector α n) : Vector α (n-1) :=
---   if _ : 0 < n then
---     ⟨v.toArray.eraseIdx 0, by simp [*]⟩
---   else
---     v.cast (by omega)
-
--- /--
--- Delete an element of a vector using a `Nat` index. By default, the `get_elem_tactic` is used to
--- synthesise a proof that the index is within bounds.
--- -/
--- @[inline] def eraseIdxN (v : Vector α n) (i : Nat) (h : i < n := by get_elem_tactic) :
---   Vector α (n - 1) := ⟨v.toArray.eraseIdxN i (by simp [*]), by simp⟩
+/-
+
+/-- Delete an element of a vector using a `Fin` index. -/
+@[inline] def feraseIdx (v : Vector α n) (i : Fin n) : Vector α (n-1) :=
+  ⟨v.toArray.feraseIdx (Fin.cast v.size_toArray.symm i), by simp [Array.size_feraseIdx]⟩
+
+/-- Delete an element of a vector using a `Nat` index. Panics if the index is out of bounds. -/
+@[inline] def eraseIdx! (v : Vector α n) (i : Nat) : Vector α (n-1) :=
+  if _ : i < n then
+    ⟨v.toArray.eraseIdx i, by simp [*]⟩
+  else
+    have : Inhabited (Vector α (n-1)) := ⟨v.pop⟩
+    panic! "index out of bounds"
+
+/-- Delete the first element of a vector. Returns the empty vector if the input vector is empty. -/
+@[inline] def tail (v : Vector α n) : Vector α (n-1) :=
+  if _ : 0 < n then
+    ⟨v.toArray.eraseIdx 0, by simp [*]⟩
+  else
+    v.cast (by omega)
+
+/--
+Delete an element of a vector using a `Nat` index. By default, the `get_elem_tactic` is used to
+synthesise a proof that the index is within bounds.
+-/
+@[inline] def eraseIdxN (v : Vector α n) (i : Nat) (h : i < n := by get_elem_tactic) :
+  Vector α (n - 1) := ⟨v.toArray.eraseIdxN i (by simp [*]), by simp⟩
+
+-/
 
 /--
 Finds the first index of a given value in a vector using `==` for comparison. Returns `none` if the