Lean4
/-- The `polyrith` tactic is no longer supported in Mathlib,
because it relied on a defunct external service.
---
Attempts to prove polynomial equality goals through polynomial arithmetic
on the hypotheses (and additional proof terms if the user specifies them).
It proves the goal by generating an appropriate call to the tactic
`linear_combination`. If this call succeeds, the call to `linear_combination`
is suggested to the user.
* `polyrith` will use all relevant hypotheses in the local context.
* `polyrith [t1, t2, t3]` will add proof terms t1, t2, t3 to the local context.
* `polyrith only [h1, h2, h3, t1, t2, t3]` will use only local hypotheses
`h1`, `h2`, `h3`, and proofs `t1`, `t2`, `t3`. It will ignore the rest of the local context.
Notes:
* This tactic only works with a working internet connection, since it calls Sage
using the SageCell web API at <https://sagecell.sagemath.org/>.
Many thanks to the Sage team and organization for allowing this use.
* This tactic assumes that the user has `curl` available on path.
-/
@[tactic_parser 1000]
public meta def «tacticPolyrithOnly[_]» : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.Polyrith.«tacticPolyrithOnly[_]» 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "polyrith" false✝)
(ParserDescr.unary✝ `optional ((with_annotate_term"&" @ParserDescr.nonReservedSymbol✝) " only" false✝)))
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " [")
((with_annotate_term"sepBy(" @ParserDescr.sepBy✝) (ParserDescr.cat✝ `term 0) "," (ParserDescr.symbol✝ ", ")
Bool.false✝))
(ParserDescr.symbol✝ "]"))))
