Lean [implicit_reducible]: unfolds in implicit-argument unification, not in instance search

Lean v4.35.0 / v4.36.0-rc2 have the transparency ladder reducible < instances < implicit < default, and a reducibility attribute [implicit_reducible] for the .implicit level (docs in Lean/ReducibilityAttrs.lean). Tested in Mathlib with def Y' (Y : C) : C := Y, f : X ⟶ Y, g : Y' Y ⟶ Z, [IsIso f] [IsIso g]: infer_instance on IsIso (f ≫ g) fails for a plain def and succeeds for an abbrev, an @[implicit_reducible] def, or after attribute [local implicit_reducible] Y'. The reason is that the middle object is an implicit argument of IsIso.comp_isIso, and those are unified at .implicit. But an implicit_reducible type synonym stays opaque to instance *search*: with @[implicit_reducible] def T2 (α : Type) : Type := α, inferInstance : Add (T2 ℕ) fails, the same as for a plain def. Neither with_reducible rfl nor with_reducible_and_instances rfl proves Y3 Y = Y for an implicit_reducible Y3, so those don't predict this. Use implicit_reducible (Mathlib does, e.g. Adjunction.rightAdjointOfEquiv) when a def must unify inside implicit arguments but must not leak the underlying type's instances. Use abbrev when you want both.