mathlib3

9d8c0f82 - doc(tactic/compute_degree): fix tactic tags, add examples to docs (#15680)