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