Theorem: SciLean.IsSmoothLinearMap.SciLean.BasisDuality.fromDual.arg_x.IsSmoothLinearMap_rule (SciLean/Core/FunctionPropositions/IsSmoothLinearMap.lean)

State before:
K✝¹ : Type ?u.33189
inst✝²⁸ : RCLike K✝¹
X✝¹ : Type ?u.33195
inst✝²⁷ : Vec K✝¹ X✝¹
Y✝¹ : Type ?u.33208
inst✝²⁶ : Vec K✝¹ Y✝¹
Z✝¹ : Type ?u.33219
inst✝²⁵ : Vec K✝¹ Z✝¹
ι✝ : Type ?u.33230
inst✝²⁴ : IndexType ι✝
inst✝²³ : LawfulIndexType ι✝
inst✝²² : DecidableEq ι✝
E✝ : ι✝ → Type ?u.33257
inst✝²¹ : (i : ι✝) → Vec K✝¹ (E✝ i)
K✝ : Type ?u.33273
inst✝²⁰ : RCLike K✝
X✝ : Type ?u.33279
inst✝¹⁹ : Vec K✝ X✝
Y✝ : Type ?u.33292
inst✝¹⁸ : Vec K✝ Y✝
Z✝ : Type ?u.33303
inst✝¹⁷ : Vec K✝ Z✝
ι : Type ?u.33314
inst✝¹⁶ : IndexType ι
inst✝¹⁵ : LawfulIndexType ι
inst✝¹⁴ : DecidableEq ι
E : ι → Type ?u.33341
inst✝¹³ : (i : ι) → Vec K✝ (E i)
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.33458
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type ?u.33461
inst✝⁴ : FinVec IY K Y
IZ : Type ?u.33551
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.33554
inst✝ : FinVec IZ K Z
⊢ IsSmoothLinearMap K fun x => BasisDuality.fromDual x
Tactic:
constructor <;> fun_prop
State after:
no goals