English
If hh₂ is differentiable at h(x) with derivative h₂', and hh is differentiable at x with derivative h', then the derivative of the composition h₂ ∘ h at x is h₂' * h'.
Русский
Если h₂ дифференцируема в h(x) с производной h₂', и h дифференцируема в x с производной h', то производная композиции h₂ ∘ h в x равна h₂' * h'.
LaTeX
$$$$\\forall x:\\ HasDerivAt hh₂(h(x))\\; \\land\\; HasDerivAt hh(x) \\,=>\\; HasDerivAt (h_2\\circ h) (h_2' * h') x. $$$$
Lean4
/-- The chain rule.
Note that the function `h₂` is a function on an algebra. If you are looking for the chain rule
with `h₂` taking values in a vector space, use `HasDerivAt.scomp_of_eq`. -/
theorem comp_of_eq (hh₂ : HasDerivAt h₂ h₂' y) (hh : HasDerivAt h h' x) (hy : y = h x) :
HasDerivAt (h₂ ∘ h) (h₂' * h') x := by rw [hy] at hh₂; exact hh₂.comp x hh
