no goals
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b✝ : β
f✝ g : α → β
inst✝ : DivisionSemiring β
s : Finset α
f : α → β
b : β
⊢ (∑ x in s, f x) / b = ∑ x in s, f x / b
simp only [div_eq_mul_inv, sum_mul]