Lean4
/-- `compute_degree` is a tactic to solve goals of the form
* `natDegree f = d`,
* `degree f = d`,
* `natDegree f ≤ d` (or `<`),
* `degree f ≤ d` (or `<`),
* `coeff f d = r`, if `d` is the degree of `f`.
The tactic may leave goals of the form `d' = d`, `d' ≤ d`, `d' < d`, or `r ≠ 0`, where `d'` in `ℕ`
or `WithBot ℕ` is the tactic's guess of the degree, and `r` is the coefficient's guess of the
leading coefficient of `f`.
`compute_degree` applies `norm_num` to the left-hand side of all side goals, trying to close them.
The variant `compute_degree!` first applies `compute_degree`.
Then it uses `norm_num` on all the remaining goals and tries `assumption`.
-/
@[tactic_parser 1000]
public meta def computeDegree : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.ComputeDegree.computeDegree 1022
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "compute_degree" false✝)
(ParserDescr.unary✝ `optional (ParserDescr.symbol✝ "!")))
