chore(*): Miscellaneous lemmas (#18677)
* `algebra.support`: `support n = univ` if `n ≠ 0`, `mul_support n = univ` if `n ≠ 1`
* `data.int.char_zero`: `↑n = 1 ↔ n = 1`
* `data.real.ennreal`: `of_real a.to_real = a ↔ a ≠ ⊤`, `(of_real a).to_real = a ↔ 0 ≤ a`
* `data.set.basic`: `s ∩ {a | p a} = {a ∈ s | p a}`
* `logic.function.basic`: `on_fun f g a b = f (g a) (g b)`
* `order.conditionally_complete_lattice.basic`: Lemmas unfolding the definition of `Sup`/`Inf` on `with_top`/`with_bot`
