case intro.intro
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b✝ : β
f✝ g : α → β
inst✝ : CommSemiring β
b : β
s : Finset α
f : α → β
h : ∀ (x : α), x ∈ s → b ∣ f x
x : α
hx : x ∈ s.val
hy : f x ∈ Multiset.map (fun x => f x) s.val
⊢ b ∣ f x
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b✝ : β
f✝ g : α → β
inst✝ : CommSemiring β
b : β
s : Finset α
f : α → β
h : ∀ (x : α), x ∈ s → b ∣ f x
y : β
hy : y ∈ Multiset.map (fun x => f x) s.val
⊢ b ∣ y
rcases Multiset.mem_map.1 hy with ⟨x, hx, rfl⟩
no goals
case intro.intro
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b✝ : β
f✝ g : α → β
inst✝ : CommSemiring β
b : β
s : Finset α
f : α → β
h : ∀ (x : α), x ∈ s → b ∣ f x
x : α
hx : x ∈ s.val
hy : f x ∈ Multiset.map (fun x => f x) s.val
⊢ b ∣ f x
exact h x hx