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