no goals
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s : Multiset α
⊢ gcd (dedup 0) = gcd 0
simp
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : gcd (dedup s) = gcd s
h : a ∈ s
⊢ gcd s = GCDMonoid.gcd a (gcd s)
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : gcd (dedup s) = gcd s
⊢ gcd (dedup (a ::ₘ s)) = gcd (a ::ₘ s)
by_cases h : a ∈ s <;> simp [IH, h]
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : gcd (dedup s) = gcd s
h : a ∈ s
⊢ fold GCDMonoid.gcd 0 s = GCDMonoid.gcd a (fold GCDMonoid.gcd 0 s)
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : gcd (dedup s) = gcd s
h : a ∈ s
⊢ gcd s = GCDMonoid.gcd a (gcd s)
unfold gcd
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : gcd (dedup s) = gcd s
h : a ∈ s
⊢ GCDMonoid.gcd a (fold GCDMonoid.gcd 0 (erase s a)) = GCDMonoid.gcd (↑normalize a) (fold GCDMonoid.gcd 0 (erase s a))
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : gcd (dedup s) = gcd s
h : a ∈ s
⊢ fold GCDMonoid.gcd 0 s = GCDMonoid.gcd a (fold GCDMonoid.gcd 0 s)
rw [← cons_erase h, fold_cons_left, ← gcd_assoc, gcd_same]
no goals
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : gcd (dedup s) = gcd s
h : a ∈ s
⊢ GCDMonoid.gcd a (fold GCDMonoid.gcd 0 (erase s a)) = GCDMonoid.gcd (↑normalize a) (fold GCDMonoid.gcd 0 (erase s a))
apply (associated_normalize _).gcd_eq_left