Total law of expectation/probability Lean formalization

Formalization of the total law of expectation/probability.

HTML-rendered Lean proofs: