no goals
ι : Type ?u.171528
α : Type ?u.171531
β : Type ?u.171534
γ : Type ?u.171537
s : Multiset ℤ
n : ℤ
⊢ sum s % n = sum (map (fun x => x % n) s) % n
induction s using Multiset.induction <;> simp [Int.add_emod, *]