mathlib

f675a864 - feat(data/real/{nnreal,ennreal}): add (e)nnreal.of_real_bit0/bit1 (#6617)

feat(data/real/{nnreal,ennreal}): add (e)nnreal.of_real_bit0/bit1 (#6617) Add bit0/bit1 lemmas for `nnreal.of_real`, `ennreal.of_real` and `ennreal.to_nnreal`. With these additions, it is for example possible to prove `h : ennreal.of_real (2 : ℝ) = 2 := by simp`. Co-authored-by: Rémy Degenne <remydegenne@gmail.com>