Theorem: Relation.Preorder.as_irrefl (GMLInit/Logic/Ordering.lean)

State before:
α : Sort u_1
r : α → α → Prop
self : Preorder r
x : α
⊢ ¬asymRel r x x
Tactic:
intro ⟨_, cxx⟩
State after:
α : Sort u_1
r : α → α → Prop
self : Preorder r
x : α
left✝ : r x x
cxx : coRel r x x
⊢ False

State before:
α : Sort u_1
r : α → α → Prop
self : Preorder r
x : α
left✝ : r x x
cxx : coRel r x x
⊢ False
Tactic:
exact co_irrefl x cxx
State after:
no goals