Theorem: IsLinearMap.isLinearMap_apply (SciLean/Core/FunctionPropositions/IsLinearMap.lean)

State before:
R : Type u_1
X : Type ?u.16164
Y : Type ?u.16167
Z : Type ?u.16170
ι : Type u_2
E : ι → Type u_3
inst✝⁸ : Semiring R
inst✝⁷ : AddCommGroup X
inst✝⁶ : Module R X
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module R Y
inst✝³ : AddCommGroup Z
inst✝² : Module R Z
inst✝¹ : (i : ι) → AddCommMonoid (E i)
inst✝ : (i : ι) → Module R (E i)
i : ι
⊢ IsLinearMap R fun f => f i
Tactic:
sorry_proof
State after:
no goals