chore: fix deprecations

Author: fgdorais

Batteries/Classes/Order.lean

@@ -164,7 +164,7 @@ theorem LawfulLTCmp.eq_compareOfLessAndEq
 theorem ReflCmp.compareOfLessAndEq_of_lt_irrefl [LT α] [DecidableLT α] [DecidableEq α]
     (lt_irrefl : ∀ x : α, ¬ x < x) :
     ReflCmp (α := α) (compareOfLessAndEq · ·) where
-  compare_self {x} := by simp [compareOfLessAndEq, if_neg (lt_irrefl x)]
+  compare_self {x} := by simp [compareOfLessAndEq, ite_eq_right (lt_irrefl x)]
 
 theorem LawfulBEqCmp.compareOfLessAndEq_of_lt_irrefl
     [LT α] [DecidableLT α] [DecidableEq α] [BEq α] [LawfulBEq α]

Batteries/Data/Char/AsciiCasing.lean

@@ -39,7 +39,7 @@ theorem toLower_eq_of_isUpper {c : Char} (h : c.isUpper) : c.toLower = ofNat (c.
 
 theorem toUpper_eq_of_not_isLower {c : Char} (h : ¬ c.isLower) : c.toUpper = c := by
   simp only [isLower, Bool.and_eq_true, decide_eq_true_eq] at h
-  simp only [toUpper, dif_neg h]
+  simp only [toUpper, dite_eq_right h]
 
 theorem toUpper_eq_of_isLower {c : Char} (h : c.isLower) : c.toUpper = ofNat (c.toNat - 32) := by
   ext
@@ -103,7 +103,7 @@ theorem toUpper_eq_of_isLower {c : Char} (h : c.isLower) : c.toUpper = ofNat (c.
         Bool.decide_and, not_and, Nat.not_le] at hl hu
       omega
     rw [toLower_eq_of_isUpper hu', toUpper_eq_of_isLower hl, toLower_eq_of_not_isUpper hu,
-      toNat_ofNat, if_pos hv, Nat.sub_add_cancel h, ofNat_toNat]
+      toNat_ofNat, ite_eq_left hv, Nat.sub_add_cancel h, ofNat_toNat]
   · rw [toUpper_eq_of_not_isLower hl]
 
 @[simp] theorem toUpper_toUpper_eq_toUpper (c : Char) : c.toUpper.toUpper = c.toUpper := by
@@ -119,7 +119,7 @@ theorem toUpper_eq_of_isLower {c : Char} (h : c.isLower) : c.toUpper = ofNat (c.
         isLower, not_and, Nat.not_le] at hu hl
       omega
     rw [toUpper_eq_of_isLower hl', toLower_eq_of_isUpper hu, toUpper_eq_of_not_isLower hl,
-      toNat_ofNat, if_pos hv, Nat.add_sub_cancel, ofNat_toNat]
+      toNat_ofNat, ite_eq_left hv, Nat.add_sub_cancel, ofNat_toNat]
   · rw [toLower_eq_of_not_isUpper hu]
 
 /-- Case folding for ASCII characters only.

Batteries/Data/Char/Basic.lean

