mathlib

914250ef - chore(data/real/ennreal): adjust form of `to_real_pos_iff` (#11047)

chore(data/real/ennreal): adjust form of `to_real_pos_iff` (#11047) We have a principle (which may not have been crystallized at the time of writing of `data/real/ennreal`) that hypotheses of lemmas should contain the weak form `a ≠ ∞`, while conclusions should report the strong form `a < ∞`, and also the same for `a ≠ 0`, `0 < a`. In the case of the existing lemma ```lean lemma to_real_pos_iff : 0 < a.to_real ↔ (0 < a ∧ a ≠ ∞):= ``` it's not clear whether the RHS of the iff should count as a hypothesis or a conclusion. So I have rewritten to provide two forms, ```lean lemma to_real_pos_iff : 0 < a.to_real ↔ (0 < a ∧ a < ∞):= lemma to_real_pos {a : ℝ≥0∞} (ha₀ : a ≠ 0) (ha_top : a ≠ ∞) : 0 < a.to_real := ``` Having both versions available shortens many proofs slightly.