diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index 295194601a..09b114bbb8 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -2125,7 +2125,7 @@ Examples:
 
 /-! ### Repr and ToString -/
 
-protected def Array.repr {α : Type u} [Repr α] (xs : Array α) : Std.Format :=
+protected def repr {α : Type u} [Repr α] (xs : Array α) : Std.Format :=
   let _ : Std.ToFormat α := ⟨repr⟩
   if xs.size == 0 then
     "#[]"
diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean
index c93343f101..175d15d50c 100644
--- a/src/Init/Data/BitVec/Basic.lean
+++ b/src/Init/Data/BitVec/Basic.lean
@@ -210,7 +210,7 @@ protected def toHex {n : Nat} (x : BitVec n) : String :=
   String.Internal.append t s
 
 /-- `BitVec` representation. -/
-protected def BitVec.repr (a : BitVec n) : Std.Format :=
+protected def repr (a : BitVec n) : Std.Format :=
   "0x" ++ (a.toHex : Std.Format) ++ "#" ++ repr n
 
 instance : Repr (BitVec n) where
diff --git a/src/Init/Data/Option/Lemmas.lean b/src/Init/Data/Option/Lemmas.lean
index d0e823c625..723358597a 100644
--- a/src/Init/Data/Option/Lemmas.lean
+++ b/src/Init/Data/Option/Lemmas.lean
@@ -744,7 +744,7 @@ theorem elim_guard : (guard p a).elim b f = if p a then f a else b := by
   cases h : p a <;> simp [*, guard]
 
 @[simp]
-theorem Option.elim_map {f : α → β} {g' : γ} {g : β → γ} (o : Option α) :
+theorem elim_map {f : α → β} {g' : γ} {g : β → γ} (o : Option α) :
     (o.map f).elim g' g = o.elim g' (g ∘ f) := by
   cases o <;> simp
 
diff --git a/src/Init/Data/Rat/Lemmas.lean b/src/Init/Data/Rat/Lemmas.lean
index 9e54e00aa6..6862fafbfd 100644
--- a/src/Init/Data/Rat/Lemmas.lean
+++ b/src/Init/Data/Rat/Lemmas.lean
@@ -1296,12 +1296,12 @@ theorem ceil_lt {x : Rat} :
 -/
 
 @[simp, grind =]
-theorem Rat.abs_zero :
+theorem abs_zero :
     (0 : Rat).abs = 0 := by
   simp [Rat.abs]
 
 @[simp]
-theorem Rat.abs_nonneg {x : Rat} :
+theorem abs_nonneg {x : Rat} :
     0 ≤ x.abs := by
   simp only [Rat.abs]
   split <;> rename_i hle
@@ -1310,11 +1310,11 @@ theorem Rat.abs_nonneg {x : Rat} :
     simp only [Rat.not_le] at hle
     rwa [Rat.lt_neg_iff, Rat.neg_zero]
 
-theorem Rat.abs_of_nonneg {x : Rat} (h : 0 ≤ x) :
+theorem abs_of_nonneg {x : Rat} (h : 0 ≤ x) :
     x.abs = x := by
   rw [Rat.abs, if_pos h]
 
-theorem Rat.abs_of_nonpos {x : Rat} (h : x ≤ 0) :
+theorem abs_of_nonpos {x : Rat} (h : x ≤ 0) :
     x.abs = -x := by
   rw [Rat.abs]
   split
@@ -1322,7 +1322,7 @@ theorem Rat.abs_of_nonpos {x : Rat} (h : x ≤ 0) :
   · rfl
 
 @[simp, grind =]
-theorem Rat.abs_neg {x : Rat} :
+theorem abs_neg {x : Rat} :
     (-x).abs = x.abs := by
   simp only [Rat.abs]
   split <;> split
@@ -1337,12 +1337,12 @@ theorem Rat.abs_neg {x : Rat} :
     apply Rat.le_of_lt
     assumption
 
-theorem Rat.abs_sub_comm {x y : Rat} :
+theorem abs_sub_comm {x y : Rat} :
     (x - y).abs = (y - x).abs := by
   rw [← Rat.neg_sub, Rat.abs_neg]
 
 @[simp]
-theorem Rat.abs_eq_zero_iff {x : Rat} :
+theorem abs_eq_zero_iff {x : Rat} :
     x.abs = 0 ↔ x = 0 := by
   simp only [Rat.abs]
   split
@@ -1352,7 +1352,7 @@ theorem Rat.abs_eq_zero_iff {x : Rat} :
       rw [← Rat.neg_neg (a := x), h, Rat.neg_zero]
     · simp +contextual
 
-theorem Rat.abs_pos_iff {x : Rat} :
+theorem abs_pos_iff {x : Rat} :
     0 < x.abs ↔ x ≠ 0 := by
   apply Iff.intro
   · intro hpos
@@ -1371,8 +1371,10 @@ theorem Rat.abs_pos_iff {x : Rat} :
 # instances
 -/
 
-instance Rat.instAssociativeHAdd : Std.Associative (α := Rat) (· + ·) := ⟨Rat.add_assoc⟩
-instance Rat.instCommutativeHAdd : Std.Commutative (α := Rat) (· + ·) := ⟨Rat.add_comm⟩
+instance instAssociativeHAdd : Std.Associative (α := Rat) (· + ·) := ⟨Rat.add_assoc⟩
+instance instCommutativeHAdd : Std.Commutative (α := Rat) (· + ·) := ⟨Rat.add_comm⟩
 instance : Std.LawfulIdentity (· + ·) (0 : Rat) where
   left_id := Rat.zero_add
   right_id := Rat.add_zero
+
+end Rat
diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean
index 63e249c24a..f2cb884edd 100644
--- a/src/Init/Data/Vector/Lemmas.lean
+++ b/src/Init/Data/Vector/Lemmas.lean
@@ -521,7 +521,7 @@ protected theorem ext {xs ys : Vector α n} (h : (i : Nat) → (_ : i < n) → x
   rw [← toList_toArray, Array.sum_toList, sum_toArray]
 
 @[simp, grind =]
-theorem Vector.toList_zip {as : Vector α n} {bs : Vector β n} :
+theorem toList_zip {as : Vector α n} {bs : Vector β n} :
     (Vector.zip as bs).toList = List.zip as.toList bs.toList := by
   rw [mk_zip_mk, toList_mk, Array.toList_zip, toList_toArray, toList_toArray]