rw[← sub_zero (cderiv K (fun x => Function.invFun (f x) z) x dx)]
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.58775
inst✝⁴ : Vec K W
ι : Type ?u.58786
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.58813
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
z : Z
hf : ∀ (x : X), Diffeomorphism K (f x)
hf' : CDifferentiable K fun xy => f xy.1 xy.2
x dx : X
H : (cderiv K (fun x => invFun (f x) ∘ f x) x dx ∘ invFun (f x)) z = 0
⊢ cderiv K (fun x => invFun (f x) z) x dx =
    let y := invFun (f x) z;
    let dfdx_y := cderiv K f x dx y;
    let df'dy := cderiv K (invFun (f x)) (f x y) dfdx_y;
    -df'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.58775
inst✝⁴ : Vec K W
ι : Type ?u.58786
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.58813
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
z : Z
hf : ∀ (x : X), Diffeomorphism K (f x)
hf' : CDifferentiable K fun xy => f xy.1 xy.2
x dx : X
H : (cderiv K (fun x => invFun (f x) ∘ f x) x dx ∘ invFun (f x)) z = 0
⊢ cderiv K (fun x => invFun (f x) z) x dx - 0 =
    let y := invFun (f x) z;
    let dfdx_y := cderiv K f x dx y;
    let df'dy := cderiv K (invFun (f x)) (f x y) dfdx_y;
    -df'dy