have hg' : CDifferentiable K g' := by rw[show g' = (fun x => (x,g x)) by rfl]; fun_prop
ι : Sort ?u.19371
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : FwdDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : Vec K X
Y : Type
inst✝² : Vec K Y
Z : Type
inst✝¹ : Vec K Z
E : ι → Type
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → m Z
g : X → Y
hf : CDifferentiableM K fun xy => f xy.1 xy.2
hg : CDifferentiable K g
f' : X × Y → m Z := fun xy => f xy.1 xy.2
g' : X → X × Y := fun x => (x, g x)
⊢ (fwdDerivM K fun x =>
      let y := g x;
      f x y) =
    fun x dx =>
    let ydy := fwdDeriv K g x dx;
    fwdDerivM K (fun xy => f xy.1 xy.2) (x, ydy.1) (dx, ydy.2)
ι : Sort ?u.19371
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : FwdDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : Vec K X
Y : Type
inst✝² : Vec K Y
Z : Type
inst✝¹ : Vec K Z
E : ι → Type
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → m Z
g : X → Y
hf : CDifferentiableM K fun xy => f xy.1 xy.2
hg : CDifferentiable K g
f' : X × Y → m Z := fun xy => f xy.1 xy.2
g' : X → X × Y := fun x => (x, g x)
hg' : CDifferentiable K g'
⊢ (fwdDerivM K fun x =>
      let y := g x;
      f x y) =
    fun x dx =>
    let ydy := fwdDeriv K g x dx;
    fwdDerivM K (fun xy => f xy.1 xy.2) (x, ydy.1) (dx, ydy.2)