no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
a : α
⊢ lcm 0 ∣ a ↔ ∀ (b : α), b ∈ 0 → b ∣ a
simp
no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
a : α
⊢ ∀ ⦃a_1 : α⦄ {s : Multiset α},
    (lcm s ∣ a ↔ ∀ (b : α), b ∈ s → b ∣ a) → (lcm (a_1 ::ₘ s) ∣ a ↔ ∀ (b : α), b ∈ a_1 ::ₘ s → b ∣ a)
simp (config := { contextual := true }) [or_imp, forall_and, lcm_dvd_iff]