Theorem: IsLinearMap.sum_pull (SciLean/Core/Meta/GenerateLinearMapSimp.lean)

State before:
K : Type u'
inst✝⁸ : CommSemiring K
X : Type u
inst✝⁷ : AddCommGroup X
inst✝⁶ : Module K X
Y : Type v
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module K Y
Z : Type w
inst✝³ : AddCommGroup Z
inst✝² : Module K Z
f✝ : X → Y
hf✝ : IsLinearMap K f✝
f : X → Y
hf : IsLinearMap K f
ι : Type
inst✝¹ : IndexType ι
inst✝ : IndexType ι
x : ι → X
⊢ f ( ∑ i, x i) = ∑ i, f (x i)
Tactic:
sorry_proof
State after:
no goals