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

State before:
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y : α
⊢ reflRel r x y → reflRel r y x → x = y
Tactic:
intro hxy hyx
State after:
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y : α
hxy : reflRel r x y
hyx : reflRel r y x
⊢ x = y

State before:
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y : α
hxy : reflRel r x y
hyx : reflRel r y x
⊢ x = y
Tactic:
match hxy, hyx with
| Or.inr rfl, _ => rfl
| _, Or.inr rfl => rfl
| Or.inl hxy, Or.inl hyx =>
  absurd hxy
  exact Asymmetric.asymm hyx
State after:
no goals

State before:
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y : α
hxy : reflRel r x y
hyx : reflRel r y x
x✝ : reflRel r x x
⊢ x = x
Tactic:
rfl
State after:
no goals

State before:
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y✝ : α
hxy✝ : reflRel r x y✝
hyx✝ : reflRel r y✝ x
y : α
hxy : r x y
hyx : r y x
⊢ x = y
Tactic:
absurd hxy
State after:
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y✝ : α
hxy✝ : reflRel r x y✝
hyx✝ : reflRel r y✝ x
y : α
hxy : r x y
hyx : r y x
⊢ ¬r x y

State before:
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y✝ : α
hxy✝ : reflRel r x y✝
hyx✝ : reflRel r y✝ x
y : α
hxy : r x y
hyx : r y x
⊢ ¬r x y
Tactic:
exact Asymmetric.asymm hyx
State after:
no goals