Use Mathlib's polynomial derivative theorem, leaving only the derivative value equality. This tactic generates an ordinary kernel-checked proof.
Equations
- GoldbachProofTools.tacticPolynomial_deriv = Lean.ParserDescr.node `GoldbachProofTools.tacticPolynomial_deriv 1024 (Lean.ParserDescr.nonReservedSymbol "polynomial_deriv" false)
Instances For
Inspect dependencies
GoldbachProofTools.tacticPolynomial_deriv ยท compiled type and proof/definition references.