mathlib

2e6c488c - chore(order/complete_lattice): use `Prop` args in `infi_inf` etc (#3611)

chore(order/complete_lattice): use `Prop` args in `infi_inf` etc (#3611) This way one can `rw binfi_inf` first, then prove `∃ i, p i`. Also move some code up to make it available near `infi_inf`.