diff --git a/src/Init/Data/Array/Subarray.lean b/src/Init/Data/Array/Subarray.lean
index 682fbb204b..f38496ec4c 100644
--- a/src/Init/Data/Array/Subarray.lean
+++ b/src/Init/Data/Array/Subarray.lean
@@ -22,7 +22,7 @@ abbrev Subarray.as (s : Subarray α) : Array α := s.array
 theorem Subarray.h₁ (s : Subarray α) : s.start ≤ s.stop := s.start_le_stop
 
 @[deprecated Subarray.stop_le_array_size]
-theorem Subarray.h₂ (s : Subarray α) : s.stop ≤ s.as.size := s.stop_le_array_size
+theorem Subarray.h₂ (s : Subarray α) : s.stop ≤ s.array.size := s.stop_le_array_size
 
 namespace Subarray
 
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 27f3632e23..5a4fbcf1d9 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -897,7 +897,7 @@ theorem sub_toAdd {n} (x y : BitVec n) : x - y = x + - y := by
 
 theorem add_sub_cancel (x y : BitVec w) : x + y - y = x := by
   apply eq_of_toNat_eq
-  have y_toNat_le := Nat.le_of_lt y.toNat_lt
+  have y_toNat_le := Nat.le_of_lt y.isLt
   rw [toNat_sub, toNat_add, Nat.mod_add_mod, Nat.add_assoc, ← Nat.add_sub_assoc y_toNat_le,
     Nat.add_sub_cancel_left, Nat.add_mod_right, toNat_mod_cancel]
 
diff --git a/src/Init/Data/Stream.lean b/src/Init/Data/Stream.lean
index f045327471..54cc28b13e 100644
--- a/src/Init/Data/Stream.lean
+++ b/src/Init/Data/Stream.lean
@@ -94,7 +94,7 @@ instance : Stream (Subarray α) α where
   next? s :=
     if h : s.start < s.stop then
       have : s.start + 1 ≤ s.stop := Nat.succ_le_of_lt h
-      some (s.as.get ⟨s.start, Nat.lt_of_lt_of_le h s.stop_le_array_size⟩,
+      some (s.array.get ⟨s.start, Nat.lt_of_lt_of_le h s.stop_le_array_size⟩,
         { s with start := s.start + 1, start_le_stop := this })
     else
       none
diff --git a/src/Lean/Data/RBTree.lean b/src/Lean/Data/RBTree.lean
index a2fde26f33..f749d80f8f 100644
--- a/src/Lean/Data/RBTree.lean
+++ b/src/Lean/Data/RBTree.lean
@@ -100,7 +100,7 @@ def fromArray (l : Array α) (cmp : α → α → Ordering) : RBTree α cmp :=
   RBMap.any t (fun a _ => p a)
 
 def subset (t₁ t₂ : RBTree α cmp) : Bool :=
-  t₁.all fun a => (t₂.find? a).toBool
+  t₁.all fun a => (t₂.find? a).isSome
 
 def seteq (t₁ t₂ : RBTree α cmp) : Bool :=
   subset t₁ t₂ && subset t₂ t₁
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index ce929262f8..ee1014f944 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -1634,6 +1634,7 @@ def isLetRecAuxMVar (mvarId : MVarId) : TermElabM Bool := do
   Remark: fresh universe metavariables are created if the constant has more universe
   parameters than `explicitLevels`. -/
 def mkConst (constName : Name) (explicitLevels : List Level := []) : TermElabM Expr := do
+  Linter.checkDeprecated constName -- TODO: check is occurring too early if there are multiple alternatives. Fix if it is not ok in practice
   let cinfo ← getConstInfo constName
   if explicitLevels.length > cinfo.levelParams.length then
     throwError "too many explicit universe levels for '{constName}'"
@@ -1645,7 +1646,6 @@ def mkConst (constName : Name) (explicitLevels : List Level := []) : TermElabM E
 private def mkConsts (candidates : List (Name × List String)) (explicitLevels : List Level) : TermElabM (List (Expr × List String)) := do
   candidates.foldlM (init := []) fun result (declName, projs) => do
     -- TODO: better support for `mkConst` failure. We may want to cache the failures, and report them if all candidates fail.
-    Linter.checkDeprecated declName -- TODO: check is occurring too early if there are multiple alternatives. Fix if it is not ok in practice
     let const ← mkConst declName explicitLevels
     return (const, projs) :: result
 
diff --git a/tests/lean/deprecated.lean b/tests/lean/deprecated.lean
index d92bde5d05..4c33c854b8 100644
--- a/tests/lean/deprecated.lean
+++ b/tests/lean/deprecated.lean
@@ -31,3 +31,9 @@ def f4 (x : Nat) := x + 1
 set_option linter.deprecated false in
 #eval f2 0 + 1
 #eval f4 0 + 1
+
+@[deprecated] def Nat.z (x : Nat) := x + 1
+
+/-- warning: `Nat.z` has been deprecated -/
+#guard_msgs in
+example (n : Nat) : n.z = n + 1 := rfl