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

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