Theorem: SciLean.fderiv.apply_rule (SciLean/Core/FunctionTransformations/FDeriv.lean)

State before:
K : Type u_3
inst✝⁹ : RCLike K
X : Type ?u.25663
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type ?u.25805
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type ?u.25940
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type u_1
inst✝² : Fintype ι
E : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace K (E i)
i : ι
⊢ (fderiv K fun x => x i) = fun x => fun dx =>L[K] dx i
Tactic:
funext x
State after:
case h
K : Type u_3
inst✝⁹ : RCLike K
X : Type ?u.25663
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type ?u.25805
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type ?u.25940
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type u_1
inst✝² : Fintype ι
E : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace K (E i)
i : ι
x : (i : ι) → E i
⊢ fderiv K (fun x => x i) x = fun dx =>L[K] dx i

State before:
case h
K : Type u_3
inst✝⁹ : RCLike K
X : Type ?u.25663
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type ?u.25805
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type ?u.25940
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type u_1
inst✝² : Fintype ι
E : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace K (E i)
i : ι
x : (i : ι) → E i
⊢ fderiv K (fun x => x i) x = fun dx =>L[K] dx i
Tactic:
sorry_proof
State after:
no goals