I was a bit skeptical at first about LEAN’s inheritance feature. But actually, it makes a lot of sense to use inheritance to model relationships between some definitions in mathematics. I found a use-case for inheritance over composition (although LEAN internally uses composition to model inheritance).

Reference: https://lean-lang.org/functional_programming_in_lean/functor-applicative-monad/inheritance.html.