case pos
α : Type u_2
β : Type u_1
γ : Type ?u.42482
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f : β → α
hs : Finset.Nonempty s
h : ∀ (x : β), x ∈ s → f x = 0
⊢ ∃ g, (∀ (b : β), b ∈ s → f b = gcd s f * g b) ∧ gcd s g = 1

case neg
α : Type u_2
β : Type u_1
γ : Type ?u.42482
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f : β → α
hs : Finset.Nonempty s
h : ¬∀ (x : β), x ∈ s → f x = 0
⊢ ∃ g, (∀ (b : β), b ∈ s → f b = gcd s f * g b) ∧ gcd s g = 1
α : Type u_2
β : Type u_1
γ : Type ?u.42482
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f : β → α
hs : Finset.Nonempty s
⊢ ∃ g, (∀ (b : β), b ∈ s → f b = gcd s f * g b) ∧ gcd s g = 1
by_cases h : ∀ x ∈ s, f x = (0 : α)
case pos
α : Type u_2
β : Type u_1
γ : Type ?u.42482
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f : β → α
hs : Finset.Nonempty s
h : ∀ (x : β), x ∈ s → f x = 0
⊢ (gcd s fun x => 1) = 1
case pos
α : Type u_2
β : Type u_1
γ : Type ?u.42482
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f : β → α
hs : Finset.Nonempty s
h : ∀ (x : β), x ∈ s → f x = 0
⊢ ∃ g, (∀ (b : β), b ∈ s → f b = gcd s f * g b) ∧ gcd s g = 1
refine' ⟨fun _ ↦ 1, fun b hb ↦ by rw [h b hb, gcd_eq_zero_iff.2 h, mul_one], _⟩
no goals
case pos
α : Type u_2
β : Type u_1
γ : Type ?u.42482
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f : β → α
hs : Finset.Nonempty s
h : ∀ (x : β), x ∈ s → f x = 0
⊢ (gcd s fun x => 1) = 1
rw [gcd_eq_gcd_image, image_const hs, gcd_singleton, id, normalize_one]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.42482
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f : β → α
hs : Finset.Nonempty s
h : ∀ (x : β), x ∈ s → f x = 0
b : β
hb : b ∈ s
⊢ f b = gcd s f * (fun x => 1) b
rw [h b hb, gcd_eq_zero_iff.2 h, mul_one]
case neg
α : Type u_2
β : Type u_1
γ : Type ?u.42482
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f : β → α
hs : Finset.Nonempty s
h : ¬∀ (x : β), x ∈ s → f x = 0
g' : {b : β} → b ∈ s → α
hg : ∀ {b : β} (hb : b ∈ s), f b = gcd s f * g' hb
⊢ ∃ g, (∀ (b : β), b ∈ s → f b = gcd s f * g b) ∧ gcd s g = 1
case neg
α : Type u_2
β : Type u_1
γ : Type ?u.42482
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f : β → α
hs : Finset.Nonempty s
h : ¬∀ (x : β), x ∈ s → f x = 0
⊢ ∃ g, (∀ (b : β), b ∈ s → f b = gcd s f * g b) ∧ gcd s g = 1
choose g' hg using @gcd_dvd _ _ _ _ s f
case neg
α : Type u_2
β : Type u_1
γ : Type ?u.42482
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f : β → α
hs : Finset.Nonempty s
g' : {b : β} → b ∈ s → α
hg : ∀ {b : β} (hb : b ∈ s), f b = gcd s f * g' hb
h : ∃ x, x ∈ s ∧ f x ≠ 0
⊢ ∃ g, (∀ (b : β), b ∈ s → f b = gcd s f * g b) ∧ gcd s g = 1
case neg
α : Type u_2
β : Type u_1
γ : Type ?u.42482
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f : β → α
hs : Finset.Nonempty s
h : ¬∀ (x : β), x ∈ s → f x = 0
g' : {b : β} → b ∈ s → α
hg : ∀ {b : β} (hb : b ∈ s), f b = gcd s f * g' hb
⊢ ∃ g, (∀ (b : β), b ∈ s → f b = gcd s f * g b) ∧ gcd s g = 1
push_neg  at h
case neg.refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.42482
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f : β → α
hs : Finset.Nonempty s
g' : {b : β} → b ∈ s → α
hg : ∀ {b : β} (hb : b ∈ s), f b = gcd s f * g' hb
h : ∃ x, x ∈ s ∧ f x ≠ 0
b : β
hb : b ∈ s
⊢ f b = gcd s f * (fun b => if hb : b ∈ s then g' hb else 0) b

case neg.refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.42482
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f : β → α
hs : Finset.Nonempty s
g' : {b : β} → b ∈ s → α
hg : ∀ {b : β} (hb : b ∈ s), f b = gcd s f * g' hb
h : ∃ x, x ∈ s ∧ f x ≠ 0
b : β
hb : b ∈ s
⊢ f b = gcd s f * if hb : b ∈ s then g' hb else 0
case neg
α : Type u_2
β : Type u_1
γ : Type ?u.42482
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f : β → α
hs : Finset.Nonempty s
g' : {b : β} → b ∈ s → α
hg : ∀ {b : β} (hb : b ∈ s), f b = gcd s f * g' hb
h : ∃ x, x ∈ s ∧ f x ≠ 0
⊢ ∃ g, (∀ (b : β), b ∈ s → f b = gcd s f * g b) ∧ gcd s g = 1
refine' ⟨fun b ↦ if hb : b ∈ s then g' hb else 0, fun b hb ↦ _,
    extract_gcd' f _ h <| fun b hb ↦ _⟩
case neg.refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.42482
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f : β → α
hs : Finset.Nonempty s
g' : {b : β} → b ∈ s → α
hg : ∀ {b : β} (hb : b ∈ s), f b = gcd s f * g' hb
h : ∃ x, x ∈ s ∧ f x ≠ 0
b : β
hb : b ∈ s
⊢ f b = gcd s f * if hb : b ∈ s then g' hb else 0
case neg.refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.42482
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f : β → α
hs : Finset.Nonempty s
g' : {b : β} → b ∈ s → α
hg : ∀ {b : β} (hb : b ∈ s), f b = gcd s f * g' hb
h : ∃ x, x ∈ s ∧ f x ≠ 0
b : β
hb : b ∈ s
⊢ f b = gcd s f * (fun b => if hb : b ∈ s then g' hb else 0) b

case neg.refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.42482
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f : β → α
hs : Finset.Nonempty s
g' : {b : β} → b ∈ s → α
hg : ∀ {b : β} (hb : b ∈ s), f b = gcd s f * g' hb
h : ∃ x, x ∈ s ∧ f x ≠ 0
b : β
hb : b ∈ s
⊢ f b = gcd s f * if hb : b ∈ s then g' hb else 0
simp only [hb, hg, dite_true]
no goals
case neg.refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.42482
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f : β → α
hs : Finset.Nonempty s
g' : {b : β} → b ∈ s → α
hg : ∀ {b : β} (hb : b ∈ s), f b = gcd s f * g' hb
h : ∃ x, x ∈ s ∧ f x ≠ 0
b : β
hb : b ∈ s
⊢ f b = gcd s f * if hb : b ∈ s then g' hb else 0
rw [dif_pos hb, hg hb]