Theorem: SciLean.BasisDuality.fromDual.arg_x.ContCDiffAt_rule (SciLean/Core/FunctionPropositions/ContCDiff.lean)

State before:
K✝¹ : Type ?u.47454
inst✝²⁴ : RCLike K✝¹
n : ℕ∞
X✝¹ : Type ?u.47462
inst✝²³ : Vec K✝¹ X✝¹
Y✝¹ : Type ?u.47475
inst✝²² : Vec K✝¹ Y✝¹
Z✝¹ : Type ?u.47486
inst✝²¹ : Vec K✝¹ Z✝¹
ι✝ : Type ?u.47497
inst✝²⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.47506
inst✝¹⁹ : (i : ι✝) → Vec K✝¹ (E✝ i)
K✝ : Type ?u.47522
inst✝¹⁸ : RCLike K✝
X✝ : Type ?u.47528
inst✝¹⁷ : Vec K✝ X✝
Y✝ : Type ?u.47541
inst✝¹⁶ : Vec K✝ Y✝
Z✝ : Type ?u.47552
inst✝¹⁵ : Vec K✝ Z✝
ι : Type ?u.47563
inst✝¹⁴ : IndexType ι
E : ι → Type ?u.47572
inst✝¹³ : (i : ι) → Vec K✝ (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.47686
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.47771
inst✝ : FinVec IZ K Z
x : X
⊢ ContCDiffAt K n (fun x => fromDual x) x
Tactic:
sorry_proof
State after:
no goals