18188 T2Space is Antitone: to golf or not to golf

Stream: PR reviews

[Michael Rothgang]

I just reviewed #18188. The proof is good (one lemma, five lines of proof), but I wonder if a slightly different (shorter) route is preferrable. Style opinions on which version is preferred are welcome.

[Violeta Hernández]

My general opinion is that full term-mode is preferred for very short proofs (one or two lines at most), while readable tactics are preferred everywhere else

[Jireh Loreaux]

My opinion is that:

1. I'm not sure why we want this lemma at all.
2. If we did, I'd go with this proof (note that it uses the lemma which I think is actually more useful):

import Mathlib.Topology.Separation

theorem t2Space_antitone {X : Type*} : Antitone (@T2Space X) :=
  fun inst₁ inst₂ h_top h_t2 ↦ @T2Space.of_injective_continuous _ _ inst₁ inst₂
    h_t2 _ Function.injective_id <| continuous_id_of_le h_top

Of course, there may be even better proofs than this.