English
If a ∈ α, and for all x ∈ s we have a | f(x) − g(x), then gcd a with s.gcd f equals gcd a with s.gcd g.
Русский
Если a делит каждую разницу f(x) − g(x) на всех x ∈ s, то gcd(a, s.gcd f) = gcd(a, s.gcd g).
LaTeX
$$$\\forall s, f,g : β\\to α,\\ (∀ x, x\\in s \\to a \\mid f(x) - g(x)) \\Rightarrow gcd\\, a\\ (s.gcd\\ f) = gcd\\, a\\ (s.gcd\\ g)$$$
Lean4
theorem gcd_eq_of_dvd_sub {s : Finset β} {f g : β → α} {a : α} (h : ∀ x : β, x ∈ s → a ∣ f x - g x) :
GCDMonoid.gcd a (s.gcd f) = GCDMonoid.gcd a (s.gcd g) := by
classical
revert h
refine s.induction_on ?_ ?_
· simp
intro b s _ hi h
rw [gcd_insert, gcd_insert, gcd_comm (f b), ← gcd_assoc, hi fun x hx ↦ h _ (mem_insert_of_mem hx), gcd_comm a,
gcd_assoc, gcd_comm a (GCDMonoid.gcd _ _), gcd_comm (g b), gcd_assoc _ _ a, gcd_comm _ a]
exact congr_arg _ (gcd_eq_of_dvd_sub_right (h _ (mem_insert_self _ _)))
