deprecations

Author: kim-em

Mathlib/CategoryTheory/Shift/CommShiftTwo.lean

@@ -66,7 +66,7 @@ noncomputable def CommShift₂Setup.int [Preadditive D] [HasShift D ℤ]
   assoc _ _ _ := by
     dsimp
     rw [← zpow_add, ← zpow_add]
-    cutsat
+    lia
   commShift _ _ := ⟨by cat_disch⟩
   ε p q := (-1) ^ (p * q)
 

Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/FinTwo.lean

@@ -55,7 +55,7 @@ lemma isParabolic_iff_of_upperTriangular [IsReduced R] (hm : m 1 0 = 0) :
   have aux : m.discr = 0 ↔ m 0 0 = m 1 1 := by
     suffices m.discr = (m 0 0 - m 1 1) ^ 2 by
       rw [this, IsReduced.pow_eq_zero_iff two_ne_zero, sub_eq_zero]
-    grind [disc_fin_two, trace_fin_two, det_fin_two]
+    grind [discr_fin_two, trace_fin_two, det_fin_two]
   have (h : m 0 0 = m 1 1) : m ∈ Set.range (scalar _) ↔ m 0 1 = 0 := by
     constructor
     · rintro ⟨a, rfl⟩

Mathlib/RingTheory/IntegralClosure/Algebra/Ideal.lean

@@ -96,7 +96,7 @@ lemma exists_monic_aeval_eq_zero_forall_mem_of_mem_map [Algebra.IsIntegral R S]
   obtain ⟨p, hp, e, h⟩ := exists_monic_aeval_eq_zero_forall_mem_pow_of_mem_map hx
   refine ⟨p, hp, e, fun i hi ↦ ?_⟩
   obtain hi | hi := hi.lt_or_gt
-  · exact Ideal.pow_le_self (by cutsat) (h _)
+  · exact Ideal.pow_le_self (by lia) (h _)
   · simp [coeff_eq_zero_of_natDegree_lt hi]
 
 end Polynomial

Mathlib/RingTheory/Perfection.lean

@@ -194,14 +194,14 @@ theorem coeff_surjective (h : Function.Surjective (frobenius R p)) (n : ℕ) :
       choose x hx using h xk
       use x
   · intro m
-    obtain (h1 | h1 | h1) : n ≤ m ∨ n = m + 1 ∨ ¬ n ≤ m + 1 := by cutsat
-    · have h1' : n ≤ m + 1 := by cutsat
+    obtain (h1 | h1 | h1) : n ≤ m ∨ n = m + 1 ∨ ¬ n ≤ m + 1 := by lia
+    · have h1' : n ≤ m + 1 := by lia
       simp only [h1', ↓reduceDIte, h1, Nat.leRec_succ, ← frobenius_def]
       exact Classical.choose_spec (h _)
     · subst h1
       simp [← frobenius_def]
-    · have h1' : ¬ n ≤ m := by cutsat
-      have : n - m = (n - (m + 1)) + 1 := by cutsat
+    · have h1' : ¬ n ≤ m := by lia
+      have : n - m = (n - (m + 1)) + 1 := by lia
       simp [h1, h1', this, pow_succ, pow_mul]
   · simp