mathlib3

2d915e4e - chore(tactic/{core + compute_degree}): tightening up compute_degree_le (#15649)

chore(tactic/{core + compute_degree}): tightening up compute_degree_le (#15649) This PR instantiates meta-variables to fix [this bug](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/debugging.20.60compute_degree_le.60), using code of Floris. I also tightened up the main tactic: it uses focus1 and it has a version that does not throw errors, suitable for iterations.