case refine'_1
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a : α
s : Multiset α
⊢ gcd (map ((fun x x_1 => x * x_1) a) 0) = ↑normalize a * gcd 0

case refine'_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a : α
s✝ : Multiset α
b : α
s : Multiset α
ih : gcd (map ((fun x x_1 => x * x_1) a) s) = ↑normalize a * gcd s
⊢ gcd (map ((fun x x_1 => x * x_1) a) (b ::ₘ s)) = ↑normalize a * gcd (b ::ₘ s)
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a : α
s : Multiset α
⊢ gcd (map ((fun x x_1 => x * x_1) a) s) = ↑normalize a * gcd s
refine' s.induction_on _ fun b s ih ↦ _
no goals
case refine'_1
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a : α
s : Multiset α
⊢ gcd (map ((fun x x_1 => x * x_1) a) 0) = ↑normalize a * gcd 0
simp_rw [map_zero, gcd_zero, mul_zero]
case refine'_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a : α
s✝ : Multiset α
b : α
s : Multiset α
ih : gcd (map ((fun x x_1 => x * x_1) a) s) = ↑normalize a * gcd s
⊢ GCDMonoid.gcd (a * b) (gcd (map (fun x => a * x) s)) = GCDMonoid.gcd (a * b) (a * gcd s)
case refine'_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a : α
s✝ : Multiset α
b : α
s : Multiset α
ih : gcd (map ((fun x x_1 => x * x_1) a) s) = ↑normalize a * gcd s
⊢ gcd (map ((fun x x_1 => x * x_1) a) (b ::ₘ s)) = ↑normalize a * gcd (b ::ₘ s)
simp_rw [map_cons, gcd_cons, ← gcd_mul_left]
case refine'_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a : α
s✝ : Multiset α
b : α
s : Multiset α
ih : gcd (map ((fun x x_1 => x * x_1) a) s) = ↑normalize a * gcd s
⊢ GCDMonoid.gcd (a * b) (↑normalize a * gcd s) = GCDMonoid.gcd (a * b) (a * gcd s)
case refine'_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a : α
s✝ : Multiset α
b : α
s : Multiset α
ih : gcd (map ((fun x x_1 => x * x_1) a) s) = ↑normalize a * gcd s
⊢ GCDMonoid.gcd (a * b) (gcd (map (fun x => a * x) s)) = GCDMonoid.gcd (a * b) (a * gcd s)
rw [ih]
no goals
case refine'_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a : α
s✝ : Multiset α
b : α
s : Multiset α
ih : gcd (map ((fun x x_1 => x * x_1) a) s) = ↑normalize a * gcd s
⊢ GCDMonoid.gcd (a * b) (↑normalize a * gcd s) = GCDMonoid.gcd (a * b) (a * gcd s)
apply ((normalize_associated a).mul_right _).gcd_eq_right