Theorem: SciLean.Basis.proj.arg_x.IsLinearMap_rule (SciLean/Core/FunctionPropositions/IsLinearMap.lean)

State before:
K : Type u_1
inst✝¹² : RCLike K
IX : Type u_3
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_2
inst✝⁸ : FinVec IX K X
IY : Type ?u.229117
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type ?u.229120
inst✝⁴ : FinVec IY K Y
IZ : Type ?u.229206
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.229209
inst✝ : FinVec IZ K Z
i : IX
⊢ IsLinearMap K fun x => ℼ i x
Tactic:
sorry_proof
State after:
no goals