Theorem: SciLean.Basis.proj.arg_x.IsAffineMap_rule (SciLean/Core/FunctionPropositions/IsAffineMap.lean)

State before:
R : Type ?u.118169
X✝ : Type ?u.118172
Y✝ : Type ?u.118175
Z✝ : Type ?u.118178
ι : Type ?u.118181
E : ι → Type ?u.118186
inst✝²⁴ : CommRing R
inst✝²³ : AddCommGroup X✝
inst✝²² : Module R X✝
inst✝²¹ : AddCommGroup Y✝
inst✝²⁰ : Module R Y✝
inst✝¹⁹ : AddCommGroup Z✝
inst✝¹⁸ : Module R Z✝
inst✝¹⁷ : IndexType ι
inst✝¹⁶ : LawfulIndexType ι
inst✝¹⁵ : DecidableEq ι
inst✝¹⁴ : (i : ι) → AddCommGroup (E i)
inst✝¹³ : (i : ι) → Module R (E i)
K : Type u_1
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_2
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type ?u.121438
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.121525
inst✝ : FinVec IZ K Z
i : IX
⊢ IsAffineMap K fun x => ℼ i x
Tactic:
sorry_proof
State after:
no goals