induction l with
| nil => simp
| cons hd tl ih => simp [ih]
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₁
l : List ι
⊢ e (List.map (fun x => f x) l).sum = (List.map (fun x => e (f x)) l).sum
no goals