[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
⊢ lcm s f ∣ a ↔ ∀ (b : β), b ∈ s → f b ∣ a
[PROOFSTEP]
apply Iff.trans Multiset.lcm_dvd
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
⊢ (∀ (b : α), b ∈ Multiset.map f s.val → b ∣ a) ↔ ∀ (b : β), b ∈ s → f b ∣ a
[PROOFSTEP]
simp only [Multiset.mem_map, and_imp, exists_imp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
⊢ (∀ (b : α) (x : β), x ∈ s.val → f x = b → b ∣ a) ↔ ∀ (b : β), b ∈ s → f b ∣ a
[PROOFSTEP]
exact ⟨fun k b hb ↦ k _ _ hb rfl, fun k a' b hb h ↦ h ▸ k _ hb⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
b : β
⊢ lcm (insert b s) f = GCDMonoid.lcm (f b) (lcm s f)
[PROOFSTEP]
by_cases h : b ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
b : β
h : b ∈ s
⊢ lcm (insert b s) f = GCDMonoid.lcm (f b) (lcm s f)
[PROOFSTEP]
rw [insert_eq_of_mem h, (lcm_eq_right_iff (f b) (s.lcm f) (Multiset.normalize_lcm (s.1.map f))).2 (dvd_lcm h)]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
b : β
h : ¬b ∈ s
⊢ lcm (insert b s) f = GCDMonoid.lcm (f b) (lcm s f)
[PROOFSTEP]
apply fold_insert h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
⊢ ↑normalize (lcm s f) = lcm s f
[PROOFSTEP]
simp [lcm_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
⊢ lcm (∅ ∪ s₂) f = GCDMonoid.lcm (lcm ∅ f) (lcm s₂ f)
[PROOFSTEP]
rw [empty_union, lcm_empty, lcm_one_left, normalize_lcm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
a : β
s : Finset β
x✝ : ¬a ∈ s
ih : lcm (s ∪ s₂) f = GCDMonoid.lcm (lcm s f) (lcm s₂ f)
⊢ lcm (insert a s ∪ s₂) f = GCDMonoid.lcm (lcm (insert a s) f) (lcm s₂ f)
[PROOFSTEP]
rw [insert_union, lcm_insert, lcm_insert, ih, lcm_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f g : β → α
hs : s₁ = s₂
hfg : ∀ (a : β), a ∈ s₂ → f a = g a
⊢ lcm s₁ f = lcm s₂ g
[PROOFSTEP]
subst hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ : Finset β
f✝ f g : β → α
hfg : ∀ (a : β), a ∈ s₁ → f a = g a
⊢ lcm s₁ f = lcm s₁ g
[PROOFSTEP]
exact Finset.fold_congr hfg
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
g : γ → β
s : Finset γ
⊢ lcm (image g s) f = lcm s (f ∘ g)
[PROOFSTEP]
classical induction' s using Finset.induction with c s _ ih <;> simp [*]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
g : γ → β
s : Finset γ
⊢ lcm (image g s) f = lcm s (f ∘ g)
[PROOFSTEP]
induction' s using Finset.induction with c s _ ih
[GOAL]
case empty
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
g : γ → β
⊢ lcm (image g ∅) f = lcm ∅ (f ∘ g)
[PROOFSTEP]
simp [*]
[GOAL]
case insert
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
g : γ → β
c : γ
s : Finset γ
a✝ : ¬c ∈ s
ih : lcm (image g s) f = lcm s (f ∘ g)
⊢ lcm (image g (insert c s)) f = lcm (insert c s) (f ∘ g)
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : Nontrivial α
⊢ lcm s f = 0 ↔ 0 ∈ f '' ↑s
[PROOFSTEP]
simp only [Multiset.mem_map, lcm_def, Multiset.lcm_eq_zero_iff, Set.mem_image, mem_coe, ← Finset.mem_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
⊢ a ∣ gcd s f ↔ ∀ (b : β), b ∈ s → a ∣ f b
[PROOFSTEP]
apply Iff.trans Multiset.dvd_gcd
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
⊢ (∀ (b : α), b ∈ Multiset.map f s.val → a ∣ b) ↔ ∀ (b : β), b ∈ s → a ∣ f b
[PROOFSTEP]
simp only [Multiset.mem_map, and_imp, exists_imp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
⊢ (∀ (b : α) (x : β), x ∈ s.val → f x = b → a ∣ b) ↔ ∀ (b : β), b ∈ s → a ∣ f b
[PROOFSTEP]
exact ⟨fun k b hb ↦ k _ _ hb rfl, fun k a' b hb h ↦ h ▸ k _ hb⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
b : β
⊢ gcd (insert b s) f = GCDMonoid.gcd (f b) (gcd s f)
[PROOFSTEP]
by_cases h : b ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
b : β
h : b ∈ s
⊢ gcd (insert b s) f = GCDMonoid.gcd (f b) (gcd s f)
[PROOFSTEP]
rw [insert_eq_of_mem h, (gcd_eq_right_iff (f b) (s.gcd f) (Multiset.normalize_gcd (s.1.map f))).2 (gcd_dvd h)]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
b : β
h : ¬b ∈ s
⊢ gcd (insert b s) f = GCDMonoid.gcd (f b) (gcd s f)
[PROOFSTEP]
apply fold_insert h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
⊢ ↑normalize (gcd s f) = gcd s f
[PROOFSTEP]
simp [gcd_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
⊢ gcd (∅ ∪ s₂) f = GCDMonoid.gcd (gcd ∅ f) (gcd s₂ f)
[PROOFSTEP]
rw [empty_union, gcd_empty, gcd_zero_left, normalize_gcd]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
a : β
s : Finset β
x✝ : ¬a ∈ s
ih : gcd (s ∪ s₂) f = GCDMonoid.gcd (gcd s f) (gcd s₂ f)
⊢ gcd (insert a s ∪ s₂) f = GCDMonoid.gcd (gcd (insert a s) f) (gcd s₂ f)
[PROOFSTEP]
rw [insert_union, gcd_insert, gcd_insert, ih, gcd_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f g : β → α
hs : s₁ = s₂
hfg : ∀ (a : β), a ∈ s₂ → f a = g a
⊢ gcd s₁ f = gcd s₂ g
[PROOFSTEP]
subst hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ : Finset β
f✝ f g : β → α
hfg : ∀ (a : β), a ∈ s₁ → f a = g a
⊢ gcd s₁ f = gcd s₁ g
[PROOFSTEP]
exact Finset.fold_congr hfg
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
g : γ → β
s : Finset γ
⊢ gcd (image g s) f = gcd s (f ∘ g)
[PROOFSTEP]
classical induction' s using Finset.induction with c s _ ih <;> simp [*]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
g : γ → β
s : Finset γ
⊢ gcd (image g s) f = gcd s (f ∘ g)
[PROOFSTEP]
induction' s using Finset.induction with c s _ ih
[GOAL]
case empty
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
g : γ → β
⊢ gcd (image g ∅) f = gcd ∅ (f ∘ g)
[PROOFSTEP]
simp [*]
[GOAL]
case insert
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
g : γ → β
c : γ
s : Finset γ
a✝ : ¬c ∈ s
ih : gcd (image g s) f = gcd s (f ∘ g)
⊢ gcd (image g (insert c s)) f = gcd (insert c s) (f ∘ g)
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
⊢ gcd s f = 0 ↔ ∀ (x : β), x ∈ s → f x = 0
[PROOFSTEP]
rw [gcd_def, Multiset.gcd_eq_zero_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
⊢ (∀ (x : α), x ∈ Multiset.map f s.val → x = 0) ↔ ∀ (x : β), x ∈ s → f x = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
⊢ (∀ (x : α), x ∈ Multiset.map f s.val → x = 0) → ∀ (x : β), x ∈ s → f x = 0
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
⊢ (∀ (x : β), x ∈ s → f x = 0) → ∀ (x : α), x ∈ Multiset.map f s.val → x = 0
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
h : ∀ (x : α), x ∈ Multiset.map f s.val → x = 0
⊢ ∀ (x : β), x ∈ s → f x = 0
[PROOFSTEP]
intro b bs
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
h : ∀ (x : α), x ∈ Multiset.map f s.val → x = 0
b : β
bs : b ∈ s
⊢ f b = 0
[PROOFSTEP]
apply h (f b)
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
h : ∀ (x : α), x ∈ Multiset.map f s.val → x = 0
b : β
bs : b ∈ s
⊢ f b ∈ Multiset.map f s.val
[PROOFSTEP]
simp only [Multiset.mem_map, mem_def.1 bs]
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
h : ∀ (x : α), x ∈ Multiset.map f s.val → x = 0
b : β
bs : b ∈ s
⊢ ∃ a, a ∈ s.val ∧ f a = f b
[PROOFSTEP]
use b
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
h : ∀ (x : α), x ∈ Multiset.map f s.val → x = 0
b : β
bs : b ∈ s
⊢ b ∈ s.val ∧ f b = f b
[PROOFSTEP]
simp only [mem_def.1 bs, eq_self_iff_true, and_self]
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
h : ∀ (x : β), x ∈ s → f x = 0
⊢ ∀ (x : α), x ∈ Multiset.map f s.val → x = 0
[PROOFSTEP]
intro a as
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
h : ∀ (x : β), x ∈ s → f x = 0
a : α
as : a ∈ Multiset.map f s.val
⊢ a = 0
[PROOFSTEP]
rw [Multiset.mem_map] at as 
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
h : ∀ (x : β), x ∈ s → f x = 0
a : α
as : ∃ a_1, a_1 ∈ s.val ∧ f a_1 = a
⊢ a = 0
[PROOFSTEP]
rcases as with ⟨b, ⟨bs, rfl⟩⟩
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
h : ∀ (x : β), x ∈ s → f x = 0
b : β
bs : b ∈ s.val
⊢ f b = 0
[PROOFSTEP]
apply h b (mem_def.1 bs)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ gcd s f = gcd (filter (fun x => f x ≠ 0) s) f
[PROOFSTEP]
classical
trans ((s.filter fun x ↦ f x = 0) ∪ s.filter fun x ↦ (f x ≠ 0)).gcd f
· rw [filter_union_filter_neg_eq]
rw [gcd_union]
refine' Eq.trans (_ : _ = GCDMonoid.gcd (0 : α) _) (_ : GCDMonoid.gcd (0 : α) _ = _)
· exact (gcd (filter (fun x => (f x ≠ 0)) s) f)
· refine' congr (congr rfl <| s.induction_on _ _) (by simp)
  · simp
  · intro a s _ h
    rw [filter_insert]
    split_ifs with h1 <;> simp [h, h1]
simp only [gcd_zero_left, normalize_gcd]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ gcd s f = gcd (filter (fun x => f x ≠ 0) s) f
[PROOFSTEP]
trans ((s.filter fun x ↦ f x = 0) ∪ s.filter fun x ↦ (f x ≠ 0)).gcd f
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ gcd s f = gcd (filter (fun x => f x = 0) s ∪ filter (fun x => f x ≠ 0) s) f
[PROOFSTEP]
rw [filter_union_filter_neg_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ gcd (filter (fun x => f x = 0) s ∪ filter (fun x => f x ≠ 0) s) f = gcd (filter (fun x => f x ≠ 0) s) f
[PROOFSTEP]
rw [gcd_union]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ GCDMonoid.gcd (gcd (filter (fun x => f x = 0) s) f) (gcd (filter (fun x => f x ≠ 0) s) f) =
    gcd (filter (fun x => f x ≠ 0) s) f
[PROOFSTEP]
refine' Eq.trans (_ : _ = GCDMonoid.gcd (0 : α) _) (_ : GCDMonoid.gcd (0 : α) _ = _)
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ α
[PROOFSTEP]
exact (gcd (filter (fun x => (f x ≠ 0)) s) f)
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ GCDMonoid.gcd (gcd (filter (fun x => f x = 0) s) f) (gcd (filter (fun x => f x ≠ 0) s) f) =
    GCDMonoid.gcd 0 (gcd (filter (fun x => f x ≠ 0) s) f)
[PROOFSTEP]
refine' congr (congr rfl <| s.induction_on _ _) (by simp)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ gcd (filter (fun x => f x ≠ 0) s) f = gcd (filter (fun x => f x ≠ 0) s) f
[PROOFSTEP]
simp
[GOAL]
case refine'_2.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ gcd (filter (fun x => f x = 0) ∅) f = 0
[PROOFSTEP]
simp
[GOAL]
case refine'_2.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ ∀ ⦃a : β⦄ {s : Finset β},
    ¬a ∈ s → gcd (filter (fun x => f x = 0) s) f = 0 → gcd (filter (fun x => f x = 0) (insert a s)) f = 0
[PROOFSTEP]
intro a s _ h
[GOAL]
case refine'_2.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
a : β
s : Finset β
a✝ : ¬a ∈ s
h : gcd (filter (fun x => f x = 0) s) f = 0
⊢ gcd (filter (fun x => f x = 0) (insert a s)) f = 0
[PROOFSTEP]
rw [filter_insert]
[GOAL]
case refine'_2.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
a : β
s : Finset β
a✝ : ¬a ∈ s
h : gcd (filter (fun x => f x = 0) s) f = 0
⊢ gcd (if f a = 0 then insert a (filter (fun x => f x = 0) s) else filter (fun x => f x = 0) s) f = 0
[PROOFSTEP]
split_ifs with h1
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
a : β
s : Finset β
a✝ : ¬a ∈ s
h : gcd (filter (fun x => f x = 0) s) f = 0
h1 : f a = 0
⊢ gcd (insert a (filter (fun x => f x = 0) s)) f = 0
[PROOFSTEP]
simp [h, h1]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
a : β
s : Finset β
a✝ : ¬a ∈ s
h : gcd (filter (fun x => f x = 0) s) f = 0
h1 : ¬f a = 0
⊢ gcd (filter (fun x => f x = 0) s) f = 0
[PROOFSTEP]
simp [h, h1]
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ GCDMonoid.gcd 0 (gcd (filter (fun x => f x ≠ 0) s) f) = gcd (filter (fun x => f x ≠ 0) s) f
[PROOFSTEP]
simp only [gcd_zero_left, normalize_gcd]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
⊢ (gcd s fun x => a * f x) = ↑normalize a * gcd s f
[PROOFSTEP]
classical
refine' s.induction_on _ _
· simp
· intro b t _ h
  rw [gcd_insert, gcd_insert, h, ← gcd_mul_left]
  apply ((normalize_associated a).mul_right _).gcd_eq_right
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
⊢ (gcd s fun x => a * f x) = ↑normalize a * gcd s f
[PROOFSTEP]
refine' s.induction_on _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
⊢ (gcd ∅ fun x => a * f x) = ↑normalize a * gcd ∅ f
[PROOFSTEP]
simp
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
⊢ ∀ ⦃a_1 : β⦄ {s : Finset β},
    ¬a_1 ∈ s →
      (gcd s fun x => a * f x) = ↑normalize a * gcd s f →
        (gcd (insert a_1 s) fun x => a * f x) = ↑normalize a * gcd (insert a_1 s) f
[PROOFSTEP]
intro b t _ h
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
b : β
t : Finset β
a✝ : ¬b ∈ t
h : (gcd t fun x => a * f x) = ↑normalize a * gcd t f
⊢ (gcd (insert b t) fun x => a * f x) = ↑normalize a * gcd (insert b t) f
[PROOFSTEP]
rw [gcd_insert, gcd_insert, h, ← gcd_mul_left]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
b : β
t : Finset β
a✝ : ¬b ∈ t
h : (gcd t fun x => a * f x) = ↑normalize a * gcd t f
⊢ GCDMonoid.gcd (a * f b) (↑normalize a * gcd t f) = GCDMonoid.gcd (a * f b) (a * gcd t f)
[PROOFSTEP]
apply ((normalize_associated a).mul_right _).gcd_eq_right
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
⊢ (gcd s fun x => f x * a) = gcd s f * ↑normalize a
[PROOFSTEP]
classical
refine' s.induction_on _ _
· simp
· intro b t _ h
  rw [gcd_insert, gcd_insert, h, ← gcd_mul_right]
  apply ((normalize_associated a).mul_left _).gcd_eq_right
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
⊢ (gcd s fun x => f x * a) = gcd s f * ↑normalize a
[PROOFSTEP]
refine' s.induction_on _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
⊢ (gcd ∅ fun x => f x * a) = gcd ∅ f * ↑normalize a
[PROOFSTEP]
simp
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
⊢ ∀ ⦃a_1 : β⦄ {s : Finset β},
    ¬a_1 ∈ s →
      (gcd s fun x => f x * a) = gcd s f * ↑normalize a →
        (gcd (insert a_1 s) fun x => f x * a) = gcd (insert a_1 s) f * ↑normalize a
[PROOFSTEP]
intro b t _ h
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
b : β
t : Finset β
a✝ : ¬b ∈ t
h : (gcd t fun x => f x * a) = gcd t f * ↑normalize a
⊢ (gcd (insert b t) fun x => f x * a) = gcd (insert b t) f * ↑normalize a
[PROOFSTEP]
rw [gcd_insert, gcd_insert, h, ← gcd_mul_right]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
b : β
t : Finset β
a✝ : ¬b ∈ t
h : (gcd t fun x => f x * a) = gcd t f * ↑normalize a
⊢ GCDMonoid.gcd (f b * a) (gcd t f * ↑normalize a) = GCDMonoid.gcd (f b * a) (gcd t f * a)
[PROOFSTEP]
apply ((normalize_associated a).mul_left _).gcd_eq_right
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f g : β → α
hs : ∃ x, x ∈ s ∧ f x ≠ 0
hg : ∀ (b : β), b ∈ s → f b = gcd s f * g b
⊢ gcd s f * gcd s g = gcd s f
[PROOFSTEP]
conv_lhs => rw [← normalize_gcd, ← gcd_mul_left, ← gcd_congr rfl hg]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f g : β → α
hs : ∃ x, x ∈ s ∧ f x ≠ 0
hg : ∀ (b : β), b ∈ s → f b = gcd s f * g b
| gcd s f * gcd s g
[PROOFSTEP]
rw [← normalize_gcd, ← gcd_mul_left, ← gcd_congr rfl hg]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f g : β → α
hs : ∃ x, x ∈ s ∧ f x ≠ 0
hg : ∀ (b : β), b ∈ s → f b = gcd s f * g b
| gcd s f * gcd s g
[PROOFSTEP]
rw [← normalize_gcd, ← gcd_mul_left, ← gcd_congr rfl hg]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f g : β → α
hs : ∃ x, x ∈ s ∧ f x ≠ 0
hg : ∀ (b : β), b ∈ s → f b = gcd s f * g b
| gcd s f * gcd s g
[PROOFSTEP]
rw [← normalize_gcd, ← gcd_mul_left, ← gcd_congr rfl hg]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f g : β → α
hs : ∃ x, x ∈ s ∧ f x ≠ 0
hg : ∀ (b : β), b ∈ s → f b = gcd s f * g b
⊢ ¬gcd s f = 0
[PROOFSTEP]
contrapose! hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f✝ f g : β → α
hg : ∀ (b : β), b ∈ s → f b = gcd s f * g b
hs : gcd s f = 0
⊢ ∀ (x : β), x ∈ s → f x = 0
[PROOFSTEP]
exact gcd_eq_zero_iff.1 hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
classical
by_cases h : ∀ x ∈ s, f x = (0 : α)
· refine' ⟨fun _ ↦ 1, fun b hb ↦ by rw [h b hb, gcd_eq_zero_iff.2 h, mul_one], _⟩
  rw [gcd_eq_gcd_image, image_const hs, gcd_singleton, id, normalize_one]
· choose g' hg using @gcd_dvd _ _ _ _ s f
  push_neg at h 
  refine' ⟨fun b ↦ if hb : b ∈ s then g' hb else 0, fun b hb ↦ _, extract_gcd' f _ h <| fun b hb ↦ _⟩
  simp only [hb, hg, dite_true]
  rw [dif_pos hb, hg hb]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
by_cases h : ∀ x ∈ s, f x = (0 : α)
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
refine' ⟨fun _ ↦ 1, fun b hb ↦ by rw [h b hb, gcd_eq_zero_iff.2 h, mul_one], _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
rw [h b hb, gcd_eq_zero_iff.2 h, mul_one]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
rw [gcd_eq_gcd_image, image_const hs, gcd_singleton, id, normalize_one]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
choose g' hg using @gcd_dvd _ _ _ _ s f
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
push_neg at h 
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
refine' ⟨fun b ↦ if hb : b ∈ s then g' hb else 0, fun b hb ↦ _, extract_gcd' f _ h <| fun b hb ↦ _⟩
[GOAL]
case neg.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
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_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
simp only [hb, hg, dite_true]
[GOAL]
case neg.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
rw [dif_pos hb, hg hb]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f g : β → α
a : α
h : ∀ (x : β), x ∈ s → a ∣ f x - g x
⊢ GCDMonoid.gcd a (gcd s f) = GCDMonoid.gcd a (gcd s g)
[PROOFSTEP]
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 _ _)))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f g : β → α
a : α
h : ∀ (x : β), x ∈ s → a ∣ f x - g x
⊢ GCDMonoid.gcd a (gcd s f) = GCDMonoid.gcd a (gcd s g)
[PROOFSTEP]
revert h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f g : β → α
a : α
⊢ (∀ (x : β), x ∈ s → a ∣ f x - g x) → GCDMonoid.gcd a (gcd s f) = GCDMonoid.gcd a (gcd s g)
[PROOFSTEP]
refine' s.induction_on _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f g : β → α
a : α
⊢ (∀ (x : β), x ∈ ∅ → a ∣ f x - g x) → GCDMonoid.gcd a (gcd ∅ f) = GCDMonoid.gcd a (gcd ∅ g)
[PROOFSTEP]
simp
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f g : β → α
a : α
⊢ ∀ ⦃a_1 : β⦄ {s : Finset β},
    ¬a_1 ∈ s →
      ((∀ (x : β), x ∈ s → a ∣ f x - g x) → GCDMonoid.gcd a (gcd s f) = GCDMonoid.gcd a (gcd s g)) →
        (∀ (x : β), x ∈ insert a_1 s → a ∣ f x - g x) →
          GCDMonoid.gcd a (gcd (insert a_1 s) f) = GCDMonoid.gcd a (gcd (insert a_1 s) g)
[PROOFSTEP]
intro b s _ hi h
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : NormalizedGCDMonoid α
s✝ : Finset β
f g : β → α
a : α
b : β
s : Finset β
a✝ : ¬b ∈ s
hi : (∀ (x : β), x ∈ s → a ∣ f x - g x) → GCDMonoid.gcd a (gcd s f) = GCDMonoid.gcd a (gcd s g)
h : ∀ (x : β), x ∈ insert b s → a ∣ f x - g x
⊢ GCDMonoid.gcd a (gcd (insert b s) f) = GCDMonoid.gcd a (gcd (insert b s) g)
[PROOFSTEP]
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]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : NormalizedGCDMonoid α
s✝ : Finset β
f g : β → α
a : α
b : β
s : Finset β
a✝ : ¬b ∈ s
hi : (∀ (x : β), x ∈ s → a ∣ f x - g x) → GCDMonoid.gcd a (gcd s f) = GCDMonoid.gcd a (gcd s g)
h : ∀ (x : β), x ∈ insert b s → a ∣ f x - g x
⊢ GCDMonoid.gcd (gcd s g) (GCDMonoid.gcd a (f b)) = GCDMonoid.gcd (gcd s g) (GCDMonoid.gcd a (g b))
[PROOFSTEP]
exact congr_arg _ (gcd_eq_of_dvd_sub_right (h _ (mem_insert_self _ _)))
