Theorem: Relation.TotalPreorder.as_compare (GMLInit/Logic/Ordering.lean)

State before:
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
inst✝ : WeaklyComplementedRel r
x y : α
⊢ asymRel r x y → ∀ (z : α), asymRel r x z ∨ asymRel r z y
Tactic:
intro h z
State after:
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
inst✝ : WeaklyComplementedRel r
x y : α
h : asymRel r x y
z : α
⊢ asymRel r x z ∨ asymRel r z y

State before:
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
inst✝ : WeaklyComplementedRel r
x y : α
h : asymRel r x y
z : α
⊢ asymRel r x z ∨ asymRel r z y
Tactic:
rw [←coRel_iff_asymRel] at h
State after:
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
inst✝ : WeaklyComplementedRel r
x y : α
h : coRel r x y
z : α
⊢ asymRel r x z ∨ asymRel r z y

State before:
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
inst✝ : WeaklyComplementedRel r
x y : α
h : coRel r x y
z : α
⊢ asymRel r x z ∨ asymRel r z y
Tactic:
repeat rw [←coRel_iff_asymRel]
State after:
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
inst✝ : WeaklyComplementedRel r
x y : α
h : coRel r x y
z : α
⊢ coRel r x z ∨ coRel r z y

State before:
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
inst✝ : WeaklyComplementedRel r
x y : α
h : coRel r x y
z : α
⊢ coRel r x z ∨ coRel r z y
Tactic:
exact Preorder.co_compare h z
State after:
no goals

State before:
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
inst✝ : WeaklyComplementedRel r
x y : α
h : coRel r x y
z : α
⊢ coRel r x z ∨ asymRel r z y
Tactic:
rw [←coRel_iff_asymRel]
State after:
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
inst✝ : WeaklyComplementedRel r
x y : α
h : coRel r x y
z : α
⊢ coRel r x z ∨ coRel r z y