Theorem: MvPolynomial.sum_map_C (FormalSnarksProject/ToMathlib/OptionEquivRight.lean)

State before:
σ A R : Type
inst✝ : CommSemiring R
l : List A
f : A → R
⊢ (List.map (fun x => C (f x)) l).sum = C (List.map f l).sum
Tactic:
induction l with
| nil => simp
| cons hd tl ih => simp [ih]
State after:
no goals

State before:
case nil
σ A R : Type
inst✝ : CommSemiring R
f : A → R
⊢ (List.map (fun x => C (f x)) []).sum = C (List.map f []).sum
Tactic:
simp
State after:
no goals

State before:
case cons
σ A R : Type
inst✝ : CommSemiring R
f : A → R
hd : A
tl : List A
ih : (List.map (fun x => C (f x)) tl).sum = C (List.map f tl).sum
⊢ (List.map (fun x => C (f x)) (hd :: tl)).sum = C (List.map f (hd :: tl)).sum
Tactic:
simp [ih]
State after:
no goals