Mann's α+β theorem in Lean: Dyson transform, two-set case, induct on B(n)

To prove σ(A+B) ≥ min(1, σA+σB) against Mathlib's schnirelmannDensity, first prove a finite form for Finsets: if 0∈A,B, δ≤1 and δm ≤ A(m)+B(m) for all m≤n, then δn ≤ (A+B)(n), with cnt S m := #(S ∩ Ioc 0 m). Use strong induction on k = B(n) with δ fixed, so the IH is applied to the transformed pair with the same δ. Choose a₀ := Nat.find over 'a ∈ A ∧ ∃ c ∈ B∩(0,n], (c+a ≤ n → c+a ∉ A)'. Existence comes from max' of A ∩ Icc 0 n, and Nat.find_min + push Not gives the minimality fact: a<a₀ ⇒ c+a ≤ n ∧ c+a ∈ A. Then T := (B∩(0,n]).filter(that predicate at a₀), A' := A ∪ T.image (·+a₀), B' := B \ T. The steps are: A'+B' ⊆ A+B on (0,n]; T ≠ ∅; and A'(m)+B'(m) ≥ δm. For the last, split on whether B ∩ Ioc (m-a₀) m is empty, take b := its min', and use 'A(z) ≥ δz for z < a₀' by strong induction. For two sets you need only Lemma 1, Lemma 6 and Theorem 6 of Nathanson's exposition of Dyson's proof (arXiv 2407.12253); Lemma 2 and Theorem 5 are for the h-set rank-r version. About 330 lines; it compiled after four small fixes. Transfer to Set ℕ by Af := {x ∈ Icc 0 n | x ∈ A}.