chore: follow up on #8173 post-stage0 update

Author: david-christiansen

src/Lean/BuiltinDocAttr.lean

@@ -22,8 +22,8 @@ This allows the documentation of core Lean features to be visible without import
 are defined in. This is only useful during bootstrapping and should not be used outside of
 the Lean source code.
 -/
-@[builtin_init, builtin_doc]
-private def initFn :=
+@[builtin_doc]
+builtin_initialize
   registerBuiltinAttribute {
     name  := `builtin_doc
     descr := "make the docs and location of this declaration available as a builtin"

src/Lean/Elab/InheritDoc.lean

@@ -14,8 +14,8 @@ Uses documentation from a specified declaration.
 
 `@[inherit_doc decl]` is used to inherit the documentation from the declaration `decl`.
 -/
-@[builtin_init, builtin_doc]
-private def init :=
+@[builtin_doc]
+builtin_initialize
   registerBuiltinAttribute {
     name := `inherit_doc
     descr := "inherit documentation from a specified declaration"

src/Lean/Elab/MutualDef.lean

@@ -32,8 +32,8 @@ Makes the bodies of definitions available to importing modules.
 This only has an effect if both the module the definition is defined in and the importing module
 have the module system enabled.
 -/
-@[builtin_init, builtin_doc]
-private def init :=
+@[builtin_doc]
+builtin_initialize
   registerBuiltinAttribute {
     name := `expose
     descr := "(module system) Make bodies of definitions available to importing modules."
@@ -49,8 +49,8 @@ be exposed in a section tagged `@[expose]`
 This only has an effect if both the module the definition is defined in and the importing module
 have the module system enabled.
 -/
-@[builtin_init, builtin_doc]
-private def init2 :=
+@[builtin_doc]
+builtin_initialize
   registerBuiltinAttribute {
     name := `no_expose
     descr := "(module system) Negate previous `[expose]` attribute."

src/Lean/Elab/Tactic/Monotonicity.lean

@@ -36,8 +36,8 @@ Monotonicity theorems should have `Lean.Order.monotone ...` as a conclusion. The
 `monotonicity` tactic (scoped in the `Lean.Order` namespace) to automatically prove monotonicity
 for functions defined using `partial_fixpoint`.
 -/
-@[builtin_init, builtin_doc]
-private def init := registerBuiltinAttribute {
+@[builtin_doc]
+builtin_initialize registerBuiltinAttribute {
   name := `partial_fixpoint_monotone
   descr := "monotonicity theorem"
   add := fun decl _ kind => MetaM.run' do

src/Lean/Elab/Term.lean

@@ -2100,8 +2100,8 @@ builtin_initialize builtinIncrementalElabs : IO.Ref NameSet ← IO.mkRef {}
 def addBuiltinIncrementalElab (decl : Name) : IO Unit := do
   builtinIncrementalElabs.modify fun s => s.insert decl
 
-@[builtin_init, inherit_doc incrementalAttr, builtin_doc]
-private def init :=
+@[inherit_doc incrementalAttr, builtin_doc]
+builtin_initialize
   registerBuiltinAttribute {
     name            := `builtin_incremental
     descr           := s!"(builtin) {incrementalAttr.attr.descr}"

src/Lean/Meta/Instances.lean

@@ -242,8 +242,8 @@ in particular for `opaque` instances.
 To assign priorities to instances, `@[instance prio]` can be used (where `prio` is a priority).
 This corresponds to the `instance (priority := prio)` notation.
 -/
-@[builtin_init, builtin_doc]
-private def init :=
+@[builtin_doc]
+builtin_initialize
   registerBuiltinAttribute {
     name  := `instance
     descr := "type class instance"

src/Lean/Meta/Tactic/ElimInfo.lean

@@ -209,8 +209,8 @@ example (x : Three) (p : Three → Prop) : p x := by
 
 `@[cases_eliminator]` works similarly for the `cases` tactic.
 -/
-@[builtin_init, builtin_doc]
-private def init : IO Unit :=
+@[builtin_doc]
+builtin_initialize
   registerBuiltinAttribute {
     name  := `induction_eliminator
     descr := "custom `rec`-like eliminator for the `induction` tactic"
@@ -249,8 +249,8 @@ example (x : Three) (p : Three → Prop) : p x := by
 
 `@[induction_eliminator]` works similarly for the `induction` tactic.
 -/
-@[builtin_init, builtin_doc]
-private def init2 : IO Unit :=
+@[builtin_doc]
+builtin_initialize
   registerBuiltinAttribute {
     name  := `cases_eliminator
     descr := "custom `casesOn`-like eliminator for the `cases` tactic"

src/Lean/Meta/Tactic/Rfl.lean

@@ -35,8 +35,8 @@ A reflexivity lemma should have the conclusion `r x x` where `r` is an arbitrary
 It is not possible to tag reflexivity lemmas for `=` using this attribute. These are handled as a
 special case in the `rfl` tactic.
 -/
-@[builtin_init, builtin_doc]
-private def initFn := registerBuiltinAttribute {
+@[builtin_doc]
+builtin_initialize registerBuiltinAttribute {
   name := `refl
   descr := "reflexivity relation"
   add := fun decl _ kind => MetaM.run' do

src/Lean/Meta/Tactic/Simp/SimpCongrTheorems.lean

@@ -136,8 +136,8 @@ theorem Option.pbind_congr
   ...
 ```
 -/
-@[builtin_init, builtin_doc]
-private def init :=
+@[builtin_doc]
+builtin_initialize
   registerBuiltinAttribute {
     name  := `congr
     descr := "congruence theorem"

src/Lean/Meta/Tactic/Symm.lean

@@ -31,8 +31,8 @@ Tags symmetry lemmas to be used by the `symm` tactic.
 
 A symmetry lemma should be of the form `r x y → r y x` where `r` is an arbitrary relation.
 -/
-@[builtin_init, builtin_doc]
-private def initFn := registerBuiltinAttribute {
+@[builtin_doc]
+builtin_initialize registerBuiltinAttribute {
   name := `symm
   descr := "symmetric relation"
   add := fun decl _ kind => MetaM.run' do