Some positivity developments got caught up in the port. Here are a few items we should implement without needing to bother backporting:

• On the fly feeding of hypotheses: positivity [h₁, h₂] should be the same as have := h₁; have := h₂; positivity. [Merged by Bors] - feat(Positivity): add support for positivity [h₁, h₂] syntax #30388
• Extension for subtraction. As this is deemed less predictable than usual extensions (a ≤ b/a < b/a ≠ b are not positivity assumptions), the preconditions should only be looked for in the hypotheses given on the fly. See feat(tactic/positivity): Extension for subtraction mathlib3#16632