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

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

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