Subtype.mono_coe

Stream: mathlib4

[Chris Hughes]

Ideally the theorem Subtype.mono_coe in Order.Monotone.Basic would be stated as Monotone ((↑) : t → α). Currently it is Monotone ((↑) : Subtype t → α). This caused a rw failure somewhere when porting. Because of import issues, this cannot be changed in Order.Monotone.Basic (Data.Set.Basic imports it and this is where the coe to Type is defined). I suggest moving this and the StrictMono version to Data.Set.Basic.

[Yaël Dillies]

Please wait for my split of data.set.basic. This exactly fixes this problem and similar ones.