!3#15260 small sets of pre-games / games / surreals are bdd

Stream: PR reviews

[Scott Morrison]

@Violeta Hernández, I've just merged one of your old mathlib3 PRs that was labelled as not-too-late, !3#15260. Mathport output should be available in <24 hours, do you think you'd be able to forward port your PR to mathlib4 then? Please ask here is you need any help with this.