no goals
ι : Type ?u.786416
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
f : α → β
a : α
s : Finset α
ha : a ∈ s
⊢ f a ∣ ∏ i in s, f i
classical
  rw [Finset.prod_eq_mul_prod_diff_singleton ha]
  exact dvd_mul_right _ _
ι : Type ?u.786416
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
f : α → β
a : α
s : Finset α
ha : a ∈ s
⊢ f a ∣ f a * ∏ x in s \ {a}, f x
ι : Type ?u.786416
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
f : α → β
a : α
s : Finset α
ha : a ∈ s
⊢ f a ∣ ∏ i in s, f i
rw [Finset.prod_eq_mul_prod_diff_singleton ha]
no goals
ι : Type ?u.786416
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
f : α → β
a : α
s : Finset α
ha : a ∈ s
⊢ f a ∣ f a * ∏ x in s \ {a}, f x
exact dvd_mul_right _ _