simp [ih]
case cons
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A₁
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
ι : Type u_1
f : ι → A₁
hd : ι
tl : List ι
ih : e (List.map (fun x => f x) tl).sum = (List.map (fun x => e (f x)) tl).sum
⊢ e (List.map (fun x => f x) (hd :: tl)).sum = (List.map (fun x => e (f x)) (hd :: tl)).sum
no goals