diff --git a/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean b/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean
index 87516d8c..2c257f1d 100644
--- a/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean
+++ b/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean
@@ -185,7 +185,7 @@ theorem roots_of_unity_in_cyclo_aux {x : K} {n l : ℕ} (hl : l ∈ n.divisors)
     by_contra h
     simp only [not_lt, le_zero_iff] at h
     rw [h] at pdivlcm_h
-    simp only [MulZeroClass.mul_zero, lcm_eq_zero_iff, PNat.ne_zero, or_false_iff] at pdivlcm_h
+    simp only [MulZeroClass.mul_zero, lcm_eq_zero_iff, PNat.ne_zero, or_false] at pdivlcm_h
     apply absurd pdivlcm_h (ne_of_gt (Nat.pos_of_mem_divisors hl))
   have K5 := (Nat.dvd_prime Nat.prime_two).1 (totient_le_one_dvd_two pdiv_ne_zero KEY3)
   cases' K5 with K5 K5
@@ -217,7 +217,7 @@ theorem roots_of_unity_in_cyclo (hpo : Odd (p : ℕ)) (x : K)
     have isPrimRoot : IsPrimitiveRoot (hζ.unit' : R) p := hζ.unit'_coe
     have hxl : (⟨x, hx⟩ : R) ^ l = 1 :=  by
       apply isRoot_of_unity_of_root_cyclotomic _ hhl
-      simp only [Nat.mem_divisors, dvd_refl, Ne, true_and_iff]
+      simp only [Nat.mem_divisors, dvd_refl, Ne, true_and]
       apply pos_iff_ne_zero.1 (Nat.pos_of_mem_divisors hl)
     have hxp' : (⟨x, hx⟩ : R) ^ (2 * p : ℕ) = 1 := by
       cases' hlp with hlp_w hlp_h
diff --git a/FltRegular/ReadyForMathlib/Homogenization.lean b/FltRegular/ReadyForMathlib/Homogenization.lean
index 590fbc68..ec499260 100644
--- a/FltRegular/ReadyForMathlib/Homogenization.lean
+++ b/FltRegular/ReadyForMathlib/Homogenization.lean
@@ -317,8 +317,8 @@ theorem leadingTerms_eq_self_iff_isHomogeneous (p : MvPolynomial ι R) :
     classical
     rw [← degree_eq_weight_one] at h_h₂
     change ¬(h_w.sum fun (_x : ι) (e : ℕ) => e) = p.totalDegree at h_h₂
-    simp only [h_h₁.symm, coeff_homogeneousComponent, exists_prop, and_true_iff, Ne,
-      not_false_iff, not_forall, ite_eq_left_iff]
+    simp only [h_h₁.symm, coeff_homogeneousComponent, exists_prop, and_true, Ne, not_false_iff,
+      not_forall, ite_eq_left_iff]
     convert h_h₂
   · rw [leadingTerms_apply]
     rw [(_ :
@@ -848,7 +848,7 @@ theorem prod_contains_no (i : ι) (P : Finset (MvPolynomial ι R))
       exact (degreeOf_eq_zero_iff _ _).2 (hp a (mem_cons_self _ _))
     · intro p hps m hmp
       apply hp p _ m hmp
-      simp only [hps, mem_cons, or_true_iff]
+      simp only [hps, mem_cons, or_true]
 
 open scoped BigOperators
 
diff --git a/lake-manifest.json b/lake-manifest.json
index 92b36357..f7cc6b93 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e5e4f1e9385f5a636cd95f7b5833d9ba7907115c",
+   "rev": "662f986ad3c5ad6ab1a1726b3c04f5ec425aa9f7",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -61,11 +61,21 @@
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
+  {"url": "https://github.com/siddhartha-gadgil/LeanSearchClient.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "c260ed920e2ebd23ef9fc8ca3fd24115e04c18b1",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "4b83244f3ea8cf1ebc70f68bc5b94691e826c827",
+   "rev": "8ce56442722e4c440569f5be581b07642dc4fbfe",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,