Theorem: IndexType.sum_linearize (SciLean/Data/IndexType.lean)

State before:
ι : Type v
inst✝⁴ : IndexType ι
I : Type u_1
X : Type u_2
inst✝³ : Add X
inst✝² : Zero X
inst✝¹ : IndexType I
inst✝ : LawfulIndexType I
f : I → X
⊢  ∑ i, f i = ∑ i, f (fromFin i)
Tactic:
simp only [sum]
State after:
ι : Type v
inst✝⁴ : IndexType ι
I : Type u_1
X : Type u_2
inst✝³ : Add X
inst✝² : Zero X
inst✝¹ : IndexType I
inst✝ : LawfulIndexType I
f : I → X
⊢ fold (IndexType.univ I) (fun s i => s + f i) 0 = fold (IndexType.univ (Fin (card I))) (fun s i => s + f (fromFin i)) 0

State before:
ι : Type v
inst✝⁴ : IndexType ι
I : Type u_1
X : Type u_2
inst✝³ : Add X
inst✝² : Zero X
inst✝¹ : IndexType I
inst✝ : LawfulIndexType I
f : I → X
⊢ fold (IndexType.univ I) (fun s i => s + f i) 0 = fold (IndexType.univ (Fin (card I))) (fun s i => s + f (fromFin i)) 0
Tactic:
rw[fold_linearize]
State after:
no goals