Scalar derivative rules

We reuse mathlib's calculus rules, then normalize the resulting derivative algebraically. Keeping this rule set separate from the tensor rules prevents the normalization step from recursively calling itself. The unindexed rules also match eta-reduced functions such as (3 * ·). Strict recursive ring normalization also identifies equivalent arguments inside nonlinear functions, such as tanh (x*x) and tanh (x^2), before comparing derivative formulas.

def attrAutograd : Lean.ParserDescr

Register a derivative lemma or an autograd certificate for autograd.

Rules are applied with backtracking. Prefer a conclusion that names the operation being proved; domain restrictions belong in the hypotheses, not in the tactic implementation.

def attrAutogradSimp : Lean.ParserDescr

Register a proved rewrite for use inside autograd expressions. For jet laws, orient rules from mathematical jets to runtime operations. Keep domain conditions in the hypotheses. Unlike @[simp], this registration affects only the autograd simplifier.