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

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