Feature request: positivity with extra terms

Stream: mathlib4

[Mitchell Lee]

linarith [t1, t2, t3] means linarith with the additional terms t1, t2, t3. This is quite useful.
Would it be possible for positivity [t1, t2, t3] to mean positivity with the additional terms t1, t2, t3?
(I suppose the same question could be asked for other tactics, like continuity, as well.)

As an example use case, here is my solution to an exercise in chapter 6 of Mathematics in Lean, which asks to define the weighted average operation on the standard 2-simplex. I would prefer to say positivity [a.x_nonneg, b.x_nonneg] rather than the ugly have := a.x_nonneg; have := b.x_nonneg; positivity.

def weightedAverage (lambda : Real) (lambda_nonneg : 0 ≤ lambda) (lambda_le : lambda ≤ 1)
    (a b : StandardTwoSimplex) : StandardTwoSimplex :=
      let_fun _ : 0 ≤ 1 - lambda := by linarith;
      { x := lambda * a.x + (1 - lambda) * b.x,
        y := lambda * a.y + (1 - lambda) * b.y,
        z := lambda * a.z + (1 - lambda) * b.z,
        x_nonneg := by have := a.x_nonneg; have := b.x_nonneg; positivity,
        y_nonneg := by have := a.y_nonneg; have := b.y_nonneg; positivity,
        z_nonneg := by have := a.z_nonneg; have := b.z_nonneg; positivity,
        sum_eq := by linear_combination lambda * a.sum_eq + (1 - lambda) * b.sum_eq}

[Kyle Miller]

I think it's good to have composable tactics, over giving tactics custom syntax in a piecemeal fashion.

Introducing a number of facts into the local context in a convenient way could be a tactic. Imagine something like

by have [a.x_nonneg, b.x_nonneg]; positivity,

[Yaël Dillies]

Yes I am working on this