Let $A \subseteq G$ be a finite subset of a group. Suppose that $|A^2| \le K|A|$. Then there is a $2^{12}K^{36}$-approximate subgroup $S \subseteq (A^{−1}A)^2$ such that $|S| \le 16K^{12}|A|$ and $|A \cap Sa| \ge \frac 1{2K} |A|$ for some $a \in A$.
This is Proposition 3.3 in the lecture notes and exists_isApproximateSubgroup_of_small_doubling in the Lean code.
⚠ The lecture notes currently have a typo: They say $|A \cap Sa| \ge \frac 1{2K}$ instead of $|A \cap Sa| \ge \frac 1{2K} |A|$. Be also aware that the $S$ in the statement is $S^2$ in the proof.
