fix lemma names

Author: YaelDillies

Mathlib/Order/SuccPred/Basic.lean

@@ -294,7 +294,7 @@ theorem succ_le_succ (h : a ≤ b) : succ a ≤ succ b := by
 theorem succ_mono : Monotone (succ : α → α) := fun _ _ => succ_le_succ
 #align order.succ_mono Order.succ_mono
 
-/-- See also `Order.succ_eq_of_wcovBy`. -/
+/-- See also `Order.succ_eq_of_covBy`. -/
 lemma le_succ_of_wcovBy (h : a ⩿ b) : b ≤ succ a := by
   obtain hab | ⟨-, hba⟩ := h.covBy_or_le_and_le
   · by_contra hba
@@ -452,9 +452,9 @@ theorem le_le_succ_iff : a ≤ b ∧ b ≤ succ a ↔ b = a ∨ b = succ a := by
 #align order.le_le_succ_iff Order.le_le_succ_iff
 
 /-- See also `Order.le_succ_of_wcovBy`. -/
-lemma succ_eq_of_wcovBy (h : a ⋖ b) : succ a = b := (succ_le_of_lt h.lt).antisymm h.wcovBy.le_succ
+lemma succ_eq_of_covBy (h : a ⋖ b) : succ a = b := (succ_le_of_lt h.lt).antisymm h.wcovBy.le_succ
 
-alias _root_.CovBy.succ_eq := succ_eq_of_wcovBy
+alias _root_.CovBy.succ_eq := succ_eq_of_covBy
 #align covby.succ_eq CovBy.succ_eq
 
 theorem le_succ_iff_eq_or_le : a ≤ succ b ↔ a = succ b ∨ a ≤ b := by
@@ -686,7 +686,7 @@ theorem pred_le_pred {a b : α} (h : a ≤ b) : pred a ≤ pred b :=
 theorem pred_mono : Monotone (pred : α → α) := fun _ _ => pred_le_pred
 #align order.pred_mono Order.pred_mono
 
-/-- See also `Order.pred_eq_of_wcovBy`. -/
+/-- See also `Order.pred_eq_of_covBy`. -/
 lemma pred_le_of_wcovBy (h : a ⩿ b) : pred b ≤ a := by
   obtain hab | ⟨-, hba⟩ := h.covBy_or_le_and_le
   · by_contra hba
@@ -834,9 +834,9 @@ theorem pred_le_le_iff {a b : α} : pred a ≤ b ∧ b ≤ a ↔ b = a ∨ b = p
 #align order.pred_le_le_iff Order.pred_le_le_iff
 
 /-- See also `Order.pred_le_of_wcovBy`. -/
-lemma pred_eq_of_wcovBy (h : a ⋖ b) : pred b = a := h.wcovBy.pred_le.antisymm (le_pred_of_lt h.lt)
+lemma pred_eq_of_covBy (h : a ⋖ b) : pred b = a := h.wcovBy.pred_le.antisymm (le_pred_of_lt h.lt)
 
-alias _root_.CovBy.pred_eq := pred_eq_of_wcovBy
+alias _root_.CovBy.pred_eq := pred_eq_of_covBy
 #align covby.pred_eq CovBy.pred_eq
 
 theorem pred_le_iff_eq_or_le : pred a ≤ b ↔ b = pred a ∨ a ≤ b := by