case refine'_1
α : Type u_1
β : Type u_2
γ : Type ?u.37723
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
⊢ (gcd ∅ fun x => f x * a) = gcd ∅ f * ↑normalize a

case refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.37723
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
α : Type u_1
β : Type u_2
γ : Type ?u.37723
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
⊢ (gcd s fun x => f x * a) = gcd s f * ↑normalize a
refine' s.induction_on _ _
no goals
case refine'_1
α : Type u_1
β : Type u_2
γ : Type ?u.37723
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
⊢ (gcd ∅ fun x => f x * a) = gcd ∅ f * ↑normalize a
simp
case refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.37723
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
case refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.37723
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
intro b t _ h
case refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.37723
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)
case refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.37723
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
rw [gcd_insert, gcd_insert, h, ← gcd_mul_right]
no goals
case refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.37723
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)
apply ((normalize_associated a).mul_left _).gcd_eq_right