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
β : Type u_1
f : β → ℕ
s : Finset β
x : β
hx : x ∈ s
hfz : f x ≠ 0
⊢ (gcd s fun b => f b / gcd s f) = 1
obtain ⟨g, he, hg⟩ := Finset.extract_gcd f ⟨x, hx⟩
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
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
refine' (Finset.gcd_congr rfl fun a ha => _).trans hg
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
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
rw [he a ha, Nat.mul_div_cancel_left]
no goals
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
exact Nat.pos_of_ne_zero (mt Finset.gcd_eq_zero_iff.1 fun h => hfz <| h x hx)