Goldbach's Conjecture for $n \ge 30$

This is Goldbach's Conjecture restricted to even integers $n \ge 30$. Superseded: this copy was accidentally created in the wrong Lean/Mathlib environment (default env, mathlib_rev c5ea003...) and cannot be imported by the target theorem goldbach, which lives in the 777aaa6 (Lean v4.29.0-rc3) environment. Replaced by a re-published goldbach_large in that environment.