α : Type u_1
β : Type u_2
γ : Type ?u.1482
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
⊢ (∀ (b : α), b ∈ Multiset.map f s.val → b ∣ a) ↔ ∀ (b : β), b ∈ s → f b ∣ a
α : Type u_1
β : Type u_2
γ : Type ?u.1482
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
⊢ lcm s f ∣ a ↔ ∀ (b : β), b ∈ s → f b ∣ a
apply Iff.trans Multiset.lcm_dvd
α : Type u_1
β : Type u_2
γ : Type ?u.1482
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
⊢ (∀ (b : α) (x : β), x ∈ s.val → f x = b → b ∣ a) ↔ ∀ (b : β), b ∈ s → f b ∣ a
α : Type u_1
β : Type u_2
γ : Type ?u.1482
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
⊢ (∀ (b : α), b ∈ Multiset.map f s.val → b ∣ a) ↔ ∀ (b : β), b ∈ s → f b ∣ a
simp only [Multiset.mem_map, and_imp, exists_imp]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.1482
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
a : α
⊢ (∀ (b : α) (x : β), x ∈ s.val → f x = b → b ∣ a) ↔ ∀ (b : β), b ∈ s → f b ∣ a
exact ⟨fun k b hb ↦ k _ _ hb rfl, fun k a' b hb h ↦ h ▸ k _ hb⟩