Commit 2023-04-29 10:38 7e05f55c

feat: allow several tactics on types that are slightly less obviously Types (#3682) Many tactics attempt to get the universe of the sort of the terms involved by matching on the level being a succ of something. Unfortunately this fails on some nontrivial examples like mvpolynomial which can have type Sort (max (u+1) (v+1)) Instead we decrement the level manually after matching it. See https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60ring.60.20tactic.20cannot.20prove.20equality.20about.20.60MvPolynomial.60/near/352549549 This PR modifies ring, ring_nf, nontriviality, polyrith, linarith, and some norm_num handlers to appropriately handle this. Test cases showing examples that failed before (inspired by the case of mvpolynomial, but in principle there could be other interesting types that have multiple universe parameters in this way, some of which may even have a linear order who knows). In doing so we factor out inferTypeQ' into its own file Mathlib.Tactic.Qq for mathlib-relevant extensions of Qq