Theorem: Tutorial.Inf_pair (GlimpseOfLean/Exercises/Topics/GaloisAdjunctions.lean)

State before:
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
⊢ x ≤ x' ↔ Inf {x, x'} = x
Tactic:
sorry
State after:
no goals