Theorem: Tutorial.adjunction.dual (GlimpseOfLean/Solutions/Topics/GaloisAdjunctions.lean)

State before:
X : Type u_1
Y : Type u_2
inst✝¹ : PartialOrder X
inst✝ : PartialOrder Y
l : X → Y
r : Y → X
h : adjunction l r
⊢ adjunction r l
Tactic:
intros y x
State after:
X : Type u_1
Y : Type u_2
inst✝¹ : PartialOrder X
inst✝ : PartialOrder Y
l : X → Y
r : Y → X
h : adjunction l r
y : Yᵒᵈ
x : Xᵒᵈ
⊢ r y ≤ x ↔ y ≤ l x

State before:
X : Type u_1
Y : Type u_2
inst✝¹ : PartialOrder X
inst✝ : PartialOrder Y
l : X → Y
r : Y → X
h : adjunction l r
y : Yᵒᵈ
x : Xᵒᵈ
⊢ r y ≤ x ↔ y ≤ l x
Tactic:
exact (h x y).symm
State after:
no goals