no goals
α : Type u_2
β : Type u_1
γ : Type ?u.6054
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
⊢ lcm (∅ ∪ s₂) f = GCDMonoid.lcm (lcm ∅ f) (lcm s₂ f)
rw [empty_union, lcm_empty, lcm_one_left, normalize_lcm]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.6054
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
a : β
s : Finset β
x✝ : ¬a ∈ s
ih : lcm (s ∪ s₂) f = GCDMonoid.lcm (lcm s f) (lcm s₂ f)
⊢ lcm (insert a s ∪ s₂) f = GCDMonoid.lcm (lcm (insert a s) f) (lcm s₂ f)
rw [insert_union, lcm_insert, lcm_insert, ih, lcm_assoc]