deprecations

Author: kim-em

Batteries/Control/AlternativeMonad.lean

@@ -104,7 +104,7 @@ section AlternativeMonad
 
 @[simp] theorem seq_failure [AlternativeMonad m] [LawfulAlternative m] [LawfulMonad m]
     (x : m (α → β)) : x <*> failure = x *> failure := by
-  simp only [seq_eq_bind, map_failure, seqRight_eq, bind_map_left]
+  simp only [seq_eq_bind_map, map_failure, seqRight_eq, bind_map_left]
 
 end AlternativeMonad
 

Batteries/Data/Array/Match.lean

@@ -58,7 +58,7 @@ def PrefixTable.extend [BEq α] (t : PrefixTable α) (x : α) : PrefixTable α w
     rw [Array.getElem_push]
     split
     · exact t.valid ..
-    · next h => exact Nat.le_trans (Nat.lt_succ.1 <| Fin.isLt ..) (Nat.not_lt.1 h)
+    · next h => exact Nat.le_trans (Nat.lt_succ_iff.1 <| Fin.isLt ..) (Nat.not_lt.1 h)
 
 /-- Make prefix table from a pattern array -/
 def mkPrefixTable [BEq α] (xs : Array α) : PrefixTable α := xs.foldl (·.extend) default

Batteries/Data/UnionFind/Basic.lean

@@ -145,7 +145,7 @@ theorem rank'_lt_rankMax (self : UnionFind) (i : Nat) (h) : (self.arr[i]).rank <
     | a::l, _, List.Mem.head _ => by dsimp; apply Nat.le_max_left
     | a::l, _, .tail _ h => by dsimp; exact Nat.le_trans (go h) (Nat.le_max_right ..)
   simp only [rankMax, ← Array.foldr_toList]
-  exact Nat.lt_succ.2 <| go (self.arr.toList.getElem_mem _)
+  exact Nat.lt_succ_iff.2 <| go (self.arr.toList.getElem_mem _)
 
 theorem rankD_lt_rankMax (self : UnionFind) (i : Nat) :
     rankD self.arr i < self.rankMax := by

Batteries/Data/UnionFind/Lemmas.lean

@@ -22,7 +22,7 @@ namespace Batteries.UnionFind
     parentD (arr.push ⟨arr.size, 0⟩) a = parentD arr a := by
   simp [parentD]; split <;> split <;> try simp [Array.getElem_push, *]
   · next h1 h2 =>
-    simp [Nat.lt_succ] at h1 h2
+    simp [Nat.lt_succ_iff] at h1 h2
     exact Nat.le_antisymm h2 h1
   · next h1 h2 => cases h1 (Nat.lt_succ_of_lt h2)
 

Batteries/Lean/EStateM.lean

@@ -70,14 +70,14 @@ theorem run_seq (f : EStateM ε σ (α → β)) (x : EStateM ε σ α) (s : σ)
     (f <*> x).run s = match f.run s with
     | .ok g s => Result.map g (x.run s)
     | .error e s => .error e s := by
-  simp only [seq_eq_bind, run_bind, run_map]
+  simp only [seq_eq_bind_map, run_bind, run_map]
   cases f.run s <;> rfl
 
 theorem run'_seq (f : EStateM ε σ (α → β)) (x : EStateM ε σ α) (s : σ) :
     (f <*> x).run' s = match f.run s with
     | .ok g s => Option.map g (x.run' s)
     | .error _ _ => none := by
-  simp only [seq_eq_bind, run'_bind, run'_map]
+  simp only [seq_eq_bind_map, run'_bind, run'_map]
   cases f.run s <;> rfl
 
 @[simp] theorem run_seqLeft (x : EStateM ε σ α) (y : EStateM ε σ β) (s : σ) :