mathlib3

0a5b9eba - feat(set_theory/game/pgame): tweak lemmas (#14810)

feat(set_theory/game/pgame): tweak lemmas (#14810) This PR does the following: - uncurry `le_of_forall_lf` and `le_of_forall_lt`. - remove `lf_of_exists_le`, as it's made redundant by `lf_of_move_right_le` and `lf_of_le_move_left`. - golfing.