chore: update to mathlib 20/05/2024 (#311)

by running `lake -Kdoc=on update`

SSA/Projects/DCE/DCE.lean

@@ -15,8 +15,6 @@ def Deleted {α : Ty} (Γ: Ctxt Ty) (v : Γ.Var α) (Γ' : Ctxt Ty) : Prop :=
 /-- build a `Deleted` for a `(Γ.snoc α) → Γ`-/
 def Deleted.deleteSnoc (Γ : Ctxt Ty) (α : Ty) : Deleted (Γ.snoc α) (Ctxt.Var.last Γ α) Γ := rfl
 
-theorem List.eraseIdx_zero : List.eraseIdx (List.cons x xs) 0 = xs := rfl
-
 theorem List.eraseIdx_succ : List.eraseIdx (List.cons x xs) (.succ n) = x :: List.eraseIdx xs n := rfl
 
 /- removing from `xs ++ [x]` at index `(length xs)` equals `xs`. -/
@@ -27,22 +25,6 @@ theorem List.eraseIdx_eq_len_concat : List.eraseIdx (xs ++ [x]) xs.length = xs :
     simp[eraseIdx_succ]
     apply IH
 
-/-- removing at any index `≥ xs.length` does not change the list. -/
-theorem List.eraseIdx_of_length_le (hn : xs.length ≤ n) : List.eraseIdx xs n = xs := by
-  induction n generalizing xs
-  case zero =>
-    induction xs
-    case nil => simp [List.eraseIdx]
-    case cons x xs' IH => simp at hn
-  case succ n' IH' =>
-    induction xs
-    case nil => simp[eraseIdx]
-    case cons x xs' IH =>
-      simp[eraseIdx_succ]
-      apply IH'
-      simp at hn
-      linarith
-
 /- removing at index `n` does not change indices `k < n` -/
 theorem List.get?_eraseIdx_of_lt (hk: k < n) : List.get? (List.eraseIdx xs n) k = List.get? xs k := by
   by_cases N_LEN:(xs.length ≤ n)

SSA/Projects/FullyHomomorphicEncryption/Basic.lean

@@ -466,7 +466,7 @@ theorem R.fromTensor_eq_fromTensor'_fromPoly_aux (coeffs : List Int) (rp : R q n
 /-- fromTensor = R.fromPoly ∘ fromTensor'.
 This permits reasoning about fromTensor directly on the polynomial ring.
 -/
-theorem R.fromTensor_eq_fromTensor'_fromPoly {q n} : R.fromTensor (q := q) (n := n) coeffs =
+theorem R.fromTensor_eq_fromTensor'_fromPoly {q n} {coeffs : List Int} : R.fromTensor (q := q) (n := n) coeffs =
   R.fromPoly (q := q) (n := n) (R.fromTensor' q coeffs) := by
     simp[fromTensor, fromTensor']
     induction coeffs
@@ -545,7 +545,7 @@ theorem R.fromTensorFinsupp_concat_monomial {q : ℕ} (c : ℤ) (cs : List ℤ)
     rw[List.length_map]
 
 /-- show that `fromTensor` is the same as `fromPoly ∘ fromTensorFinsupp`. -/
-theorem R.fromTensor_eq_fromTensorFinsupp_fromPoly {q n} : R.fromTensor (q := q) (n := n) coeffs =
+theorem R.fromTensor_eq_fromTensorFinsupp_fromPoly {q n} {coeffs : List ℤ} : R.fromTensor (q := q) (n := n) coeffs =
   R.fromPoly (q := q) (n := n) (R.fromTensorFinsupp q coeffs) := by
     simp[fromTensor, fromTensor']
     induction coeffs  using List.reverseRecOn

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "56d2e4ee226603eb6b90b05f6b944bde42672cd5",
+   "rev": "914ad4f90518b7a2373ad6742a9518903f207927",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "2225b0e4a3528da20499e2304b521e0c4c2a4563",
+   "rev": "f617e0673845925e612b62141ff54c4b7980dc63",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -49,7 +49,7 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "c46d22bbe4f8363c0829ce0eb48a95012cdc0d79",
+   "rev": "35e38eb320982cfd2fcc864e0e0467ca223c8cdb",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,7 +58,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
-   "rev": "e6ea7987e2bef631d2be529252a5ff581e12362e",
+   "rev": "544c1c46397244b93b6cdb6db9eb456969062b15",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",