funext x dx
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_4
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type u_3
inst✝⁵ : Vec K Z
W : Type ?u.41063
inst✝⁴ : Vec K W
ι : Type ?u.41074
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.41101
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Z
hf : Diffeomorphism K f
hg : CDifferentiable K g
⊢ (cderiv K fun x => invFun f (g x)) = fun x dx =>
    let z := g x;
    let dz := cderiv K g x dx;
    let y := invFun f z;
    let dy := invFun (cderiv K f y) dz;
    dy
case h.h
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_4
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type u_3
inst✝⁵ : Vec K Z
W : Type ?u.41063
inst✝⁴ : Vec K W
ι : Type ?u.41074
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.41101
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Z
hf : Diffeomorphism K f
hg : CDifferentiable K g
x dx : X
⊢ cderiv K (fun x => invFun f (g x)) x dx =
    let z := g x;
    let dz := cderiv K g x dx;
    let y := invFun f z;
    let dy := invFun (cderiv K f y) dz;
    dy