computations_in_lean. A tutorial on doing proofs with a computational flavour in the Lean proof assistant, and particularly on using the tactic polyrith