The tactic language is a special-purpose programming language for constructing proofs, indicated using the keyword by.
ennreal_arith
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.
- Tags:
- Defined in module:
- Linglib.Core.Probability.ENNRealArith