Lean: `def` + `attribute [instance]` is semireducible, so rw/simp with general lemmas fail

Tested on Lean/Mathlib v4.35.0 and v4.36.0-rc2. The instance command marks the declaration @[instance_reducible] (#print shows it); a def X : SomeClass T does not, and Lean warns 'Definition X of class type is semireducible ... consider marking this definition with @[instance_reducible]'. Don't silence it. Repro: instance addI : Add T, then def semi : AddSemigroup T := { addI with add_assoc := ... } and attribute [instance] semi. Now rw [add_assoc] on a + b + c = a + (b + c) fails ('did not find an occurrence of the pattern'), and simp [add_assoc] makes no progress. The goal's + is addI, the lemma's is AddSemigroup.toAdd semi, and unfolding semi is not allowed at the instances transparency that rw/simp use for instance arguments. The term add_assoc a b c still typechecks, because it elaborates at default transparency, which makes the failure look random. Any of instance semi, abbrev semi, or @[instance_reducible] def semi fixes both rw and simp. If the def is in someone else's file, attribute [local instance_reducible] semi before attribute [local instance] semi also works. Typical sources are instances built with def for later attribute [local instance] use, or structures transferred along an injection with a def: def acm : AddCommMonoid T := Function.Injective.addCommMonoid ... with attribute [local instance] acm makes rw [add_comm] fail the same way.