Trigger CI for leanprover/lean4#6123

Batteries/Data/Array/Lemmas.lean

@@ -90,99 +90,141 @@ theorem map_empty (f : α → β) : map f #[] = #[] := mapM_empty f
 
 theorem mem_singleton : a ∈ #[b] ↔ a = b := 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
-
--- /-! ### 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
+/-! ### insertAt -/
+
+@[simp] private theorem size_insertIdx_loop (as : Array α) (i : Nat) (j : Fin as.size) :
+    (insertIdx.loop i as j).size = as.size := by
+  unfold insertIdx.loop
+  split
+  · rw [size_insertIdx_loop, size_swap]
+  · rfl
+
+@[simp] theorem size_insertIdx (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α) :
+    (as.insertIdx i v).size = as.size + 1 := by
+  rw [insertIdx, size_insertIdx_loop, size_push]
+
+@[deprecated size_insertIdx (since := "2024-11-20")] alias size_insertAt := size_insertIdx
+
+theorem getElem_insertIdx_loop_lt {as : Array α} {i : Nat} {j : Fin as.size} {k : Nat} {h}
+    (w : k < i) :
+    (insertIdx.loop i as j)[k] = as[k]'(by simpa using h) := by
+  unfold insertIdx.loop
+  split <;> rename_i h₁
+  · simp only
+    rw [getElem_insertIdx_loop_lt w]
+    rw [getElem_swap]
+    split <;> rename_i h₂
+    · simp_all
+      omega
+    · split <;> rename_i h₃
+      · omega
+      · simp_all
+  · rfl
+
+theorem getElem_insertIdx_loop_eq {as : Array α} {i : Nat} {j : Nat} {hj : j < as.size} {h} :
+    (insertIdx.loop i as ⟨j, hj⟩)[i] = if i ≤ j then as[j] else as[i]'(by simpa using h) := by
+  unfold insertIdx.loop
+  split <;> rename_i h₁
+  · simp at h₁
+    have : j - 1 < j := by omega
+    rw [getElem_insertIdx_loop_eq]
+    rw [getElem_swap]
+    simp
+    split <;> rename_i h₂
+    · rw [if_pos (by omega)]
+    · omega
+  · simp at h₁
+    by_cases h' : i = j
+    · simp [h']
+    · have t : ¬ i ≤ j := by omega
+      simp [t]
+
+theorem getElem_insertIdx_loop_gt {as : Array α} {i : Nat} {j : Nat} {hj : j < as.size}
+    {k : Nat} {h} (w : i < k) :
+    (insertIdx.loop i as ⟨j, hj⟩)[k] =
+      if k ≤ j then as[k-1]'(by simp at h; omega) else as[k]'(by simpa using h) := by
+  unfold insertIdx.loop
+  split <;> rename_i h₁
+  · simp only
+    simp only at h₁
+    have : j - 1 < j := by omega
+    rw [getElem_insertIdx_loop_gt w]
+    rw [getElem_swap]
+    simp only [Fin.getElem_fin]
+    split <;> rename_i h₂
+    · rw [if_neg (by omega), if_neg (by omega)]
+      have t : k ≤ j := by omega
+      simp [t]
+    · rw [getElem_swap]
+      simp only [Fin.getElem_fin]
+      rw [if_neg (by omega)]
+      split <;> rename_i h₃
+      · simp [h₃]
+      · have t : ¬ k ≤ j := by omega
+        simp [t]
+  · simp only at h₁
+    have t : ¬ k ≤ j := by omega
+    simp [t]
+
+theorem getElem_insertIdx_loop {as : Array α} {i : Nat} {j : Nat} {hj : j < as.size} {k : Nat} {h} :
+    (insertIdx.loop i as ⟨j, hj⟩)[k] =
+      if h₁ : k < i then
+        as[k]'(by simpa using h)
+      else
+        if h₂ : k = i then
+          if i ≤ j then as[j] else as[i]'(by simpa [h₂] using h)
+        else
+          if k ≤ j then as[k-1]'(by simp at h; omega) else as[k]'(by simpa using h) := by
+  split <;> rename_i h₁
+  · rw [getElem_insertIdx_loop_lt h₁]
+  · split <;> rename_i h₂
+    · subst h₂
+      rw [getElem_insertIdx_loop_eq]
+    · rw [getElem_insertIdx_loop_gt (by omega)]
+
+theorem getElem_insertIdx (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α)
+    (k) (h' : k < (as.insertIdx i v).size) :
+    (as.insertIdx i v)[k] =
+      if h₁ : k < i then
+        as[k]'(by omega)
+      else
+        if h₂ : k = i then
+          v
+        else
+          as[k - 1]'(by simp at h'; omega) := by
+  unfold insertIdx
+  rw [getElem_insertIdx_loop]
+  simp only [size_insertIdx] at h'
+  replace h' : k ≤ as.size := by omega
+  simp only [getElem_push, h, ↓reduceIte, Nat.lt_irrefl, ↓reduceDIte, h', dite_eq_ite]
+  split <;> rename_i h₁
+  · rw [dif_pos (by omega)]
+  · split <;> rename_i h₂
+    · simp [h₂]
+    · split <;> rename_i h₃
+      · rfl
+      · omega
+
+theorem getElem_insertIdx_lt (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α)
+    (k) (h' : k < (as.insertIdx i v).size) (h : k < i) :
+    (as.insertIdx i v)[k] = as[k] := by
+  simp [getElem_insertIdx, h]
+
+@[deprecated getElem_insertIdx_lt (since := "2024-11-20")] alias getElem_insertAt_lt :=
+getElem_insertIdx_lt
+
+theorem getElem_insertIdx_eq (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α) :
+    (as.insertIdx i v)[i]'(by simp; omega) = v := by
+  simp [getElem_insertIdx, h]
+
+@[deprecated getElem_insertIdx_eq (since := "2024-11-20")] alias getElem_insertAt_eq :=
+getElem_insertIdx_eq
+
+theorem getElem_insertIdx_gt (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α)
+    (k) (h' : k < (as.insertIdx i v).size) (h : i < k) :
+    (as.insertIdx i v)[k] = as[k-1]'(by simp at h'; omega) := by
+  rw [getElem_insertIdx]
+  rw [dif_neg (by omega), dif_neg (by omega)]
+
+@[deprecated getElem_insertIdx_gt (since := "2024-11-20")] alias getElem_insertAt_gt :=
+getElem_insertIdx_gt

Batteries/Data/Range/Lemmas.lean

@@ -45,11 +45,6 @@ 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
 
--- 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 =
@@ -62,12 +57,15 @@ theorem forIn'_eq_forIn_range' [Monad m] (r : Std.Range)
   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
+    simp only [numElems, Nat.not_le.2 h, ↓reduceIte, 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 [*])
+      intro n; induction n with
+        (intro H init
+         unfold forIn'.loop
+         simp only [↓reduceDIte, Nat.add_zero, List.pmap, List.forIn_cons, List.forIn_nil, h])
       | succ n ih => simp [ih (List.forall_mem_cons.1 H).2]; rfl
     · next step0 =>
       have hstep := Nat.pos_of_ne_zero step0
@@ -89,10 +87,15 @@ theorem forIn'_eq_forIn_range' [Monad m] (r : Std.Range)
           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
+          have := h2 0
+          simp only [Nat.mul_zero, Nat.add_zero, Nat.le_zero_eq, Nat.add_one_ne_zero, iff_false,
+            Nat.not_le] at this
+          rw [forIn'.loop]
+          simp only [this, ↓reduceDIte, ih, List.pmap, List.forIn_cons]
+          rfl
   else
-    simp [List.range', h, numElems_stop_le_start ⟨start, stop, step⟩ (Nat.not_lt.1 h), L]
+    simp only [numElems_stop_le_start ⟨start, stop, step⟩ (Nat.not_lt.1 h), List.range'_zero,
+      List.pmap, List.forIn_nil, L]
     cases stop <;> unfold forIn'.loop <;> simp [List.forIn', h]
 
 theorem forIn_eq_forIn_range' [Monad m] (r : Std.Range)
@@ -102,5 +105,3 @@ theorem forIn_eq_forIn_range' [Monad m] (r : Std.Range)
   · 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.getElem_mem h)
+  exact Nat.lt_succ.2 <| go (self.arr.toList.getElem_mem _)
 
 theorem rankD_lt_rankMax (self : UnionFind) (i : Nat) :
     rankD self.arr i < self.rankMax := by

Batteries/Data/Vector/Basic.lean

@@ -263,38 +263,27 @@ proof_wanted instLawfulBEq (α n) [BEq α] [LawfulBEq α] : LawfulBEq (Vector α
 @[inline] def reverse (v : Vector α n) : Vector α n :=
   ⟨v.toArray.reverse, 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 and a tactic provided proof. -/
+@[inline] def eraseIdx (v : Vector α n) (i : Nat) (h : i < n := by get_elem_tactic) :
+    Vector α (n-1) :=
+  ⟨v.toArray.eraseIdx i (v.size_toArray.symm ▸ h), by simp [Array.size_eraseIdx]⟩
 
 /-- 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 [*]⟩
+    v.eraseIdx i
   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 [*]⟩
+    v.eraseIdx 0
   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⟩
-
--/
+@[deprecated (since := "2024-11-20")] alias eraseIdxN := eraseIdx
 
 /--
 Finds the first index of a given value in a vector using `==` for comparison. Returns `none` if the