[codethief]

> Technically speaking the elements in the supertype are all distinct from the elements in the subtype and viceversa.

Emphasis on "technically". The embedding is trivial. The Lean docs linked by the GP suggest to put those technicalities aside:

> Even though they are pairs syntactically, Subtype should really be thought of as elements of the base type with associated proof obligations.

[gugagore]

Right, though the embedding is trivial, the conceptual distinction is not. In Lean, a subtype is a refinement that restricts by proof. In OOP, a subclass augments or overrides behavior. It's composition versus inheritance. The trivial embedding masks a fundamental shift in what "subtype" means.