Adding superfluous hypotheses makes positivity fail

Stream: mathlib4

[Michael Rothgang]

Experimenting with positivity and finiteness support for ENNReal, I discovered that adding superfluous hypotheses can make positivity fail. This seems very surprising to me. Any ideas where this is coming from or how to debug this?
CC @Floris van Doorn @Pan Lin

import Mathlib

example {x y : ENNReal} : x + y + 1 ≠ 0 := by positivity

example {x y : ENNReal} (hx : x ≠ 0) : x + y + 1 ≠ 0 := by
  fail_if_success positivity -- why does this fail?
  sorry

[Michael Rothgang]

(For broader context, this makes finiteness less powerful also.)

[Floris van Doorn]

This seems to be a bug in the evalAdd function for positivity.
Debugging with

set_option trace.Tactic.positivity true
set_option trace.Tactic.positivity.failure true

shows that in the first case it's trying to add x + y (nonnegative) and 1 (positive) which is positive.
In the second case it's trying to add x + y (positive) and 1 (positive), and cannot figure out that this is positive.
The function docs#Mathlib.Meta.Positivity.evalAdd tries to find docs#AddRightMono in the first case and docs#AddLeftStrictMono in the second case. This second instance doesn't exists on ENNReal.

Please fix this by:

• weakening the type class instance needed for docs#add_pos (probably to AddLeftMono?)
• weakening the instance needed in evalAdd to in the positive+positive case.

[Floris van Doorn]

docs#add_pos' seems to be the version of add_pos that I want here. Is there a reason that the unprimed version assumes the stronger type-class assumptions? (I guess it's only stronger if you have a partial order: docs#addLeftMono_of_addLeftStrictMono.)

[Floris van Doorn]

#34133