diff --git a/LeanPool/Redhill/Common/SubsumCondition.lean b/LeanPool/Redhill/Common/SubsumCondition.lean
index 6da68c7e67..d6366d5b5c 100644
--- a/LeanPool/Redhill/Common/SubsumCondition.lean
+++ b/LeanPool/Redhill/Common/SubsumCondition.lean
@@ -41,6 +41,13 @@ def StrongSSC : Prop :=
 
 variable {a}
 
+lemma SignType.natAbs_intCast_le_one (b : SignType) : (b : ℤ).natAbs ≤ 1 := by
+  cases b <;> decide
+
+lemma SignType.one_le_natAbs_intCast_sub {b₁ b₂ : SignType} (h : b₁ ≠ b₂) :
+    1 ≤ (b₁ - b₂ : ℤ).natAbs := by
+  cases b₁ <;> cases b₂ <;> simp_all
+
 lemma StrongSSC.SSC (h : StrongSSC a) : SSC a := by
   unfold _root_.SSC StrongSSC IsSubsumBlock at *
   contrapose! h
diff --git a/LeanPool/Redhill/General/Subsum.lean b/LeanPool/Redhill/General/Subsum.lean
index 6558b2ba4c..74aaa654a8 100644
--- a/LeanPool/Redhill/General/Subsum.lean
+++ b/LeanPool/Redhill/General/Subsum.lean
@@ -124,9 +124,10 @@ lemma X4_le_natAbs_b4 {b₁ b₂ b₃ b₄ : SignType} (hl : b₄ < b₃) :
       refine Nat.sub_le_sub_right ?_ _
       obtain rfl | rfl | rfl := b₃.trichotomy
       · simp at hl
-      · obtain rfl : b₄ = -1 := by decide +revert
+      · obtain rfl : b₄ = -1 := SignType.neg_iff.mp hl
         simpa using b₄_lower_bound hh
-      · obtain rfl | rfl : b₄ = 0 ∨ b₄ = -1 := by decide +revert
+      · obtain rfl | rfl : b₄ = 0 ∨ b₄ = -1 :=
+          (SignType.nonpos_iff.mp (SignType.lt_one_iff.mp hl)).symm
         · simpa using b₃_lower_bound hh
         · simp_rw [SignType.coe_neg, SignType.coe_one, neg_one_mul, neg_neg, one_mul]
           have n₁ : 0 ≤ (X F h - Y F : ℤ) ^ 5 := by
@@ -143,7 +144,7 @@ lemma X4_le_natAbs_b4 {b₁ b₂ b₃ b₄ : SignType} (hl : b₄ < b₃) :
       rw [add_mul]
       refine (Int.natAbs_add_le _ _).trans (Nat.add_le_add ?_ ?_)
       · rw [Int.natAbs_mul, ← one_mul (4 * _)]
-        exact mul_le_mul' (by decide +revert) (b₁_upper_bound hh)
+        exact mul_le_mul' (SignType.natAbs_intCast_le_one b₁) (b₁_upper_bound hh)
       · rw [show (10 * Y F - 1 : ℤ) = (10 * Y F - 1 : ℕ) by grind [Y_pos], ← mul_assoc]
         simp_rw [Int.natAbs_mul, Int.natAbs_pow, Int.natAbs_natCast]
         apply Nat.mul_le_mul_right
@@ -169,18 +170,19 @@ lemma X4_le_natAbs_b3 {b₁ b₂ b₃ : SignType} (hl : b₃ < b₂) :
     _ ≤ 5 * X F h ^ 4 - (b₁ * (X F h ^ 2 + 10 * Y F ^ 3 : ℤ) ^ 2).natAbs := by
       refine Nat.sub_le_sub_left ?_ _
       rw [Int.natAbs_mul, ← one_mul (4 * _)]
-      exact mul_le_mul' (by decide +revert) (b₁_upper_bound hh)
+      exact mul_le_mul' (SignType.natAbs_intCast_le_one b₁) (b₁_upper_bound hh)
     _ ≤ (b₂ * ((10 * Y F - 1 : ℤ) * X F h ^ 4) +
         b₃ * (-2 * Y F * (5 * X F h ^ 4 + 10 * X F h ^ 2 * Y F ^ 2 + Y F ^ 4))).natAbs -
         (b₁ * (X F h ^ 2 + 10 * Y F ^ 3 : ℤ) ^ 2).natAbs := by
       refine Nat.sub_le_sub_right ?_ _
       obtain rfl | rfl | rfl := b₂.trichotomy
       · simp at hl
