diff --git a/src/Init/Data/Fin/Basic.lean b/src/Init/Data/Fin/Basic.lean
index 06701eee94..3d3a08c601 100644
--- a/src/Init/Data/Fin/Basic.lean
+++ b/src/Init/Data/Fin/Basic.lean
@@ -100,7 +100,7 @@ instance : ShiftLeft (Fin n) where
 instance : ShiftRight (Fin n) where
   shiftRight := Fin.shiftRight
 
-instance ofNatInst : OfNat (Fin (no_index (n+1))) i where
+instance instOfNat : OfNat (Fin (no_index (n+1))) i where
   ofNat := Fin.ofNat i
 
 instance : Inhabited (Fin (no_index (n+1))) where
diff --git a/src/Init/Data/Int/Basic.lean b/src/Init/Data/Int/Basic.lean
index 26f4d9dc4f..27378a4e0f 100644
--- a/src/Init/Data/Int/Basic.lean
+++ b/src/Init/Data/Int/Basic.lean
@@ -49,7 +49,7 @@ attribute [extern "lean_int_neg_succ_of_nat"] Int.negSucc
 
 instance : Coe Nat Int := ⟨Int.ofNat⟩
 
-instance ofNatInst : OfNat Int n where
+instance instOfNat : OfNat Int n where
   ofNat := Int.ofNat n
 
 namespace Int
diff --git a/src/Init/Data/UInt/Basic.lean b/src/Init/Data/UInt/Basic.lean
index 25a49e4f48..9af27276f4 100644
--- a/src/Init/Data/UInt/Basic.lean
+++ b/src/Init/Data/UInt/Basic.lean
@@ -39,7 +39,7 @@ def UInt8.shiftRight (a b : UInt8) : UInt8 := ⟨a.val >>> (modn b 8).val⟩
 def UInt8.lt (a b : UInt8) : Prop := a.val < b.val
 def UInt8.le (a b : UInt8) : Prop := a.val ≤ b.val
 
-instance UInt8.ofNatInst : OfNat UInt8 n := ⟨UInt8.ofNat n⟩
+instance UInt8.instOfNat : OfNat UInt8 n := ⟨UInt8.ofNat n⟩
 instance : Add UInt8       := ⟨UInt8.add⟩
 instance : Sub UInt8       := ⟨UInt8.sub⟩
 instance : Mul UInt8       := ⟨UInt8.mul⟩
@@ -110,7 +110,7 @@ def UInt16.shiftRight (a b : UInt16) : UInt16 := ⟨a.val >>> (modn b 16).val⟩
 def UInt16.lt (a b : UInt16) : Prop := a.val < b.val
 def UInt16.le (a b : UInt16) : Prop := a.val ≤ b.val
 
-instance UInt16.ofNatInst : OfNat UInt16 n := ⟨UInt16.ofNat n⟩
+instance UInt16.instOfNat : OfNat UInt16 n := ⟨UInt16.ofNat n⟩
 instance : Add UInt16       := ⟨UInt16.add⟩
 instance : Sub UInt16       := ⟨UInt16.sub⟩
 instance : Mul UInt16       := ⟨UInt16.mul⟩
@@ -183,7 +183,7 @@ def UInt8.toUInt32 (a : UInt8) : UInt32 := a.toNat.toUInt32
 @[extern "lean_uint16_to_uint32"]
 def UInt16.toUInt32 (a : UInt16) : UInt32 := a.toNat.toUInt32
 
-instance UInt32.ofNatInst : OfNat UInt32 n := ⟨UInt32.ofNat n⟩
+instance UInt32.instOfNat : OfNat UInt32 n := ⟨UInt32.ofNat n⟩
 instance : Add UInt32       := ⟨UInt32.add⟩
 instance : Sub UInt32       := ⟨UInt32.sub⟩
 instance : Mul UInt32       := ⟨UInt32.mul⟩
@@ -243,7 +243,7 @@ def UInt16.toUInt64 (a : UInt16) : UInt64 := a.toNat.toUInt64
 @[extern "lean_uint32_to_uint64"]
 def UInt32.toUInt64 (a : UInt32) : UInt64 := a.toNat.toUInt64
 
-instance UInt64.ofNatInst : OfNat UInt64 n := ⟨UInt64.ofNat n⟩
+instance UInt64.instOfNat : OfNat UInt64 n := ⟨UInt64.ofNat n⟩
 instance : Add UInt64       := ⟨UInt64.add⟩
 instance : Sub UInt64       := ⟨UInt64.sub⟩
 instance : Mul UInt64       := ⟨UInt64.mul⟩
@@ -321,7 +321,7 @@ def USize.toUInt32 (a : USize) : UInt32 := a.toNat.toUInt32
 def USize.lt (a b : USize) : Prop := a.val < b.val
 def USize.le (a b : USize) : Prop := a.val ≤ b.val
 
-instance USize.ofNatInst : OfNat USize n := ⟨USize.ofNat n⟩
+instance USize.instOfNat : OfNat USize n := ⟨USize.ofNat n⟩
 instance : Add USize       := ⟨USize.add⟩
 instance : Sub USize       := ⟨USize.sub⟩
 instance : Mul USize       := ⟨USize.mul⟩
diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean
index 32c60a5323..8fadff9754 100644
--- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean
+++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean
@@ -26,7 +26,7 @@ def fromExpr? (e : Expr) : SimpM (Option Value) := do
 
 def Value.toExpr (v : Value) : Expr :=
   let vExpr := mkRawNatLit v.value
-  mkApp2 v.ofNatFn vExpr (mkApp2 (mkConst ``Fin.ofNatInst) (Lean.toExpr (v.size - 1)) vExpr)
+  mkApp2 v.ofNatFn vExpr (mkApp2 (mkConst ``Fin.instOfNat) (Lean.toExpr (v.size - 1)) vExpr)
 
 @[inline] def reduceBin (declName : Name) (arity : Nat) (op : Nat → Nat → Nat) (e : Expr) : SimpM (Option Step) := do
   unless e.isAppOfArity declName arity do return none
diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean
index 94325df2eb..e368c72632 100644
--- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean
+++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean
@@ -26,7 +26,7 @@ def fromExpr? (e : Expr) : SimpM (Option Int) := do
 def toExpr (v : Int) : Expr :=
   let n := v.natAbs
   let r := mkRawNatLit n
-  let e := mkApp3 (mkConst ``OfNat.ofNat [levelZero]) (mkConst ``Int) r (mkApp (mkConst ``ofNatInst) r)
+  let e := mkApp3 (mkConst ``OfNat.ofNat [levelZero]) (mkConst ``Int) r (mkApp (mkConst ``instOfNat) r)
   if v < 0 then
     mkAppN (mkConst ``Neg.neg [levelZero]) #[mkConst ``Int, mkConst ``instNegInt, e]
   else
diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean
index ade9e5dff9..10bd14c76d 100644
--- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean
+++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean
@@ -28,7 +28,7 @@ def $fromExpr (e : Expr) : SimpM (Option Value) := do
 
 def $toExpr (v : Value) : Expr :=
   let vExpr := mkRawNatLit v.value.val
-  mkApp2 v.ofNatFn vExpr (mkApp (mkConst $(quote (typeName.getId ++ `ofNatInst))) vExpr)
+  mkApp2 v.ofNatFn vExpr (mkApp (mkConst $(quote (typeName.getId ++ `instOfNat))) vExpr)
 
 @[inline] def reduceBin (declName : Name) (arity : Nat) (op : $typeName → $typeName → $typeName) (e : Expr) : SimpM (Option Step) := do
   unless e.isAppOfArity declName arity do return none