-- Mathlib/Algebra/GCDMonoid/Finset.lean
theorem gcd_eq_of_dvd_sub {s : Finset β} {f g : β → α} {a : α}
    (h : ∀ x : β, x ∈ s → a ∣ f x - g x) :
    GCDMonoid.gcd a (s.gcd f) = GCDMonoid.gcd a (s.gcd g)

Proof state:
case refine_1
α : Type u_2
β : Type u_3
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f g : β → α
a : α
⊢ (∀ x ∈ ∅, a ∣ f x - g x) → GCDMonoid.gcd a (∅.gcd f) = GCDMonoid.gcd a (∅.gcd g)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f g : β → α
a : α
h : ∀ x ∈ s, a ∣ f x - g x
⊢ GCDMonoid.gcd a (s.gcd f) = GCDMonoid.gcd a (s.gcd g)

Tactic:
revert h

Result:
α : Type u_2
β : Type u_3
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f g : β → α
a : α
⊢ (∀ x ∈ s, a ∣ f x - g x) → GCDMonoid.gcd a (s.gcd f) = GCDMonoid.gcd a (s.gcd g)

Proof state:
α : Type u_2
β : Type u_3
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f g : β → α
a : α
⊢ (∀ x ∈ s, a ∣ f x - g x) → GCDMonoid.gcd a (s.gcd f) = GCDMonoid.gcd a (s.gcd g)

Tactic:
refine s.induction_on ?_ ?_

Result:
case refine_1
α : Type u_2
β : Type u_3
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f g : β → α
a : α
⊢ (∀ x ∈ ∅, a ∣ f x - g x) → GCDMonoid.gcd a (∅.gcd f) = GCDMonoid.gcd a (∅.gcd g)

case refine_2
α : 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 ∈ s, a ∣ f x - g x) → GCDMonoid.gcd a (s.gcd f) = GCDMonoid.gcd a (s.gcd g)) →
        (∀ x ∈ insert a_1 s, a ∣ f x - g x) →
          GCDMonoid.gcd a ((insert a_1 s).gcd f) = GCDMonoid.gcd a ((insert a_1 s).gcd g)

Proof state:
case refine_2
α : 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 ∈ s, a ∣ f x - g x) → GCDMonoid.gcd a (s.gcd f) = GCDMonoid.gcd a (s.gcd g)) →
        (∀ x ∈ insert a_1 s, a ∣ f x - g x) →
          GCDMonoid.gcd a ((insert a_1 s).gcd f) = GCDMonoid.gcd a ((insert a_1 s).gcd g)

Tactic:
intro b s _ hi h

Result:
case refine_2
α : 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 ∈ s, a ∣ f x - g x) → GCDMonoid.gcd a (s.gcd f) = GCDMonoid.gcd a (s.gcd g)
h : ∀ x ∈ insert b s, a ∣ f x - g x
⊢ GCDMonoid.gcd a ((insert b s).gcd f) = GCDMonoid.gcd a ((insert b s).gcd g)

Proof state:
case refine_2
α : 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 ∈ s, a ∣ f x - g x) → GCDMonoid.gcd a (s.gcd f) = GCDMonoid.gcd a (s.gcd g)
h : ∀ x ∈ insert b s, a ∣ f x - g x
⊢ GCDMonoid.gcd a ((insert b s).gcd f) = GCDMonoid.gcd a ((insert b s).gcd g)

Tactic:
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]

Result:
case refine_2
α : 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 ∈ s, a ∣ f x - g x) → GCDMonoid.gcd a (s.gcd f) = GCDMonoid.gcd a (s.gcd g)
h : ∀ x ∈ insert b s, a ∣ f x - g x
⊢ GCDMonoid.gcd (s.gcd g) (GCDMonoid.gcd a (f b)) = GCDMonoid.gcd (s.gcd g) (GCDMonoid.gcd a (g b))

Proof state:
case refine_2
α : 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 ∈ s, a ∣ f x - g x) → GCDMonoid.gcd a (s.gcd f) = GCDMonoid.gcd a (s.gcd g)
h : ∀ x ∈ insert b s, a ∣ f x - g x
⊢ GCDMonoid.gcd (s.gcd g) (GCDMonoid.gcd a (f b)) = GCDMonoid.gcd (s.gcd g) (GCDMonoid.gcd a (g b))

Tactic:
exact congr_arg _ (gcd_eq_of_dvd_sub_right (h _ (mem_insert_self _ _)))

Result:
no goals