chore: rename valuation_posSubmonoid_ne_zero_of_compatible (#28040)

and sneak one more lemma in

Author: kckennylau

Mathlib/RingTheory/Valuation/ValuativeRel.lean

@@ -552,11 +552,20 @@ lemma isEquiv {Γ₁ Γ₂ : Type*}
   simp_rw [← Valuation.Compatible.rel_iff_le]
 
 @[simp]
-lemma valuation_posSubmonoid_ne_zero_of_compatible {Γ : Type*} [LinearOrderedCommMonoidWithZero Γ]
+lemma _root_.Valuation.apply_posSubmonoid_ne_zero {Γ : Type*} [LinearOrderedCommMonoidWithZero Γ]
     (v : Valuation R Γ) [v.Compatible] (x : posSubmonoid R) :
     v (x : R) ≠ 0 := by
   simp [(isEquiv v (valuation R)).ne_zero, valuation_posSubmonoid_ne_zero]
 
+@[deprecated (since := "2025-08-06")]
+alias valuation_posSubmonoid_ne_zero_of_compatible := _root_.Valuation.apply_posSubmonoid_ne_zero
+
+@[simp]
+lemma _root_.Valuation.apply_posSubmonoid_pos {Γ : Type*} [LinearOrderedCommMonoidWithZero Γ]
+    (v : Valuation R Γ) [v.Compatible] (x : posSubmonoid R) :
+    0 < v x :=
+  zero_lt_iff.mpr <| v.apply_posSubmonoid_ne_zero x
+
 variable (R) in
 /-- An alias for endowing a ring with a preorder defined as the valuative relation. -/
 def WithPreorder := R