no goals
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s : Multiset α
⊢ lcm (dedup 0) = lcm 0
simp
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : lcm (dedup s) = lcm s
h : a ∈ s
⊢ lcm s = GCDMonoid.lcm a (lcm s)
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : lcm (dedup s) = lcm s
⊢ lcm (dedup (a ::ₘ s)) = lcm (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 : lcm (dedup s) = lcm s
h : a ∈ s
⊢ fold GCDMonoid.lcm 1 s = GCDMonoid.lcm a (fold GCDMonoid.lcm 1 s)
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : lcm (dedup s) = lcm s
h : a ∈ s
⊢ lcm s = GCDMonoid.lcm a (lcm s)
unfold lcm
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : lcm (dedup s) = lcm s
h : a ∈ s
⊢ GCDMonoid.lcm a (fold GCDMonoid.lcm 1 (erase s a)) = GCDMonoid.lcm (↑normalize a) (fold GCDMonoid.lcm 1 (erase s a))
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : lcm (dedup s) = lcm s
h : a ∈ s
⊢ fold GCDMonoid.lcm 1 s = GCDMonoid.lcm a (fold GCDMonoid.lcm 1 s)
rw [← cons_erase h, fold_cons_left, ← lcm_assoc, lcm_same]
no goals
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : lcm (dedup s) = lcm s
h : a ∈ s
⊢ GCDMonoid.lcm a (fold GCDMonoid.lcm 1 (erase s a)) = GCDMonoid.lcm (↑normalize a) (fold GCDMonoid.lcm 1 (erase s a))
apply lcm_eq_of_associated_left (associated_normalize _)