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

State before:
R : Type u_1
X : Type u_2
Y : Type ?u.18207
Z : Type ?u.18210
ι : Type u_4
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)
f : X → (i : ι) → E i
hf : ∀ (i : ι), IsLinearMap R fun x => f x i
⊢ IsLinearMap R fun x i => f x i
Tactic:
sorry_proof
State after:
no goals