@@ -89,7 +89,7 @@ private theorem of_all_eq_true_aux (h : Char.all p) (n : Nat) (hn : n.isValidCha
 
 theorem eq_true_of_all_eq_true (h : Char.all p) (c : Char) : p c := by
   have : c.toNat.isValidChar := c.valid
-  rw [← c.ofNat_toNat, ofNat, dif_pos this]
+  rw [← c.ofNat_toNat, ofNat, dite_eq_left this]
   exact of_all_eq_true_aux h c.toNat this
 
 theorem exists_eq_false_of_all_eq_false (h : Char.all p = false) :
@@ -135,7 +135,7 @@ private theorem of_any_eq_false_aux (h : Char.any p = false) (n : Nat) (hn : n.i
 
 theorem eq_false_of_any_eq_false (h : Char.any p = false) (c : Char) : p c = false := by
   have : c.toNat.isValidChar := c.valid
-  rw [← c.ofNat_toNat, ofNat, dif_pos this]
+  rw [← c.ofNat_toNat, ofNat, dite_eq_left this]
   exact of_any_eq_false_aux h c.toNat this
 
 theorem any_eq_true_iff_exists_eq_true : Char.any p = true ↔ ∃ c, p c = true := by

Batteries/Data/Fin/Coding.lean

@@ -240,7 +240,7 @@ def encodeSigma (f : Fin n → Nat) (x : (i : Fin n) × Fin (f i)) : Fin (Fin.su
       · contradiction
     | ⟨⟨i+1, hi⟩, ⟨x, hx⟩⟩ =>
       have : ¬ encodeSigma f ⟨⟨i+1, hi⟩, ⟨x, hx⟩⟩ < f 0 := by simp [encodeSigma]
-      rw [dif_neg this]
+      rw [dite_eq_right this]
       have : (encodeSigma f ⟨⟨i+1, hi⟩, ⟨x, hx⟩⟩).1 - f 0 =
           (encodeSigma (f ·.succ) ⟨⟨i, Nat.lt_of_succ_lt_succ hi⟩, ⟨x, hx⟩⟩).1 := by
         simp [encodeSigma, Nat.add_sub_cancel_left]
@@ -417,7 +417,7 @@ theorem encodeSubtype_succ_neg {P : Fin (n+1) → Prop} [DecidablePred P] (h₀
     | zero => absurd x.val.is_lt; simp
     | succ n ih =>
       if h₀ : P 0 then
-        simp only [decodeSubtype, dif_pos h₀]
+        simp only [decodeSubtype, dite_eq_left h₀]
         cases i using Fin.cases with
         | zero => rw [encodeSubtype_zero_pos h₀]
         | succ i =>
@@ -426,7 +426,7 @@ theorem encodeSubtype_succ_neg {P : Fin (n+1) → Prop} [DecidablePred P] (h₀
           congr
           rw [ih (fun i => P i.succ) ⟨i, h⟩]
       else
-        simp only [decodeSubtype, dif_neg h₀]
+        simp only [decodeSubtype, dite_eq_right h₀]
         cases i using Fin.cases with
         | zero => contradiction
         | succ i =>

Batteries/Data/Fin/Fold.lean

@@ -76,11 +76,11 @@ theorem dfoldr_eq_foldr (f : (i : Fin n) → α → α) (x) :
 theorem dfoldlM_loop_lt [Monad m] (f : ∀ (i : Fin n), α i.castSucc → m (α i.succ)) (h : i < n) (x) :
     dfoldlM.loop n α f i (Nat.lt_add_right 1 h) x =
       (f ⟨i, h⟩ x) >>= (dfoldlM.loop n α f (i+1) (Nat.add_lt_add_right h 1)) := by
-  rw [dfoldlM.loop, dif_pos h]
+  rw [dfoldlM.loop, dite_eq_left h]
 
 theorem dfoldlM_loop_eq [Monad m] (f : ∀ (i : Fin n), α i.castSucc → m (α i.succ)) (x) :
     dfoldlM.loop n α f n (Nat.le_refl _) x = pure x := by
-  rw [dfoldlM.loop, dif_neg (Nat.lt_irrefl _)]; rfl
+  rw [dfoldlM.loop, dite_eq_right (Nat.lt_irrefl _)]; rfl
 
 set_option backward.isDefEq.respectTransparency false in
 @[simp] theorem dfoldlM_zero [Monad m] (f : (i : Fin 0) → α i.castSucc → m (α i.succ)) (x) :

Batteries/Data/Fin/Lemmas.lean

@@ -285,7 +285,7 @@ theorem find?_one {p : Fin 1 → Bool} : find? p = if p 0 then some 0 else none
 theorem find?_succ {p : Fin (n+1) → Bool} :
     find? p = if p 0 then some 0 else (find? (p ·.succ)).map Fin.succ := by
   simp only [findSome?_succ, Option.guard, fun a => apply_ite (Option.or · a),
-    Option.some_or, Option.none_or, map_findSome?, Option.map_if]
+    Option.some_or, Option.none_or, map_findSome?, Option.map_ite]
 
 @[grind =]
 theorem find?_eq_some_iff {p : Fin n → Bool} :
@@ -356,7 +356,7 @@ theorem findRev?_succ {p : Fin (n+1) → Bool} :
     findRev? p = if p (last n) then some (last n)
     else (findRev? fun i => p i.castSucc).map Fin.castSucc := by
   simp only [findSomeRev?_succ, Option.guard, fun a => apply_ite (Option.or · a),
-    Option.some_or, Option.none_or, map_findSomeRev?, Option.map_if]
+    Option.some_or, Option.none_or, map_findSomeRev?, Option.map_ite]
 
 theorem findRev?_one {p : Fin 1 → Bool} : findRev? p = if p 0 then some 0 else none := by
   grind [findRev?_succ]

Batteries/Data/Float/Lemmas.lean

@@ -79,7 +79,7 @@ theorem pack_unpack {spec : Format} (b : BitVec spec.numBits) :
     unfold pack
     extract_lets mantbits biasedexp
     simp only [BitVec.ofNat_toNat, BitVec.setWidth_eq, mvec]
-    rw [if_neg, if_neg]
+    rw [ite_eq_right, ite_eq_right]
     · rw [Format.mantissaBits, Nat.add_comm, Nat.add_left_cancel_iff]
       apply Nat.ne_of_lt
       have := mt BitVec.toNat_inj.mp hmvec
@@ -95,7 +95,7 @@ theorem pack_unpack {spec : Format} (b : BitVec spec.numBits) :
       false_and, decide_false, Bool.false_eq_true, ↓reduceIte, evec]
     unfold pack
     extract_lets mantbits biasedexp
-    rw [if_neg, if_pos]
+    rw [ite_eq_right, ite_eq_left]
     · congr 1
       · simp +arith [biasedexp, e, evec]
       · rw [BitVec.ofNat_toNat, BitVec.setWidth_append]

Batteries/Data/List/Lemmas.lean

@@ -302,10 +302,10 @@ theorem cons_diff (a : α) (l₁ l₂ : List α) :
       simp[*]
 
 theorem cons_diff_of_mem {a : α} {l₂ : List α} (h : a ∈ l₂) (l₁ : List α) :
-    (a :: l₁).diff l₂ = l₁.diff (l₂.erase a) := by rw [cons_diff, if_pos h]
+    (a :: l₁).diff l₂ = l₁.diff (l₂.erase a) := by rw [cons_diff, ite_eq_left h]
 
 theorem cons_diff_of_not_mem {a : α} {l₂ : List α} (h : a ∉ l₂) (l₁ : List α) :
-    (a :: l₁).diff l₂ = a :: l₁.diff l₂ := by rw [cons_diff, if_neg h]
+    (a :: l₁).diff l₂ = a :: l₁.diff l₂ := by rw [cons_diff, ite_eq_right h]
 
 theorem diff_eq_foldl : ∀ l₁ l₂ : List α, l₁.diff l₂ = foldl List.erase l₁ l₂
   | _, [] => rfl

Batteries/Data/List/Pairwise.lean

@@ -46,10 +46,10 @@ theorem pairwise_iff_get : Pairwise R l ↔ ∀ (i j) (_hij : i < j), R (get l i
 @[simp] theorem pwFilter_nil [DecidableRel R] : pwFilter R [] = [] := rfl
 
 @[simp] theorem pwFilter_cons_of_pos [DecidableRel (α := α) R] {a : α} {l : List α}
-    (h : ∀ b ∈ pwFilter R l, R a b) : pwFilter R (a :: l) = a :: pwFilter R l := if_pos h
+    (h : ∀ b ∈ pwFilter R l, R a b) : pwFilter R (a :: l) = a :: pwFilter R l := ite_eq_left h
 
 @[simp] theorem pwFilter_cons_of_neg [DecidableRel (α := α) R] {a : α} {l : List α}
-    (h : ¬∀ b ∈ pwFilter R l, R a b) : pwFilter R (a :: l) = pwFilter R l := if_neg h
+    (h : ¬∀ b ∈ pwFilter R l, R a b) : pwFilter R (a :: l) = pwFilter R l := ite_eq_right h
 
 theorem pwFilter_map [DecidableRel (α := α) R] (f : β → α) :
     ∀ l : List β, pwFilter R (map f l) = map f (pwFilter (fun x y => R (f x) (f y)) l)

Batteries/Data/String/Lemmas.lean

@@ -225,7 +225,7 @@ theorem utf8GetAux_of_valid (cs cs' : List Char) {i p : Nat} (hp : i + utf8Len c
   | [], c::cs' => simp [← hp, Pos.Raw.utf8GetAux]
   | c::cs, cs' =>
     simp only [List.cons_append, Pos.Raw.utf8GetAux, Char.reduceDefault]
-    rw [if_neg]
+    rw [ite_eq_right]
     case hnc => simp only [← hp, utf8Len_cons, Pos.Raw.ext_iff]; exact ne_self_add_add_utf8Size
     refine utf8GetAux_of_valid cs cs' ?_
     simpa [Nat.add_assoc, Nat.add_comm] using hp
@@ -246,7 +246,7 @@ theorem utf8GetAux?_of_valid (cs cs' : List Char) {i p : Nat} (hp : i + utf8Len
   | [], c::cs' => simp [← hp, Pos.Raw.utf8GetAux?]
   | c::cs, cs' =>
     simp only [List.cons_append, Pos.Raw.utf8GetAux?]
-    rw [if_neg]
+    rw [ite_eq_right]
     case hnc => simp only [← hp, Pos.Raw.ext_iff]; exact ne_self_add_add_utf8Size
     refine utf8GetAux?_of_valid cs cs' ?_
     simpa [Nat.add_assoc, Nat.add_comm] using hp
@@ -263,7 +263,7 @@ theorem utf8SetAux_of_valid (c' : Char) (cs cs' : List Char) {i p : Nat} (hp : i
   | [], c::cs' => simp [← hp, Pos.Raw.utf8SetAux]
   | c::cs, cs' =>
     simp only [Pos.Raw.utf8SetAux, List.cons_append]
-    rw [if_neg]
+    rw [ite_eq_right]
     case hnc => simp only [← hp, Pos.Raw.ext_iff]; exact ne_self_add_add_utf8Size
     refine congrArg (c::·) (utf8SetAux_of_valid c' cs cs' ?_)
     simpa [Nat.add_assoc, Nat.add_comm] using hp
@@ -307,7 +307,7 @@ theorem utf8PrevAux_of_valid {cs cs' : List Char} {c : Char} {i p : Nat}
   | [] => simp [Pos.Raw.utf8PrevAux, ← hp, Pos.Raw.add_char_eq]
   | c'::cs =>
     simp only [Pos.Raw.utf8PrevAux, List.cons_append, utf8Len_cons, ← hp]
-    rw [if_neg]
+    rw [ite_eq_right]
     case hnc =>
       simp only [Pos.Raw.le_iff, Pos.Raw.byteIdx_add_char]
       grind [!Char.utf8Size_pos]
@@ -352,7 +352,7 @@ theorem findAux_of_valid (p) : ∀ l m r,
   | l, [], r => by unfold Legacy.findAux List.takeWhile; simp
   | l, c::m, r => by
     unfold Legacy.findAux List.takeWhile
-    rw [dif_pos (by exact Nat.lt_add_of_pos_right add_utf8Size_pos)]
+    rw [dite_eq_left (by exact Nat.lt_add_of_pos_right add_utf8Size_pos)]
     have h1 := get_of_valid l (c::m++r); have h2 := next_of_valid l c (m++r)
     simp only [List.cons_append, Char.reduceDefault, List.headD_cons] at h1 h2
     simp only [List.append_assoc, List.cons_append, h1, utf8Len_cons, h2]
@@ -375,7 +375,7 @@ theorem revFindAux_of_valid (p) : ∀ l r,
   | [], r => by unfold Legacy.revFindAux List.dropWhile; simp
   | c::l, r => by
     unfold Legacy.revFindAux List.dropWhile
-    rw [dif_neg (by exact Pos.Raw.ne_of_gt add_utf8Size_pos)]
+    rw [dite_eq_right (by exact Pos.Raw.ne_of_gt add_utf8Size_pos)]
     have h1 := get_of_valid l.reverse (c::r); have h2 := prev_of_valid l.reverse c r
     simp only [utf8Len_reverse, Char.reduceDefault, List.headD_cons] at h1 h2
     simp only [List.reverse_cons, List.append_assoc, List.singleton_append,
@@ -396,7 +396,7 @@ theorem firstDiffPos_loop_eq (l₁ l₂ r₁ r₂ stop p)
   unfold List.takeWhile₂; split <;> unfold firstDiffPos.loop
   · next a r₁ b r₂ =>
     rw [
-      dif_pos <| by
+      dite_eq_left <| by
         rw [hstop, ← hl₁, ← hl₂]
         refine Nat.lt_min.2 ⟨?_, ?_⟩ <;> exact Nat.lt_add_of_pos_right add_utf8Size_pos,
       show Pos.Raw.get (ofList (l₁ ++ a :: r₁)) ⟨p⟩ = a by
@@ -414,7 +414,7 @@ theorem firstDiffPos_loop_eq (l₁ l₂ r₁ r₂ stop p)
           (by simp [hl₁]) (by simp [hl₂]) (by simp [hstop, ← Nat.add_assoc, Nat.add_right_comm])
     · simp
   · next h =>
-    rw [dif_neg] <;> simp [hstop, ← hl₁, ← hl₂, -Nat.not_lt, Nat.lt_min]
+    rw [dite_eq_right] <;> simp [hstop, ← hl₁, ← hl₂, -Nat.not_lt, Nat.lt_min]
     intro h₁ h₂
     have : ∀ {cs}, 0 < utf8Len cs → cs ≠ [] := by rintro _ h rfl; simp at h
     obtain ⟨a, as, e₁⟩ := List.exists_cons_of_ne_nil (this h₁)
@@ -761,7 +761,7 @@ theorem offsetOfPosAux_of_valid : ∀ l m r n,
   | l, [], r, n => by unfold String.Pos.Raw.offsetOfPosAux; simp
   | l, c::m, r, n => by
     unfold String.Pos.Raw.offsetOfPosAux
-    rw [if_neg (by exact Nat.not_le.2 (Nat.lt_add_of_pos_right add_utf8Size_pos))]
+    rw [ite_eq_right (by exact Nat.not_le.2 (Nat.lt_add_of_pos_right add_utf8Size_pos))]
     simp only [List.append_assoc, atEnd_of_valid l (c::m++r)]
     simp only [List.cons_append, utf8Len_cons, next_of_valid l c (m ++ r)]
     simpa [← Nat.add_assoc, Nat.add_right_comm] using
@@ -777,7 +777,7 @@ theorem foldlAux_of_valid (f : α → Char → α) : ∀ l m r a,
   | l, [], r, a => by unfold Legacy.foldlAux; simp
   | l, c::m, r, a => by
     unfold Legacy.foldlAux
-    rw [dif_pos (by exact Nat.lt_add_of_pos_right add_utf8Size_pos)]
+    rw [dite_eq_left (by exact Nat.lt_add_of_pos_right add_utf8Size_pos)]
     simp only [List.append_assoc, List.cons_append, utf8Len_cons, next_of_valid l c (m ++ r),
       get_of_valid l (c :: (m ++ r)), Char.reduceDefault, List.headD_cons, List.foldl_cons]
     simpa [← Nat.add_assoc, Nat.add_right_comm] using foldlAux_of_valid f (l++[c]) m r (f a c)
@@ -792,7 +792,7 @@ theorem foldrAux_of_valid (f : Char → α → α) (l m r a) :
   rw [← m.reverse_reverse]
   induction m.reverse generalizing r a with (unfold Legacy.foldrAux; simp)
   | cons c m IH =>
-    rw [if_pos add_utf8Size_pos]
+    rw [ite_eq_left add_utf8Size_pos]
     simp only [← Nat.add_assoc, by simpa using prev_of_valid (l ++ m.reverse) c r]
     simp only [by simpa using get_of_valid (l ++ m.reverse) (c :: r)]
     simpa using IH (c::r) (f c a)
@@ -806,7 +806,7 @@ theorem anyAux_of_valid (p : Char → Bool) : ∀ l m r,
   | l, [], r => by unfold Legacy.anyAux; simp
   | l, c::m, r => by
     unfold Legacy.anyAux
-    rw [dif_pos (by exact Nat.lt_add_of_pos_right add_utf8Size_pos)]
+    rw [dite_eq_left (by exact Nat.lt_add_of_pos_right add_utf8Size_pos)]
     simp only [List.append_assoc, List.cons_append, get_of_valid l (c :: (m ++ r)),
       Char.reduceDefault, List.headD_cons, utf8Len_cons, next_of_valid l c (m ++ r),
       Bool.if_true_left, Bool.decide_eq_true, List.any_cons]
@@ -834,7 +834,7 @@ theorem mapAux_of_valid (f : Char → Char) :
   | l, [] => by unfold Legacy.mapAux; simp
   | l, c::r => by
     unfold Legacy.mapAux
-    rw [dif_neg (by rw [atEnd_of_valid]; simp)]
+    rw [dite_eq_right (by rw [atEnd_of_valid]; simp)]
     simp only [get_of_valid l (c :: r), Char.reduceDefault,
       List.headD_cons, set_of_valid l (c :: r), List.modifyHead_cons, next_of_valid l (f c) r,
       List.map_cons]
@@ -854,7 +854,7 @@ theorem takeWhileAux_of_valid (p : Char → Bool) : ∀ l m r,
   | l, [], r => by unfold Substring.Raw.takeWhileAux List.takeWhile; simp
   | l, c::m, r => by
     unfold Substring.Raw.takeWhileAux List.takeWhile
-    rw [dif_pos (by exact Nat.lt_add_of_pos_right add_utf8Size_pos)]
+    rw [dite_eq_left (by exact Nat.lt_add_of_pos_right add_utf8Size_pos)]
     simp only [List.append_assoc, List.cons_append, get_of_valid l (c :: (m ++ r)),
       Char.reduceDefault, List.headD_cons, utf8Len_cons, next_of_valid l c (m ++ r)]
     cases p c <;> simp
@@ -952,7 +952,7 @@ theorem next : ∀ {s}, ValidFor l (m₁ ++ c :: m₂) r s →
   | _, ⟨⟩ => by
     simp only [Substring.Raw.next, utf8Len_append, utf8Len_cons, List.append_assoc,
       List.cons_append]
-    rw [if_neg (mt Pos.Raw.ext_iff.1 ?a)]
+    rw [ite_eq_right (mt Pos.Raw.ext_iff.1 ?a)]
     case a =>
       simpa [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using
         @ne_add_utf8Size_add_self (utf8Len l + utf8Len m₁) (utf8Len m₂) c
@@ -967,7 +967,7 @@ theorem prev : ∀ {s}, ValidFor l (m₁ ++ c :: m₂) r s →
     s.prev ⟨utf8Len m₁ + c.utf8Size⟩ = ⟨utf8Len m₁⟩
   | _, ⟨⟩ => by
     simp only [Substring.Raw.prev, List.append_assoc, List.cons_append]
-    rw [if_neg (mt Pos.Raw.ext_iff.1 <| Ne.symm ?a)]
+    rw [ite_eq_right (mt Pos.Raw.ext_iff.1 <| Ne.symm ?a)]
     case a => simpa [Nat.add_comm] using @ne_add_utf8Size_add_self (utf8Len l) (utf8Len m₁) c
     have := prev_of_valid (l ++ m₁) c (m₂ ++ r)
     simp only [List.append_assoc, utf8Len_append, Nat.add_assoc,