fun_trans
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
⊢ cderiv K (fun x' => invFun (f x) z) x dx = 0
no goals