Theorem: RingHom.list_map_sum (FormalSnarksProject/ToMathlib/PolynomialQuotient.lean)

State before:
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
Tactic:
induction s with
| nil =>
  simp
| cons x xs ih =>
  simp [ih]
State after:
no goals

State before:
case nil
A : Type v
B : Type w
inst✝¹ : Semiring A
inst✝ : Semiring B
φ : A →+* 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
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
Tactic:
simp [ih]
State after:
no goals