refactor(RingTheory/Valuation/ValuativeRel/Basic): fix theorem names for multiplication (leanprover-community#33658)

We rename `vle_mul_right` to `mul_vle_mul_left` and reorder its arguments to match `mul_le_mul_left`, and other analogous changes.

Author: vihdzp

Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean

@@ -76,16 +76,14 @@ class ValuativeRel (R : Type*) [CommRing R] where
   vle_total (x y) : vle x y ∨ vle y x
   vle_trans {z y x} : vle x y → vle y z → vle x z
   vle_add {x y z} : vle x z → vle y z → vle (x + y) z
-  vle_mul_right {x y} (z) : vle x y → vle (x * z) (y * z)
+  mul_vle_mul_left {x y} (h : vle x y) (z) : vle (x * z) (y * z)
   vle_mul_cancel {x y z} : ¬ vle z 0 → vle (x * z) (y * z) → vle x y
   not_vle_one_zero : ¬ vle 1 0
 
 @[inherit_doc] infix:50 " ≤ᵥ " => ValuativeRel.vle
 
 macro_rules | `($a ≤ᵥ $b) => `(binrel% ValuativeRel.vle $a $b)
 
-attribute [gcongr] ValuativeRel.vle_mul_right
-
 namespace Valuation
 
 variable {R Γ : Type*} [CommRing R] [LinearOrderedCommMonoidWithZero Γ]
@@ -109,7 +107,7 @@ namespace ValuativeRel
 @[deprecated (since := "2025-12-20")] alias rel_total := vle_total
 @[deprecated (since := "2025-12-20")] alias rel_trans := vle_trans
 @[deprecated (since := "2025-12-20")] alias rel_add := vle_add
-@[deprecated (since := "2025-12-20")] alias rel_mul_right := vle_mul_right
+@[deprecated (since := "2025-12-20")] alias rel_mul_right := mul_vle_mul_left
 @[deprecated (since := "2025-12-20")] alias rel_mul_cancel := vle_mul_cancel
 @[deprecated (since := "2025-12-20")] alias not_rel_one_zero := not_vle_one_zero
 
@@ -132,7 +130,7 @@ lemma srel_iff {x y : R} : x <ᵥ y ↔ ¬ y ≤ᵥ x := Iff.rfl
 
 @[deprecated (since := "2025-12-20")] alias not_srel_iff := not_vlt
 
-@[simp]
+@[simp, refl]
 lemma vle_refl (x : R) : x ≤ᵥ x := by
   cases vle_total x x <;> assumption
 
@@ -153,7 +151,7 @@ protected alias vle.rfl := vle_rfl
 
 @[simp]
 theorem zero_vle (x : R) : 0 ≤ᵥ x := by
-  simpa using vle_mul_right x ((vle_total 0 1).resolve_right not_vle_one_zero)
+  simpa using mul_vle_mul_left ((vle_total 0 1).resolve_right not_vle_one_zero) x
 
 @[deprecated (since := "2025-12-20")] alias zero_rel := zero_vle
 
@@ -163,12 +161,19 @@ lemma zero_vlt_one : (0 : R) <ᵥ 1 :=
 
 @[deprecated (since := "2025-12-20")] alias zero_srel_one := zero_vlt_one
 
-@[gcongr]
-lemma vle_mul_left {x y : R} (z) : x ≤ᵥ y → z * x ≤ᵥ z * y := by
+@[deprecated mul_vle_mul_left (since := "2026-01-06")]
+lemma vle_mul_right {x y : R} (z) (h : x ≤ᵥ y) : x * z ≤ᵥ y * z :=
+  mul_vle_mul_left h z
+
+lemma mul_vle_mul_right {x y : R} (h : x ≤ᵥ y) (z) : z * x ≤ᵥ z * y := by
   rw [mul_comm z x, mul_comm z y]
-  apply vle_mul_right
+  exact mul_vle_mul_left h z
+
+@[deprecated mul_vle_mul_right (since := "2025-01-06")]
+lemma vle_mul_left {x y : R} (z) (h : x ≤ᵥ y) : z * x ≤ᵥ z * y :=
+  mul_vle_mul_right h z
 
-@[deprecated (since := "2025-12-20")] alias rel_mul_left := vle_mul_left
+@[deprecated (since := "2025-12-20")] alias rel_mul_left := mul_vle_mul_right
 
 instance : Trans (vle (R := R)) (vle (R := R)) (vle (R := R)) where
   trans h1 h2 := vle_trans h1 h2
@@ -187,14 +192,13 @@ protected alias vle.trans' := vle_trans'
 @[deprecated (since := "2025-12-20")] protected alias Rel.trans' := vle.trans'
 
 @[gcongr]
-lemma mul_vle_mul {x x' y y' : R} (h1 : x ≤ᵥ y) (h2 : x' ≤ᵥ y') : x * x' ≤ᵥ y * y' := by
-  calc x * x' ≤ᵥ x * y' := vle_mul_left _ h2
-    _ ≤ᵥ y * y' := vle_mul_right _ h1
+lemma mul_vle_mul {x x' y y' : R} (h1 : x ≤ᵥ y) (h2 : x' ≤ᵥ y') : x * x' ≤ᵥ y * y' :=
+  (mul_vle_mul_left h1 _).trans (mul_vle_mul_right h2 _)
 
 @[deprecated (since := "2025-12-20")] alias mul_rel_mul := mul_vle_mul
 
 @[simp] lemma mul_vle_mul_iff_left (hz : 0 <ᵥ z) : x * z ≤ᵥ y * z ↔ x ≤ᵥ y :=
-  ⟨vle_mul_cancel hz, vle_mul_right _⟩
+  ⟨vle_mul_cancel hz, (mul_vle_mul_left · _)⟩
 
 @[deprecated (since := "2025-12-20")] alias mul_rel_mul_iff_left := mul_vle_mul_iff_left
 
@@ -206,11 +210,17 @@ lemma mul_vle_mul {x x' y y' : R} (h1 : x ≤ᵥ y) (h2 : x' ≤ᵥ y') : x * x'
 @[simp] lemma mul_vlt_mul_iff_left (hz : 0 <ᵥ z) : x * z <ᵥ y * z ↔ x <ᵥ y :=
   (mul_vle_mul_iff_left hz).not
 
+@[gcongr] alias ⟨_, mul_vlt_mul_left⟩ := mul_vlt_mul_iff_left
+@[deprecated (since := "2026-01-06")] alias vlt_mul_right := mul_vlt_mul_left
+
 @[deprecated (since := "2025-12-20")] alias mul_srel_mul_iff_left := mul_vlt_mul_iff_left
 
 @[simp] lemma mul_vlt_mul_iff_right (hx : 0 <ᵥ x) : x * y <ᵥ x * z ↔ y <ᵥ z :=
   (mul_vle_mul_iff_right hx).not
 
+@[gcongr] alias ⟨_, mul_vlt_mul_right⟩ := mul_vlt_mul_iff_right
+@[deprecated (since := "2026-01-06")] alias vlt_mul_left := mul_vlt_mul_right
+
 @[deprecated (since := "2025-12-20")] alias mul_srel_mul_iff_right := mul_vlt_mul_iff_right
 
 @[deprecated (since := "2025-11-04")] alias rel_mul := mul_vle_mul
@@ -441,24 +451,24 @@ instance : LE (ValueGroupWithZero R) where
     · refine propext ⟨fun h => vle_trans ?_ (zero_vle _), fun h => vle_trans ?_ (zero_vle _)⟩
       · apply vle_mul_cancel (s * v).prop
         rw [mul_right_comm, Submonoid.coe_mul, ← mul_assoc]
-        apply vle_trans (vle_mul_right (u : R) (vle_mul_right (v : R) h₂))
+        apply (mul_vle_mul_left (mul_vle_mul_left h₂ v) u).trans
         rw [mul_right_comm x]
-        apply vle_trans (vle_mul_right (u : R) (vle_mul_right (t : R) h))
-        apply vle_trans (vle_mul_right (u : R) (vle_mul_right (t : R) (vle_mul_right (s : R) hz)))
+        apply (mul_vle_mul_left (mul_vle_mul_left h t) u).trans
+        apply vle_trans (mul_vle_mul_left (mul_vle_mul_left (mul_vle_mul_left hz s) t) u)
         simp
       · apply vle_mul_cancel (t * u).prop
         rw [mul_right_comm, Submonoid.coe_mul, ← mul_assoc]
-        apply vle_trans (vle_mul_right (v : R) (vle_mul_right (u : R) h₁))
+        apply (mul_vle_mul_left (mul_vle_mul_left h₁ u) v).trans
         rw [mul_right_comm y]
-        apply vle_trans (vle_mul_right (v : R) (vle_mul_right (s : R) h))
-        apply vle_trans (vle_mul_right (v : R) (vle_mul_right (s : R) (vle_mul_right (t : R) hw)))
+        apply (mul_vle_mul_left (mul_vle_mul_left h s) v).trans
+        apply vle_trans (mul_vle_mul_left (mul_vle_mul_left (mul_vle_mul_left hw t) s) v)
         simp
     · absurd hz
       apply vle_mul_cancel u.prop
-      simpa using vle_trans h₃ (vle_mul_right (v : R) hw)
+      simpa using h₃.trans (mul_vle_mul_left hw v)
     · absurd hw
       apply vle_mul_cancel v.prop
-      simpa using vle_trans h₄ (vle_mul_right (u : R) hz)
+      simpa using h₄.trans (mul_vle_mul_left hz u)
     · refine propext ⟨fun h => ?_, fun h => ?_⟩
       · apply vle_mul_cancel s.prop
         apply vle_mul_cancel hz
@@ -491,9 +501,9 @@ instance : LinearOrder (ValueGroupWithZero R) where
     apply vle_mul_cancel b₂.prop
     calc a₁ * c₂ * b₂
       _ = a₁ * b₂ * c₂ := by rw [mul_right_comm]
-      _ ≤ᵥ b₁ * a₂ * c₂ := vle_mul_right (c₂ : R) hab
+      _ ≤ᵥ b₁ * a₂ * c₂ := mul_vle_mul_left hab _
       _ = b₁ * c₂ * a₂ := by rw [mul_right_comm]
-      _ ≤ᵥ c₁ * b₂ * a₂ := vle_mul_right (a₂ : R) hbc
+      _ ≤ᵥ c₁ * b₂ * a₂ := mul_vle_mul_left hbc _
       _ = c₁ * a₂ * b₂ := by rw [mul_right_comm]
   le_antisymm a b hab hba := by
     induction a using ValueGroupWithZero.ind
@@ -533,7 +543,7 @@ instance : IsOrderedMonoid (ValueGroupWithZero R) where
     simp only [ValueGroupWithZero.mk_mul_mk, ValueGroupWithZero.mk_le_mk, Submonoid.coe_mul]
     conv_lhs => apply mul_mul_mul_comm
     conv_rhs => apply mul_mul_mul_comm
-    exact vle_mul_right _ hab
+    exact mul_vle_mul_left hab _
 
 instance : Inv (ValueGroupWithZero R) where
   inv := ValueGroupWithZero.lift (fun x s => by
@@ -543,10 +553,10 @@ instance : Inv (ValueGroupWithZero R) where
     · simp [hx, hy]
     · absurd hy
       apply vle_mul_cancel s.prop
-      simpa using vle_trans h₂ (vle_mul_right (t : R) hx)
+      simpa using vle_trans h₂ (mul_vle_mul_left hx t)
     · absurd hx
       apply vle_mul_cancel t.prop
-      simpa using vle_trans h₁ (vle_mul_right (s : R) hy)
+      simpa using vle_trans h₁ (mul_vle_mul_left hy s)
     · simp only [dif_neg hx, dif_neg hy]
       apply ValueGroupWithZero.sound
       · simpa [mul_comm] using h₂
@@ -618,7 +628,7 @@ def ofValuation
   vle_total x y := le_total (v x) (v y)
   vle_trans := le_trans
   vle_add hab hbc := (map_add_le_max v _ _).trans (sup_le hab hbc)
-  vle_mul_right _ h := by simp [map_mul]; gcongr
+  mul_vle_mul_left _ h := by simp [map_mul]; gcongr
   vle_mul_cancel h0 h := by
     rw [map_zero, le_zero_iff] at h0
     simp only [map_mul] at h
@@ -716,7 +726,7 @@ instance : ValuativeRel (WithPreorder R) where
   vle_total := vle_total (R := R)
   vle_trans := vle_trans (R := R)
   vle_add := vle_add (R := R)
-  vle_mul_right := vle_mul_right (R := R)
+  mul_vle_mul_left := mul_vle_mul_left (R := R)
   vle_mul_cancel := vle_mul_cancel (R := R)
   not_vle_one_zero := not_vle_one_zero (R := R)
 
@@ -729,7 +739,7 @@ def supp : Ideal R where
   carrier := { x | x ≤ᵥ 0 }
   add_mem' ha hb := vle_add ha hb
   zero_mem' := vle_refl _
-  smul_mem' x _ h := by simpa using vle_mul_left _ h
+  smul_mem' x _ h := by simpa using mul_vle_mul_right h _
 
 @[simp]
 lemma supp_def (x : R) : x ∈ supp R ↔ x ≤ᵥ 0 := Iff.refl _
@@ -774,48 +784,40 @@ lemma vlt.trans (hab : a <ᵥ b) (hbc : b <ᵥ c) : a <ᵥ c :=
 
 @[deprecated (since := "2025-12-20")] alias SRel.trans := vlt.trans
 
-lemma vle_mul_right_iff (hc : 0 <ᵥ c) : a * c ≤ᵥ b * c ↔ a ≤ᵥ b :=
-  ⟨vle_mul_cancel hc, vle_mul_right _⟩
+@[deprecated (since := "2026-01-06")] alias vle_mul_right_iff := mul_vle_mul_iff_left
 
 @[deprecated (since := "2025-12-20")] alias rel_mul_right_iff := vle_mul_right_iff
 
-lemma vle_mul_left_iff (hc : 0 <ᵥ c) : c * a ≤ᵥ c * b ↔ a ≤ᵥ b := by
-  simp [mul_comm c, vle_mul_right_iff hc]
-
-@[deprecated (since := "2025-12-20")] alias rel_mul_left_iff := vle_mul_left_iff
-
-lemma vlt_mul_right_iff (hc : 0 <ᵥ c) : a * c <ᵥ b * c ↔ a <ᵥ b :=
-  (vle_mul_right_iff hc).not
+@[deprecated (since := "2026-01-06")] alias vle_mul_left_iff := mul_vle_mul_iff_right
 
-@[deprecated (since := "2025-12-20")] alias srel_mul_right_iff := vlt_mul_right_iff
+@[deprecated (since := "2025-12-20")] alias rel_mul_left_iff := mul_vle_mul_iff_right
 
-@[gcongr] alias ⟨_, vlt_mul_right⟩ := vlt_mul_right_iff
+@[deprecated (since := "2026-01-06")] alias vlt_mul_right_iff := mul_vlt_mul_iff_left
 
-@[deprecated (since := "2025-12-20")] alias srel_mul_right := vlt_mul_right
+@[deprecated (since := "2025-12-20")] alias srel_mul_right_iff := mul_vlt_mul_iff_left
 
-lemma vlt_mul_left_iff (hc : 0 <ᵥ c) : c * a <ᵥ c * b ↔ a <ᵥ b :=
-  (vle_mul_left_iff hc).not
+@[deprecated (since := "2025-12-20")] alias srel_mul_right := mul_vlt_mul_right
 
-@[deprecated (since := "2025-12-20")] alias srel_mul_left_iff := vlt_mul_left_iff
+@[deprecated (since := "2026-01-06")] alias vlt_mul_left_iff := mul_vlt_mul_iff_right
 
-@[gcongr] alias ⟨_, vlt_mul_left⟩ := vlt_mul_left_iff
+@[deprecated (since := "2025-12-20")] alias srel_mul_left_iff := mul_vlt_mul_iff_right
 
-@[deprecated (since := "2025-12-20")] alias srel_mul_left := vlt_mul_left
+@[deprecated (since := "2025-12-20")] alias srel_mul_left := mul_vlt_mul_right
 
 lemma mul_vlt_mul_of_vlt_of_vle (hab : a <ᵥ b) (hcd : c ≤ᵥ d) (hd : 0 <ᵥ d) :
     a * c <ᵥ b * d :=
-  (vle_mul_left _ hcd).trans_vlt (vlt_mul_right hd hab)
+  (mul_vle_mul_right hcd _).trans_vlt (mul_vlt_mul_left hd hab)
 
 @[deprecated (since := "2025-12-20")] alias mul_srel_mul_of_srel_of_rel := mul_vlt_mul_of_vlt_of_vle
 
 lemma mul_vlt_mul_of_vle_of_vlt (hab : a ≤ᵥ b) (hcd : c <ᵥ d) (ha : 0 <ᵥ a) :
     a * c <ᵥ b * d :=
-  (vlt_mul_left ha hcd).trans_vle (vle_mul_right _ hab)
+  (mul_vlt_mul_right ha hcd).trans_vle (mul_vle_mul_left hab _)
 
 @[deprecated (since := "2025-12-20")] alias mul_srel_mul_of_rel_of_srel := mul_vlt_mul_of_vle_of_vlt
 
 lemma mul_vlt_mul (hab : a <ᵥ b) (hcd : c <ᵥ d) : a * c <ᵥ b * d :=
-  (vle_mul_left _ hcd.vle).trans_vlt (vlt_mul_right ((zero_vle c).trans_vlt hcd) hab)
+  (mul_vle_mul_right hcd.vle _).trans_vlt (mul_vlt_mul_left ((zero_vle c).trans_vlt hcd) hab)
 
 @[deprecated (since := "2025-12-20")] alias mul_srel_mul := mul_vlt_mul
 
@@ -827,24 +829,22 @@ lemma pow_vle_pow (hab : a ≤ᵥ b) (n : ℕ) : a ^ n ≤ᵥ b ^ n := by
 @[deprecated (since := "2025-12-20")] alias pow_rel_pow := pow_vle_pow
 
 lemma pow_vlt_pow (hab : a <ᵥ b) {n : ℕ} (hn : n ≠ 0) : a ^ n <ᵥ b ^ n := by
-  obtain (rfl | n) := n
-  · aesop
-  clear hn
-  induction n with
-  | zero => aesop
-  | succ _ _ => simp_all [pow_succ, mul_vlt_mul]
+  induction n using Nat.twoStepInduction with
+  | zero => contradiction
+  | one => simpa
+  | more _ _ => simp_all [pow_succ, mul_vlt_mul]
 
 @[deprecated (since := "2025-12-20")] alias pow_srel_pow := pow_vlt_pow
 
 lemma pow_vle_pow_of_vle_one (ha : a ≤ᵥ 1) {n m : ℕ} (hnm : n ≤ m) : a ^ m ≤ᵥ a ^ n := by
   obtain ⟨m, rfl⟩ := exists_add_of_le hnm
-  simpa [pow_add] using vle_mul_left (a ^ n) (pow_vle_pow ha m)
+  simpa [pow_add] using mul_vle_mul_right (pow_vle_pow ha m) _
 
 @[deprecated (since := "2025-12-20")] alias pow_rel_pow_of_rel_one := pow_vle_pow_of_vle_one
 
 lemma pow_vle_pow_of_one_vle (ha : 1 ≤ᵥ a) {n m : ℕ} (hnm : n ≤ m) : a ^ n ≤ᵥ a ^ m := by
   obtain ⟨m, rfl⟩ := exists_add_of_le hnm
-  simpa [pow_add] using vle_mul_left (a ^ n) (pow_vle_pow ha m)
+  simpa [pow_add] using mul_vle_mul_right (pow_vle_pow ha m) _
 
 @[deprecated (since := "2025-12-20")] alias pow_rel_pow_of_one_rel := pow_vle_pow_of_one_vle
 
@@ -867,12 +867,12 @@ lemma zero_vlt_iff : 0 <ᵥ a ↔ a ≠ 0 := by
 @[deprecated (since := "2025-12-20")] alias zero_srel_iff := zero_vlt_iff
 
 lemma vle_div_iff (hc : c ≠ 0) : a ≤ᵥ b / c ↔ a * c ≤ᵥ b := by
-  rw [← vle_mul_right_iff (c := c) (by simpa), div_mul_cancel₀ _ (by aesop)]
+  rw [← mul_vle_mul_iff_left (by simpa), div_mul_cancel₀ _ (by aesop)]
 
 @[deprecated (since := "2025-12-20")] alias rel_div_iff := vle_div_iff
 
 lemma div_vle_iff (hc : c ≠ 0) : a / c ≤ᵥ b ↔ a ≤ᵥ b * c := by
-  rw [← vle_mul_right_iff (c := c) (by simpa), div_mul_cancel₀ _ (by aesop)]
+  rw [← mul_vle_mul_iff_left (by simpa), div_mul_cancel₀ _ (by aesop)]
 
 @[deprecated (since := "2025-12-20")] alias div_rel_iff := div_vle_iff
 
@@ -901,8 +901,8 @@ lemma inv_vlt_one (hx : x ≠ 0) : x⁻¹ <ᵥ 1 ↔ 1 <ᵥ x :=
 
 @[deprecated (since := "2025-12-20")] alias inv_srel_one := inv_vlt_one
 
-lemma one_vlt_inv (hx : x ≠ 0) : x⁻¹ <ᵥ 1 ↔ 1 <ᵥ x :=
-  (one_vle_inv hx).not
+lemma one_vlt_inv (hx : x ≠ 0) : 1 <ᵥ x⁻¹ ↔ x <ᵥ 1 :=
+  (inv_vle_one hx).not
 
 @[deprecated (since := "2025-12-20")] alias one_srel_inv := one_vlt_inv
 

Mathlib/RingTheory/Valuation/ValuativeRel/Trivial.lean

@@ -28,7 +28,6 @@ namespace ValuativeRel
 variable {R Γ : Type} [CommRing R] [DecidableEq R] [IsDomain R]
   [LinearOrderedCommGroupWithZero Γ]
 
-
 open WithZero
 
 /-- The trivial valuative relation on a domain `R`, such that all non-zero elements are related.
@@ -39,7 +38,7 @@ def trivialRel : ValuativeRel R where
   vle_total _ _ := by split_ifs <;> simp_all
   vle_trans _ _ := by split_ifs; simp_all
   vle_add _ _ := by split_ifs; simp_all
-  vle_mul_right _ := by split_ifs <;> simp_all
+  mul_vle_mul_left _ _ := by split_ifs at * <;> simp_all
   vle_mul_cancel _ := by split_ifs <;> simp_all
   not_vle_one_zero := by split_ifs <;> simp_all