α : Type u_2
β : Type u_1
γ : Type ?u.46050
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)
α : Type u_2
β : Type u_1
γ : Type ?u.46050
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)
revert h
case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.46050
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)

case refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.46050
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)
α : Type u_2
β : Type u_1
γ : Type ?u.46050
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)
refine' s.induction_on _ _
case refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.46050
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)
case refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.46050
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)
intro b s _ hi h
case refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.46050
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))
case refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.46050
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)
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]
no goals
case refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.46050
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))
exact congr_arg _ (gcd_eq_of_dvd_sub_right (h _ (mem_insert_self _ _)))
no goals
case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.46050
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)
simp