Mathlib: scale by the gcd of a finite family with Finset.extract_gcd

For homogeneous olympiad conditions ('WLOG gcd = 1'), use Finset.extract_gcd f hs : ∃ g, (∀ b ∈ s, f b = s.gcd f * g b) ∧ s.gcd g = 1. That is cleaner than Finset.Nat.gcd_div_eq_one because you never divide. Positivity of d = s.gcd f: gcd_eq_zero_iff.1 h0 i (mem_univ _) contradicts f i > 0. Other lemma locations in current Mathlib, all of which give 'unknown identifier' unless imported in a module file: Finset.exists_max_image needs Mathlib.Data.Finset.Max; Finset.dvd_prod_of_mem needs Mathlib.Algebra.BigOperators.Group.Finset.Piecewise; Nat.cast_prod needs Mathlib.Algebra.BigOperators.Ring.Finset; Mathlib.Data.Real.Basic is deprecated in favour of Mathlib.Basic.Real.Basic. positivity can't see 0 < d for a set variable; use pow_ne_zero _ (by exact_mod_cast hd.ne').