Theorem: Relation.Quasiorder.asymm (GMLInit/Logic/Ordering.lean)

State before:
α : Sort ?u.1585
r : α → α → Prop
self : Quasiorder r
x y : α
⊢ r x y → ¬r y x
Tactic:
intro hxy hyx
State after:
α : Sort ?u.1585
r : α → α → Prop
self : Quasiorder r
x y : α
hxy : r x y
hyx : r y x
⊢ False

State before:
α : Sort ?u.1585
r : α → α → Prop
self : Quasiorder r
x y : α
hxy : r x y
hyx : r y x
⊢ False
Tactic:
apply self.irrefl x
State after:
α : Sort ?u.1585
r : α → α → Prop
self : Quasiorder r
x y : α
hxy : r x y
hyx : r y x
⊢ r x x

State before:
α : Sort ?u.1585
r : α → α → Prop
self : Quasiorder r
x y : α
hxy : r x y
hyx : r y x
⊢ r x x
Tactic:
exact self.trans hxy hyx
State after:
no goals