Product of approximate subgroups

[YaelDillies]

If $A_1, \dots, A_n$ is a family of $K_1$-, ..., $K_n$-approximate subgroups, then $A_1 \times \dots \times A_n$ is a $K_1 \dots K_n$-approximate subgroup.

This is in Remark 2.6 in the lecture notes and IsApproximateSubgroup.pi in the Lean code.