fun_trans
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.43254
inst✝⁴ : Vec K W
ι : Type ?u.43265
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.43292
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → 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) = 0
⊢ cderiv K (fun x => invFun (f x)) x dx - cderiv K (fun x => invFun (f x) ∘ f x) x dx ∘ invFun (f x) = fun z =>
    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.43254
inst✝⁴ : Vec K W
ι : Type ?u.43265
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.43292
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → 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) = 0
⊢ cderiv K (fun x => invFun (f x)) x dx - cderiv K (fun x => invFun (f x) ∘ f x) x dx ∘ invFun (f x) = fun z =>
    -invFun (cderiv K (f x) (invFun (f x) (f x (invFun (f x) z)))) (cderiv K (fun x' => f x' (invFun (f x) z)) x dx)