Theorem: AlgEquiv.list_map_sum (FormalSnarksProject/ToMathlib/OptionEquivRight.lean)

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

State before:
case nil
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₁
⊢ e (List.map (fun x => f x) []).sum = (List.map (fun x => e (f x)) []).sum
Tactic:
simp
State after:
no goals

State before:
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
Tactic:
simp [ih]
State after:
no goals