induction s with
| nil =>
  simp
| cons x xs ih =>
  simp [ih]
A : Type v
B : Type w
inst✝¹ : Semiring A
inst✝ : Semiring B
φ : A →+* B
ι : Type u_1
f : ι → A
s : List ι
⊢ φ (List.map (fun x => f x) s).sum = (List.map (fun x => φ (f x)) s).sum
no goals