chore: rm @[eqns] in SetTheory/Ordinal/Notation (#11646)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Mathlib/SetTheory/Ordinal/Notation.lean

@@ -127,18 +127,16 @@ def ofNat : ℕ → ONote
   | Nat.succ n => oadd 0 n.succPNat 0
 #align onote.of_nat ONote.ofNat
 
--- Porting note: the generated simp lemmas of `ofNat` is not good so we replace.
+-- Adaptation note:
+-- During the port we marked these lemmas with `@[eqns]` to emulate the old Lean 3 behaviour.
+-- See https://github.com/leanprover-community/mathlib4/issues/11647
 
-theorem ofNat_zero : ofNat 0 = 0 :=
+@[simp] theorem ofNat_zero : ofNat 0 = 0 :=
   rfl
 
-theorem ofNat_succ (n) : ofNat (Nat.succ n) = oadd 0 n.succPNat 0 :=
+@[simp] theorem ofNat_succ (n) : ofNat (Nat.succ n) = oadd 0 n.succPNat 0 :=
   rfl
 
-attribute [eqns ofNat_zero ofNat_succ] ofNat
-
-attribute [simp] ofNat
-
 instance nat (n : ℕ) : OfNat ONote n where
   ofNat := ofNat n