RFC: expand reducibility warning about class-typed `def`s

Proposal

Lean warns about class-typed defs that aren't marked with a reducibility attribute:

/--
warning: Definition `foo` of class type must be marked with `@[reducible]` or `@[implicit_reducible]`
-/
#guard_msgs in
def foo : @Std.Refl Nat Eq where
  refl _ := rfl

(in elabMutualDef and addInstance)

I think this warning should be expanded to include e.g. a link to docs/reference, and maybe "when in doubt, choose @[implicit_reducible]".
I forgot which one was less reducible, and wanted the warning to tell me.

Additionally it should have the standard message telling the user how to turn off the linter, with set_option warn.classDefReducibility false.

Read the warning logic in src/Lean/Elab/MutualDef.lean at elabMutualDef and src/Lean/Meta/Instances.lean at addInstance. Update the class-typed def warning with reducibility guidance, relevant documentation or reference links, the suggested default, and the standard option-disabling message; done means both warning paths provide the expanded guidance.