Commit 2022-08-08 21:44 b9762673

chore(data/real/ennreal): deduplicate ennreal.nat_ne_top (#15853) The lemmas ennreal.nat_ne_top and ennreal.coe_nat_ne_top are near duplicates, with the former being a simp lemma taking an explicit argument, and the latter being a non-simp lemma taking an implicit argument. The former is used slightly more frequently (in explicit form) in mathlib. We remove ennreal.coe_nat_ne_top in favor of ennreal.nat_ne_top.