Theorem: AlgHom.list_map_sum (FormalSnarksProject/ToMathlib/ForTransformations.lean)

State before:
F : Type
inst✝⁵ : Field F
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
φ : A →ₐ[R] B
ι : Type u_1
f : ι → A
s : List ι
⊢ φ (List.map (fun x => f x) s).sum = (List.map (fun x => φ (f x)) s).sum
Tactic:
induction s with
| nil =>
  simp
| cons x xs ih =>
  simp only [List.map_cons, List.sum_cons, map_add, ih]
State after:
no goals

State before:
case nil
F : Type
inst✝⁵ : Field F
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
φ : A →ₐ[R] B
ι : Type u_1
f : ι → A
⊢ φ (List.map (fun x => f x) []).sum = (List.map (fun x => φ (f x)) []).sum
Tactic:
simp
State after:
no goals

State before:
case cons
F : Type
inst✝⁵ : Field F
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
φ : A →ₐ[R] 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
Tactic:
simp only [List.map_cons, List.sum_cons, map_add, ih]
State after:
no goals