-      · obtain rfl : b₃ = -1 := by decide +revert
+      · obtain rfl : b₃ = -1 := SignType.neg_iff.mp hl
         simpa using b₃_lower_bound_2
       · have cY : (10 * Y F - 1 : ℤ) = (10 * Y F - 1 : ℕ) := by grind [Y_pos]
         rw [SignType.coe_one, one_mul, cY]
-        obtain rfl | rfl : b₃ = 0 ∨ b₃ = -1 := by decide +revert
+        obtain rfl | rfl : b₃ = 0 ∨ b₃ = -1 :=
+          (SignType.nonpos_iff.mp (SignType.lt_one_iff.mp hl)).symm
         · rw [SignType.coe_zero, zero_mul, add_zero, Int.natAbs_mul]
           simp_rw [Int.natAbs_pow, Int.natAbs_natCast]
           exact Nat.mul_le_mul_right _ (by lia)
@@ -243,7 +245,7 @@ lemma X_le_natAbs_redEmb1 {b₁ b₂ b₃ b₄ : SignType} (hb : b₁ ≠ b₂ 
       rw [Int.natAbs_mul, ← one_mul (X F h ^ 4 + _)]
       norm_cast
       apply Nat.mul_le_mul_right
-      decide +revert
+      exact SignType.one_le_natAbs_intCast_sub hb
     _ ≤ ((b₁ - b₂ : ℤ) * (X F h ^ 4 + 20 * X F h ^ 2 * Y F ^ 3)).natAbs -
         (100 * Y F ^ 6 * b₁ - 2 * Y F ^ 5 * b₂ : ℤ).natAbs := by
       refine Nat.sub_le_sub_left ((Y6_le_X hh).trans' ?_) _
@@ -252,10 +254,10 @@ lemma X_le_natAbs_redEmb1 {b₁ b₂ b₃ b₄ : SignType} (hb : b₁ ≠ b₂ 
       calc
         _ ≤ 100 * Y F ^ 6 * 1 + 2 * Y F ^ 6 * 1 := by
           gcongr
-          · decide +revert
+          · exact SignType.natAbs_intCast_le_one b₁
           · exact Y_pos
           · decide
-          · decide +revert
+          · exact SignType.natAbs_intCast_le_one b₂
         _ ≤ _ := by lia
     _ ≤ _ := Int.sub_le_add_natAbs
 
diff --git a/LeanPool/Redhill/Odd/Subsum.lean b/LeanPool/Redhill/Odd/Subsum.lean
index 52cb6b899a..ef20d0b75a 100644
--- a/LeanPool/Redhill/Odd/Subsum.lean
+++ b/LeanPool/Redhill/Odd/Subsum.lean
@@ -152,7 +152,7 @@ lemma natAbs_le_redEmb1_reduced {b₁ b₂ : SignType} (h : b₁ ≠ b₂) (hx :
   refine (tsub_le_tsub ?_ ?_).trans Int.sub_le_add_natAbs
   · simp only [Int.natAbs_mul, Int.natAbs_pow, Int.reduceAbs,
       Int.natAbs_add_of_nonneg (sq_nonneg _) zero_le_one]
-    have : 1 ≤ (b₂ - b₁ : ℤ).natAbs := by cases b₁ <;> cases b₂ <;> simp_all
+    have : 1 ≤ (b₂ - b₁ : ℤ).natAbs := SignType.one_le_natAbs_intCast_sub h.symm
     rw [← mul_assoc]
     apply mul_le_mul' (by lia)
     calc
@@ -196,7 +196,11 @@ lemma isSubsumBlock_redEmb1 (hx : Y n F ≤ x.natAbs) :
       Y n F ≤ (b₁ * (x - 1) ^ 5 + b₂ * (10 * (x ^ 2 + 1) ^ 2) + b₃ * -(x + 1) ^ 5).natAbs by
     apply this
     contrapose! ncb
-    exact ⟨b 0, fun i ↦ by fin_cases i <;> tauto⟩
+    refine ⟨b 0, fun i ↦ ?_⟩
+    fin_cases i
+    · rfl
+    · exact ncb.1.symm
+    · exact ncb.2.symm
   exact fun h ↦ Y_le_natAbs_redEmb1 h hx
 
 lemma tupReduce_tup {c₁ : n + 2 = n + 5 - #(univ.map redEmb1)} :