diff --git a/Mathlib/Algebra/Order/Archimedean/Basic.lean b/Mathlib/Algebra/Order/Archimedean/Basic.lean
index 612a79ebe8f136..f2ba71cf32dfa8 100644
--- a/Mathlib/Algebra/Order/Archimedean/Basic.lean
+++ b/Mathlib/Algebra/Order/Archimedean/Basic.lean
@@ -510,8 +510,8 @@ instance WithZero.instMulArchimedean (M) [CommMonoid M] [PartialOrder M] [MulArc
   constructor
   intro x y hxy
   cases y with
-  | zero => exact absurd hxy (zero_le _).not_gt
+  | zero => cases hxy.pos.false
   | coe y =>
     cases x with
-    | zero => refine ⟨0, zero_le _⟩
+    | zero => refine ⟨0, zero_le⟩
     | coe x => simpa [← WithZero.coe_pow] using (MulArchimedean.arch x (by simpa using hxy))
diff --git a/Mathlib/Algebra/Order/GroupWithZero/Canonical.lean b/Mathlib/Algebra/Order/GroupWithZero/Canonical.lean
index 06a11e634c2cae..c2945a3447455b 100644
--- a/Mathlib/Algebra/Order/GroupWithZero/Canonical.lean
+++ b/Mathlib/Algebra/Order/GroupWithZero/Canonical.lean
@@ -244,8 +244,8 @@ instance instBoundedOrder [OrderTop α] : BoundedOrder (WithZero α) :=
 instance : IsBotZeroClass (WithZero α) where
   isBot_zero _ := bot_le
 
--- TODO: deprecate
-lemma zero_le (a : WithZero α) : 0 ≤ a := by simp
+@[deprecated _root_.zero_le (since := "2026-05-06")]
+protected lemma zero_le (a : WithZero α) : 0 ≤ a := by simp
 
 /-- There is a general version `le_zero_iff`, but this lemma does not require a `PartialOrder`. -/
 @[simp]
@@ -308,8 +308,8 @@ instance instPreorder : Preorder (WithZero α) := inferInstanceAs <| Preorder (W
 instance instMulLeftMono [Mul α] [MulLeftMono α] :
     MulLeftMono (WithZero α) := by
   refine ⟨fun a b c hbc => ?_⟩
-  induction a; · exact zero_le _
-  induction b; · exact zero_le _
+  induction a; · exact zero_le
+  induction b; · exact zero_le
   rcases WithZero.coe_le_iff.1 hbc with ⟨c, rfl, hbc'⟩
   rw [← coe_mul _ c, ← coe_mul, coe_le_coe]
   exact mul_le_mul_right hbc' _
@@ -398,7 +398,7 @@ instance instPartialOrder : PartialOrder (WithZero α) :=
 instance instMulLeftReflectLT [Mul α] [MulLeftReflectLT α] :
     MulLeftReflectLT (WithZero α) := by
   refine ⟨fun a b c h => ?_⟩
-  have := ((zero_le _).trans_lt h).ne'
+  have := h.ne_zero
   induction a
   · simp at this
   induction c
@@ -511,7 +511,7 @@ instance instCanonicallyOrderedAdd [AddZeroClass α] [Preorder α] [CanonicallyO
 
 instance instLinearOrderedCommMonoidWithZero [CommMonoid α] [LinearOrder α]
     [IsOrderedCancelMonoid α] : LinearOrderedCommMonoidWithZero (WithZero α) where
-  isBot_zero := WithZero.zero_le
+  isBot_zero _ := zero_le
   mul_lt_mul_of_pos_left
   | (a : α), _, 0, (c : α), _ => by simp [← WithZero.coe_mul]
   | (a : α), _, (b : α), (c : α), hbc => by norm_cast at *; exact mul_lt_mul_right hbc _
diff --git a/Mathlib/FieldTheory/RatFunc/Valuation.lean b/Mathlib/FieldTheory/RatFunc/Valuation.lean
index a362a1be42c885..7f9ec8ae069657 100644
--- a/Mathlib/FieldTheory/RatFunc/Valuation.lean
+++ b/Mathlib/FieldTheory/RatFunc/Valuation.lean
@@ -68,19 +68,9 @@ theorem InftyValuation.map_mul' (x y : RatFunc F) :
 
 theorem InftyValuation.map_add_le_max' (x y : RatFunc F) :
     inftyValuationDef F (x + y) ≤ max (inftyValuationDef F x) (inftyValuationDef F y) := by
-  by_cases hx : x = 0
-  · rw [hx, zero_add]
-    conv_rhs => rw [inftyValuationDef, if_pos (Eq.refl _)]
-    rw [max_eq_right (WithZero.zero_le (inftyValuationDef F y))]
-  · by_cases hy : y = 0
-    · rw [hy, add_zero]
-      conv_rhs => rw [max_comm, inftyValuationDef, if_pos (Eq.refl _)]
-      rw [max_eq_right (WithZero.zero_le (inftyValuationDef F x))]
-    · by_cases hxy : x + y = 0
-      · rw [inftyValuationDef, if_pos hxy]; exact zero_le'
-      · rw [inftyValuationDef, inftyValuationDef, inftyValuationDef, if_neg hx, if_neg hy,
-          if_neg hxy]
-        simpa using RatFunc.intDegree_add_le hy hxy
+  unfold inftyValuationDef
+  have := @RatFunc.intDegree_add_le F
+  aesop
 
 @[simp]
 theorem inftyValuation_of_nonzero {x : RatFunc F} (hx : x ≠ 0) :
diff --git a/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean b/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
index db5aa5a3f73f06..acedc29b14dc74 100644
--- a/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
+++ b/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
@@ -204,8 +204,8 @@ theorem intValuation_zero_lt (x : nonZeroDivisors R) : 0 < v.intValuation x := b
 
 /-- The `v`-adic valuation on `R` is bounded above by 1. -/
 theorem intValuation_le_one (x : R) : v.intValuation x ≤ 1 := by
-  by_cases hx : x = 0
-  · rw [hx, Valuation.map_zero]; exact WithZero.zero_le 1
+  obtain rfl | hx := eq_or_ne x 0
+  · simp
   · rw [v.intValuation_if_neg hx, ← exp_zero, exp_le_exp, Right.neg_nonpos_iff]
     exact Int.natCast_nonneg _
 
@@ -711,7 +711,7 @@ lemma adicCompletion.mul_nonZeroDivisor_mem_adicCompletionIntegers (v : HeightOn
     -- now manually translate the goal (an inequality in ℤᵐ⁰) to an inequality of "log" of ℤ
     simp only [map_pow, mem_adicCompletionIntegers, map_mul, this, inv_pow, ← exp_nsmul, nsmul_one,
       Int.natCast_natAbs]
-    exact mul_inv_le_one_of_le₀ (le_exp_log.trans (by simp [le_abs_self])) (zero_le _)
+    exact mul_inv_le_one_of_le₀ (le_exp_log.trans (by simp [le_abs_self])) zero_le
 
 instance : FaithfulSMul (v.adicCompletionIntegers K) (v.adicCompletion K) :=
   Subsemiring.faithfulSMul _