fix, mostly by commenting out

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
 

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

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 [*]

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