nonneg_of_forall tactic

Closes 0 ≤ f a₁ + f a₂ + ⋯ + f aₙ given ∀ x, 0 ≤ f x in context.

Decomposes sums via add_nonneg (and products via mul_nonneg), then closes leaf goals by applying forall-quantified non-negativity hypotheses from the local context.

Typical usage at QUD-based RSAConfig construction sites:

s1Score_nonneg := by
  intro l0 α q w u hl _; cases q <;> simp [qudProject] <;> nonneg_of_forall

def tacticNonneg_of_forall : Lean.ParserDescr

Close 0 ≤ f a₁ + f a₂ + ⋯ + f aₙ given ∀ x, 0 ≤ f x in context.

Decomposes sums via add_nonneg (and products via mul_nonneg), then closes leaf goals by applying forall-quantified non-negativity hypotheses from the local context.

Equations

• tacticNonneg_of_forall = Lean.ParserDescr.node `tacticNonneg_of_forall 1024 (Lean.ParserDescr.nonReservedSymbol "nonneg_of_forall" false)