ennreal_arith tactic

Discharges concrete ℝ≥0∞ arithmetic goals — equalities, strict inequalities, and negated strict inequalities — between sums of rational literals. Mathlib's norm_num does not extend across ⊤, and field_simp / bound / gcongr / ring likewise do not handle ENNReal. The established pattern is to lift through ENNReal.toReal (which requires ≠ ⊤ finiteness witnesses on both sides) and discharge the residual real arithmetic with norm_num.

This file packages that pattern as a tactic. Helper lemmas ENNReal.eq_of_toReal, ENNReal.lt_of_toReal, ENNReal.le_of_toReal provide the lifts; the macro tries equality first, then strict inequality, then negated strict inequality (via not_lt.mpr reduces to non-strict).

Typical usage in finite-PMF construction:

PMF.ofFintype (fun w => match w.val with | 0 => 3/8 | 1 => 1/8 | ...)
  (by rw [Fin.sum_univ_four]; ennreal_arith)

theorem ENNReal.eq_of_toReal {a b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ ⊤) (h : a.toReal = b.toReal) : a = b

Equality of ℝ≥0∞ values via toReal, given finiteness on both sides.

theorem ENNReal.lt_of_toReal {a b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ ⊤) (h : a.toReal < b.toReal) : a < b

Strict inequality of ℝ≥0∞ values via toReal, given finiteness on both sides.

theorem ENNReal.le_of_toReal {a b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ ⊤) (h : a.toReal ≤ b.toReal) : a ≤ b

Non-strict inequality of ℝ≥0∞ values via toReal, given finiteness on both sides.

def tacticEnnreal_arith : Lean.ParserDescr

Discharge a concrete ℝ≥0∞ arithmetic goal — equality a = b, strict inequality a < b, or negated strict inequality ¬ a < b — between nonnegative real numerical expressions built from +, *, /, and natural-number literals.

Lifts through ENNReal.toReal (with ≠ ⊤ side conditions discharged by simp [ENNReal.add_eq_top, ENNReal.div_eq_top]) and closes the residual real-arithmetic goal with norm_num.

Equations

• tacticEnnreal_arith = Lean.ParserDescr.node `tacticEnnreal_arith 1024 (Lean.ParserDescr.nonReservedSymbol "ennreal_arith" false)