[GOAL]
β : Type u_1
f : β → ℕ
s : Finset β
x : β
hx : x ∈ s
hfz : f x ≠ 0
⊢ (gcd s fun b => f b / gcd s f) = 1
[PROOFSTEP]
obtain ⟨g, he, hg⟩ := Finset.extract_gcd f ⟨x, hx⟩
[GOAL]
case intro.intro
β : Type u_1
f : β → ℕ
s : Finset β
x : β
hx : x ∈ s
hfz : f x ≠ 0
g : β → ℕ
he : ∀ (b : β), b ∈ s → f b = gcd s f * g b
hg : gcd s g = 1
⊢ (gcd s fun b => f b / gcd s f) = 1
[PROOFSTEP]
refine' (Finset.gcd_congr rfl fun a ha => _).trans hg
[GOAL]
case intro.intro
β : Type u_1
f : β → ℕ
s : Finset β
x : β
hx : x ∈ s
hfz : f x ≠ 0
g : β → ℕ
he : ∀ (b : β), b ∈ s → f b = gcd s f * g b
hg : gcd s g = 1
a : β
ha : a ∈ s
⊢ f a / gcd s f = g a
[PROOFSTEP]
rw [he a ha, Nat.mul_div_cancel_left]
[GOAL]
case intro.intro.H
β : Type u_1
f : β → ℕ
s : Finset β
x : β
hx : x ∈ s
hfz : f x ≠ 0
g : β → ℕ
he : ∀ (b : β), b ∈ s → f b = gcd s f * g b
hg : gcd s g = 1
a : β
ha : a ∈ s
⊢ 0 < gcd s f
[PROOFSTEP]
exact Nat.pos_of_ne_zero (mt Finset.gcd_eq_zero_iff.1 fun h => hfz <| h x hx)
[GOAL]
β : Type u_1
f : β → ℤ
s : Finset β
x : β
hx : x ∈ s
hfz : f x ≠ 0
⊢ (gcd s fun b => f b / gcd s f) = 1
[PROOFSTEP]
obtain ⟨g, he, hg⟩ := Finset.extract_gcd f ⟨x, hx⟩
[GOAL]
case intro.intro
β : Type u_1
f : β → ℤ
s : Finset β
x : β
hx : x ∈ s
hfz : f x ≠ 0
g : β → ℤ
he : ∀ (b : β), b ∈ s → f b = gcd s f * g b
hg : gcd s g = 1
⊢ (gcd s fun b => f b / gcd s f) = 1
[PROOFSTEP]
refine' (Finset.gcd_congr rfl fun a ha => _).trans hg
[GOAL]
case intro.intro
β : Type u_1
f : β → ℤ
s : Finset β
x : β
hx : x ∈ s
hfz : f x ≠ 0
g : β → ℤ
he : ∀ (b : β), b ∈ s → f b = gcd s f * g b
hg : gcd s g = 1
a : β
ha : a ∈ s
⊢ f a / gcd s f = g a
[PROOFSTEP]
rw [he a ha, Int.mul_ediv_cancel_left]
[GOAL]
case intro.intro.H
β : Type u_1
f : β → ℤ
s : Finset β
x : β
hx : x ∈ s
hfz : f x ≠ 0
g : β → ℤ
he : ∀ (b : β), b ∈ s → f b = gcd s f * g b
hg : gcd s g = 1
a : β
ha : a ∈ s
⊢ gcd s f ≠ 0
[PROOFSTEP]
exact mt Finset.gcd_eq_zero_iff.1 fun h => hfz <| h x hx
[GOAL]
K : Type u_1
inst✝ : Field K
β : Type u_2
f : β → Polynomial K
s : Finset β
x : β
hx : x ∈ s
hfz : f x ≠ 0
⊢ (gcd s fun b => f b / gcd s f) = 1
[PROOFSTEP]
obtain ⟨g, he, hg⟩ := Finset.extract_gcd f ⟨x, hx⟩
[GOAL]
case intro.intro
K : Type u_1
inst✝ : Field K
β : Type u_2
f : β → Polynomial K
s : Finset β
x : β
hx : x ∈ s
hfz : f x ≠ 0
g : β → Polynomial K
he : ∀ (b : β), b ∈ s → f b = gcd s f * g b
hg : gcd s g = 1
⊢ (gcd s fun b => f b / gcd s f) = 1
[PROOFSTEP]
refine' (Finset.gcd_congr rfl fun a ha => _).trans hg
[GOAL]
case intro.intro
K : Type u_1
inst✝ : Field K
β : Type u_2
f : β → Polynomial K
s : Finset β
x : β
hx : x ∈ s
hfz : f x ≠ 0
g : β → Polynomial K
he : ∀ (b : β), b ∈ s → f b = gcd s f * g b
hg : gcd s g = 1
a : β
ha : a ∈ s
⊢ f a / gcd s f = g a
[PROOFSTEP]
rw [he a ha, EuclideanDomain.mul_div_cancel_left]
[GOAL]
case intro.intro.a0
K : Type u_1
inst✝ : Field K
β : Type u_2
f : β → Polynomial K
s : Finset β
x : β
hx : x ∈ s
hfz : f x ≠ 0
g : β → Polynomial K
he : ∀ (b : β), b ∈ s → f b = gcd s f * g b
hg : gcd s g = 1
a : β
ha : a ∈ s
⊢ gcd s f ≠ 0
[PROOFSTEP]
exact mt Finset.gcd_eq_zero_iff.1 fun h => hfz <| h x hx
