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

State before:
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
⊢ x ≤ x' ↔ Sup {x, x'} = x'
Tactic:
rw [Set.pair_comm x x']
State after:
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
⊢ x ≤ x' ↔ Sup {x', x} = x'

State before:
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
⊢ x ≤ x' ↔ Sup {x', x} = x'
Tactic:
exact Inf_pair (X := OrderDual X)
State after:
no goals