A proof of Pointwise Birkhoff Ergodic Theorem in Lean