no goals
ι : Type ?u.169674
α : Type ?u.169677
β : Type ?u.169680
γ : Type ?u.169683
s : Multiset ℕ
n : ℕ
⊢ sum s % n = sum (map (fun x => x % n) s) % n
induction s using Multiset.induction <;> simp [Nat.add_mod, *]