Theorem: SciLean.jacobian.comp_rule (SciLean/Core/Integral/Jacobian.lean)

State before:
R : Type u_1
inst✝³ : RealScalar R
U : Type u_2
inst✝² : SemiHilbert R U
V : Type u_3
inst✝¹ : SemiHilbert R V
W : Type ?u.33364
inst✝ : SemiHilbert R W
f : U → V
g : U → U
hf : HasAdjDiff R f
hg : HasAdjDiff R g
⊢ (jacobian R fun x => f (g x)) = fun x => jacobian R f x * jacobian R g x
Tactic:
sorry_proof
State after:
no goals