mathlib3

c1686dff - feat(data/real/ennreal): interactions between infi/supr and to_nnreal/to_real (#18946)

feat(data/real/ennreal): interactions between infi/supr and to_nnreal/to_real (#18946) Add lemmas relating `ennreal.to_real` and `ennreal.to_nnreal` to the indexed infimum. Note that a slightly different set of lemmas and proofs were added in leanprover-community/mathlib4#3457. Please make sure to switch to these versions when forward-porting, and add `#align`s to the existing lemmas. This also adds `inf_dist_eq_infi`, which is from the same mathlib4 PR. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>