internlm/Lean-Github huggingface dataset:
Theorem: Relation.TotalPreorder.coRel_iff_asymRel
Proof state before:
case mp
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y : α
⊢ coRel r x y → asymRel r x y
Tactic:
intro cxy
Proof state after:
case mp
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y : α
cxy : coRel r x y
⊢ asymRel r x y
Theorem: Relation.TotalPreorder.coRel_iff_asymRel
Proof state before:
case mp
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y : α
cxy : coRel r x y
⊢ asymRel r x y
Tactic:
constructor
Proof state after:
case mp.left
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y : α
cxy : coRel r x y
⊢ r x y

case mp.right
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y : α
cxy : coRel r x y
⊢ coRel r x y
Theorem: Relation.TotalPreorder.coRel_iff_asymRel
Proof state before:
case mp.left
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y : α
cxy : coRel r x y
⊢ r x y
Tactic:
cases Total.total (r:=r) x y with
| inl hxy => exact hxy
| inr hyx => absurd cxy; exact hyx
Proof state after:
no goals
Theorem: Relation.TotalPreorder.coRel_iff_asymRel
Proof state before:
case mp.left.inl
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y : α
cxy : coRel r x y
hxy : r x y
⊢ r x y
Tactic:
exact hxy
Proof state after:
no goals
Theorem: Relation.TotalPreorder.coRel_iff_asymRel
Proof state before:
case mp.left.inr
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y : α
cxy : coRel r x y
hyx : r y x
⊢ r x y
Tactic:
absurd cxy
Proof state after:
case mp.left.inr
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y : α
cxy : coRel r x y
hyx : r y x
⊢ r y x
Theorem: Relation.TotalPreorder.coRel_iff_asymRel
Proof state before:
case mp.left.inr
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y : α
cxy : coRel r x y
hyx : r y x
⊢ r y x
Tactic:
exact hyx
Proof state after:
no goals
Theorem: Relation.TotalPreorder.coRel_iff_asymRel
Proof state before:
case mp.right
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y : α
cxy : coRel r x y
⊢ coRel r x y
Tactic:
exact cxy
Proof state after:
no goals
Theorem: Relation.TotalPreorder.coRel_iff_asymRel
Proof state before:
case mpr
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y : α
⊢ asymRel r x y → coRel r x y
Tactic:
exact And.right
Proof state after:
no goals
Theorem: Relation.TotalPreorder.co_trans
Proof state before:
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y z : α
⊢ coRel r x y → coRel r y z → coRel r x z
Tactic:
repeat rw [coRel_iff_asymRel]
Proof state after:
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y z : α
⊢ asymRel r x y → asymRel r y z → asymRel r x z
Theorem: Relation.TotalPreorder.co_trans
Proof state before:
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y z : α
⊢ asymRel r x y → asymRel r y z → asymRel r x z
Tactic:
exact Preorder.as_trans
Proof state after:
no goals
Theorem: Relation.TotalPreorder.co_trans
Proof state before:
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y z : α
⊢ asymRel r x y → asymRel r y z → coRel r x z
Tactic:
rw [coRel_iff_asymRel]
Proof state after:
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y z : α
⊢ asymRel r x y → asymRel r y z → asymRel r x z
Theorem: Relation.TotalPreorder.as_compare
Proof 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
Proof 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
Theorem: Relation.TotalPreorder.as_compare
Proof 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
Proof 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
Theorem: Relation.TotalPreorder.as_compare
Proof 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]
Proof 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
Theorem: Relation.TotalPreorder.as_compare
Proof 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
Proof state after:
no goals
Theorem: Relation.TotalPreorder.as_compare
Proof 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]
Proof 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
Theorem: Relation.TotalOrder.coRel_iff_rel_and_ne
Proof state before:
α : Sort u_1
r : α → α → Prop
self : TotalOrder r
x y : α
⊢ coRel r x y ↔ r x y ∧ x ≠ y
Tactic:
constructor
Proof state after:
case mp
α : Sort u_1
r : α → α → Prop
self : TotalOrder r
x y : α
⊢ coRel r x y → r x y ∧ x ≠ y

case mpr
α : Sort u_1
r : α → α → Prop
self : TotalOrder r
x y : α
⊢ r x y ∧ x ≠ y → coRel r x y
Theorem: Relation.TotalOrder.coRel_iff_rel_and_ne
Proof state before:
case mp
α : Sort u_1
r : α → α → Prop
self : TotalOrder r
x y : α
⊢ coRel r x y → r x y ∧ x ≠ y
Tactic:
intro cxy
Proof state after:
case mp
α : Sort u_1
r : α → α → Prop
self : TotalOrder r
x y : α
cxy : coRel r x y
⊢ r x y ∧ x ≠ y
Theorem: Relation.TotalOrder.coRel_iff_rel_and_ne
Proof state before:
case mp
α : Sort u_1
r : α → α → Prop
self : TotalOrder r
x y : α
cxy : coRel r x y
⊢ r x y ∧ x ≠ y
Tactic:
constructor
Proof state after:
case mp.left
α : Sort u_1
r : α → α → Prop
self : TotalOrder r
x y : α
cxy : coRel r x y
⊢ r x y

case mp.right
α : Sort u_1
r : α → α → Prop
self : TotalOrder r
x y : α
cxy : coRel r x y
⊢ x ≠ y
Theorem: Relation.TotalOrder.coRel_iff_rel_and_ne
Proof state before:
case mp.left
α : Sort u_1
r : α → α → Prop
self : TotalOrder r
x y : α
cxy : coRel r x y
⊢ r x y
Tactic:
cases Total.total (r:=r) x y with
| inl hxy => exact hxy
| inr hyx => absurd cxy; exact hyx
Proof state after:
no goals
Theorem: Relation.TotalOrder.coRel_iff_rel_and_ne
Proof state before:
case mp.left.inl
α : Sort u_1
r : α → α → Prop
self : TotalOrder r
x y : α
cxy : coRel r x y
hxy : r x y
⊢ r x y
Tactic:
exact hxy
Proof state after:
no goals
Theorem: Relation.TotalOrder.coRel_iff_rel_and_ne
Proof state before:
case mp.left.inr
α : Sort u_1
r : α → α → Prop
self : TotalOrder r
x y : α
cxy : coRel r x y
hyx : r y x
⊢ r x y
Tactic:
absurd cxy
Proof state after:
case mp.left.inr
α : Sort u_1
r : α → α → Prop
self : TotalOrder r
x y : α
cxy : coRel r x y
hyx : r y x
⊢ r y x
Theorem: Relation.TotalOrder.coRel_iff_rel_and_ne
Proof state before:
case mp.left.inr
α : Sort u_1
r : α → α → Prop
self : TotalOrder r
x y : α
cxy : coRel r x y
hyx : r y x
⊢ r y x
Tactic:
exact hyx
Proof state after:
no goals
Theorem: Relation.TotalOrder.coRel_iff_rel_and_ne
Proof state before:
case mp.right
α : Sort u_1
r : α → α → Prop
self : TotalOrder r
x y : α
cxy : coRel r x y
⊢ x ≠ y
Tactic:
intro | rfl => absurd cxy; exact Reflexive.rfl
Proof state after:
no goals
Theorem: Relation.TotalOrder.coRel_iff_rel_and_ne
Proof state before:
α : Sort u_1
r : α → α → Prop
self : TotalOrder r
x y : α
x✝ : x = y
cxy : coRel r x x
⊢ False
Tactic:
absurd cxy
Proof state after:
α : Sort u_1
r : α → α → Prop
self : TotalOrder r
x y : α
x✝ : x = y
cxy : coRel r x x
⊢ r x x
Theorem: Relation.TotalOrder.coRel_iff_rel_and_ne
Proof state before:
α : Sort u_1
r : α → α → Prop
self : TotalOrder r
x y : α
x✝ : x = y
cxy : coRel r x x
⊢ r x x
Tactic:
exact Reflexive.rfl
Proof state after:
no goals
Theorem: Relation.TotalOrder.coRel_iff_rel_and_ne
Proof state before:
case mpr
α : Sort u_1
r : α → α → Prop
self : TotalOrder r
x y : α
⊢ r x y ∧ x ≠ y → coRel r x y
Tactic:
intro ⟨hxy, hne⟩ hyx
Proof state after:
case mpr
α : Sort u_1
r : α → α → Prop
self : TotalOrder r
x y : α
hxy : r x y
hne : x ≠ y
hyx : r y x
⊢ False
Theorem: Relation.TotalOrder.coRel_iff_rel_and_ne
Proof state before:
case mpr
α : Sort u_1
r : α → α → Prop
self : TotalOrder r
x y : α
hxy : r x y
hne : x ≠ y
hyx : r y x
⊢ False
Tactic:
absurd hne
Proof state after:
case mpr
α : Sort u_1
r : α → α → Prop
self : TotalOrder r
x y : α
hxy : r x y
hne : x ≠ y
hyx : r y x
⊢ x = y
Theorem: Relation.TotalOrder.coRel_iff_rel_and_ne
Proof state before:
case mpr
α : Sort u_1
r : α → α → Prop
self : TotalOrder r
x y : α
hxy : r x y
hne : x ≠ y
hyx : r y x
⊢ x = y
Tactic:
exact Antisymmetric.antisymm hxy hyx
Proof state after:
no goals
Theorem: Relation.Quasiorder.rc_refl
Proof state before:
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x : α
⊢ reflRel r x x
Tactic:
right
Proof state after:
case h
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x : α
⊢ x = x
Theorem: Relation.Quasiorder.rc_refl
Proof state before:
case h
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x : α
⊢ x = x
Tactic:
rfl
Proof state after:
no goals
Theorem: Relation.Quasiorder.rc_trans
Proof state before:
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y z : α
⊢ reflRel r x y → reflRel r y z → reflRel r x z
Tactic:
intro hxy hyz
Proof state after:
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y z : α
hxy : reflRel r x y
hyz : reflRel r y z
⊢ reflRel r x z
Theorem: Relation.Quasiorder.rc_trans
Proof state before:
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y z : α
hxy : reflRel r x y
hyz : reflRel r y z
⊢ reflRel r x z
Tactic:
match hxy, hyz with
| Or.inr rfl, Or.inr rfl => right; rfl
| Or.inr rfl, Or.inl hyz => left; exact hyz
| Or.inl hxy, Or.inr rfl => left; exact hxy
| Or.inl hxy, Or.inl hyz => left; exact Transitive.trans hxy hyz
Proof state after:
no goals
Theorem: Relation.Quasiorder.rc_trans
Proof state before:
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y z : α
hxy : reflRel r x y
hyz : reflRel r y z
⊢ reflRel r x x
Tactic:
right
Proof state after:
case h
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y z : α
hxy : reflRel r x y
hyz : reflRel r y z
⊢ x = x
Theorem: Relation.Quasiorder.rc_trans
Proof state before:
case h
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y z : α
hxy : reflRel r x y
hyz : reflRel r y z
⊢ x = x
Tactic:
rfl
Proof state after:
no goals
Theorem: Relation.Quasiorder.rc_trans
Proof state before:
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y z✝ : α
hxy : reflRel r x y
hyz✝ : reflRel r y z✝
z : α
hyz : r x z
⊢ reflRel r x z
Tactic:
left
Proof state after:
case h
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y z✝ : α
hxy : reflRel r x y
hyz✝ : reflRel r y z✝
z : α
hyz : r x z
⊢ r x z
Theorem: Relation.Quasiorder.rc_trans
Proof state before:
case h
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y z✝ : α
hxy : reflRel r x y
hyz✝ : reflRel r y z✝
z : α
hyz : r x z
⊢ r x z
Tactic:
exact hyz
Proof state after:
no goals
Theorem: Relation.Quasiorder.rc_trans
Proof state before:
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y z✝ : α
hxy✝ : reflRel r x y
hyz : reflRel r y z✝
z : α
hxy : r x z
⊢ reflRel r x z
Tactic:
left
Proof state after:
case h
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y z✝ : α
hxy✝ : reflRel r x y
hyz : reflRel r y z✝
z : α
hxy : r x z
⊢ r x z
Theorem: Relation.Quasiorder.rc_trans
Proof state before:
case h
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y z✝ : α
hxy✝ : reflRel r x y
hyz : reflRel r y z✝
z : α
hxy : r x z
⊢ r x z
Tactic:
exact hxy
Proof state after:
no goals
Theorem: Relation.Quasiorder.rc_trans
Proof state before:
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y✝ z✝ : α
hxy✝ : reflRel r x y✝
hyz✝ : reflRel r y✝ z✝
z y : α
hxy : r x y
hyz : r y z
⊢ reflRel r x z
Tactic:
left
Proof state after:
case h
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y✝ z✝ : α
hxy✝ : reflRel r x y✝
hyz✝ : reflRel r y✝ z✝
z y : α
hxy : r x y
hyz : r y z
⊢ r x z
Theorem: Relation.Quasiorder.rc_trans
Proof state before:
case h
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y✝ z✝ : α
hxy✝ : reflRel r x y✝
hyz✝ : reflRel r y✝ z✝
z y : α
hxy : r x y
hyz : r y z
⊢ r x z
Tactic:
exact Transitive.trans hxy hyz
Proof state after:
no goals
Theorem: Relation.Quasiorder.rc_antisymm
Proof 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
Proof state after:
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y : α
hxy : reflRel r x y
hyx : reflRel r y x
⊢ x = y
Theorem: Relation.Quasiorder.rc_antisymm
Proof 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
Proof state after:
no goals
Theorem: Relation.Quasiorder.rc_antisymm
Proof 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
Proof state after:
no goals
Theorem: Relation.Quasiorder.rc_antisymm
Proof 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
Proof 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
Theorem: Relation.Quasiorder.rc_antisymm
Proof 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
Proof state after:
no goals
Theorem: Relation.LinearQuasiorder.co_trans
Proof state before:
α : Sort u_1
r : α → α → Prop
self : LinearQuasiorder r
x y z : α
⊢ coRel r x y → coRel r y z → coRel r x z
Tactic:
intro cxy cyz rzx
Proof state after:
α : Sort u_1
r : α → α → Prop
self : LinearQuasiorder r
x y z : α
cxy : coRel r x y
cyz : coRel r y z
rzx : r z x
⊢ False
Theorem: Relation.LinearQuasiorder.co_trans
Proof state before:
α : Sort u_1
r : α → α → Prop
self : LinearQuasiorder r
x y z : α
cxy : coRel r x y
cyz : coRel r y z
rzx : r z x
⊢ False
Tactic:
cases Comparison.compare rzx y with
| inl rzy => exact cyz rzy
| inr ryx => exact cxy ryx
Proof state after:
no goals
Theorem: Relation.LinearQuasiorder.co_trans
Proof state before:
case inl
α : Sort u_1
r : α → α → Prop
self : LinearQuasiorder r
x y z : α
cxy : coRel r x y
cyz : coRel r y z
rzx : r z x
rzy : r z y
⊢ False
Tactic:
exact cyz rzy
Proof state after:
no goals
Theorem: Relation.LinearQuasiorder.co_trans
Proof state before:
case inr
α : Sort u_1
r : α → α → Prop
self : LinearQuasiorder r
x y z : α
cxy : coRel r x y
cyz : coRel r y z
rzx : r z x
ryx : r y x
⊢ False
Tactic:
exact cxy ryx
Proof state after:
no goals
Theorem: Relation.LinearQuasiorder.co_total
Proof state before:
α : Sort u_1
r : α → α → Prop
self : LinearQuasiorder r
inst✝ : ComplementedRel r
x y : α
⊢ coRel r x y ∨ coRel r y x
Tactic:
by_cases r x y using Complemented with
| .isTrue hxy => left; exact Asymmetric.asymm hxy
| .isFalse nxy => right; exact nxy
Proof state after:
no goals
Theorem: Relation.LinearQuasiorder.co_total
Proof state before:
α : Sort u_1
r : α → α → Prop
self : LinearQuasiorder r
inst✝ : ComplementedRel r
x y : α
hxy : r x y
⊢ coRel r x y ∨ coRel r y x
Tactic:
left
Proof state after:
case h
α : Sort u_1
r : α → α → Prop
self : LinearQuasiorder r
inst✝ : ComplementedRel r
x y : α
hxy : r x y
⊢ coRel r x y
Theorem: Relation.LinearQuasiorder.co_total
Proof state before:
case h
α : Sort u_1
r : α → α → Prop
self : LinearQuasiorder r
inst✝ : ComplementedRel r
x y : α
hxy : r x y
⊢ coRel r x y
Tactic:
exact Asymmetric.asymm hxy
Proof state after:
no goals
Theorem: Relation.LinearQuasiorder.co_total
Proof state before:
α : Sort u_1
r : α → α → Prop
self : LinearQuasiorder r
inst✝ : ComplementedRel r
x y : α
nxy : ¬r x y
⊢ coRel r x y ∨ coRel r y x
Tactic:
right
Proof state after:
case h
α : Sort u_1
r : α → α → Prop
self : LinearQuasiorder r
inst✝ : ComplementedRel r
x y : α
nxy : ¬r x y
⊢ coRel r y x
Theorem: Relation.LinearQuasiorder.co_total
Proof state before:
case h
α : Sort u_1
r : α → α → Prop
self : LinearQuasiorder r
inst✝ : ComplementedRel r
x y : α
nxy : ¬r x y
⊢ coRel r y x
Tactic:
exact nxy
Proof state after:
no goals
Theorem: Relation.LinearOrder.co_antisymm
Proof state before:
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : StableEq α
x y : α
⊢ coRel r x y → coRel r y x → x = y
Tactic:
intro cxy cyx
Proof state after:
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : StableEq α
x y : α
cxy : coRel r x y
cyx : coRel r y x
⊢ x = y
Theorem: Relation.LinearOrder.co_antisymm
Proof state before:
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : StableEq α
x y : α
cxy : coRel r x y
cyx : coRel r y x
⊢ x = y
Tactic:
by_contradiction
| assuming hne =>
  cases Connex.connex (r:=r) hne with
  | inl hxy => absurd hxy; exact cyx
  | inr hyx => absurd hyx; exact cxy
Proof state after:
no goals
Theorem: Relation.LinearOrder.co_antisymm
Proof state before:
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : StableEq α
x y : α
cxy : coRel r x y
cyx : coRel r y x
hne : ¬x = y
⊢ False
Tactic:
cases Connex.connex (r:=r) hne with
| inl hxy => absurd hxy; exact cyx
| inr hyx => absurd hyx; exact cxy
Proof state after:
no goals
Theorem: Relation.LinearOrder.co_antisymm
Proof state before:
case inl
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : StableEq α
x y : α
cxy : coRel r x y
cyx : coRel r y x
hne : ¬x = y
hxy : r x y
⊢ False
Tactic:
absurd hxy
Proof state after:
case inl
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : StableEq α
x y : α
cxy : coRel r x y
cyx : coRel r y x
hne : ¬x = y
hxy : r x y
⊢ ¬r x y
Theorem: Relation.LinearOrder.co_antisymm
Proof state before:
case inl
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : StableEq α
x y : α
cxy : coRel r x y
cyx : coRel r y x
hne : ¬x = y
hxy : r x y
⊢ ¬r x y
Tactic:
exact cyx
Proof state after:
no goals
Theorem: Relation.LinearOrder.co_antisymm
Proof state before:
case inr
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : StableEq α
x y : α
cxy : coRel r x y
cyx : coRel r y x
hne : ¬x = y
hyx : r y x
⊢ False
Tactic:
absurd hyx
Proof state after:
case inr
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : StableEq α
x y : α
cxy : coRel r x y
cyx : coRel r y x
hne : ¬x = y
hyx : r y x
⊢ ¬r y x
Theorem: Relation.LinearOrder.co_antisymm
Proof state before:
case inr
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : StableEq α
x y : α
cxy : coRel r x y
cyx : coRel r y x
hne : ¬x = y
hyx : r y x
⊢ ¬r y x
Tactic:
exact cxy
Proof state after:
no goals
Theorem: Relation.LinearOrder.coRel_iff_reflRel
Proof state before:
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝¹ : StableEq α
inst✝ : ComplementedRel r
x y : α
⊢ coRel r x y ↔ reflRel r x y
Tactic:
constructor
Proof state after:
case mp
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝¹ : StableEq α
inst✝ : ComplementedRel r
x y : α
⊢ coRel r x y → reflRel r x y

case mpr
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝¹ : StableEq α
inst✝ : ComplementedRel r
x y : α
⊢ reflRel r x y → coRel r x y
Theorem: Relation.LinearOrder.coRel_iff_reflRel
Proof state before:
case mp
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝¹ : StableEq α
inst✝ : ComplementedRel r
x y : α
⊢ coRel r x y → reflRel r x y
Tactic:
intro cxy
Proof state after:
case mp
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝¹ : StableEq α
inst✝ : ComplementedRel r
x y : α
cxy : coRel r x y
⊢ reflRel r x y
Theorem: Relation.LinearOrder.coRel_iff_reflRel
Proof state before:
case mp
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝¹ : StableEq α
inst✝ : ComplementedRel r
x y : α
cxy : coRel r x y
⊢ reflRel r x y
Tactic:
by_cases r x y using Complemented with
| .isTrue hxy => left; exact hxy
| .isFalse cyx =>
  right
  by_contradiction
  | assuming hne =>
    cases Connex.connex (r:=r) hne with
    | inl hxy => absurd cyx; exact hxy
    | inr hyx => absurd cxy; exact hyx
Proof state after:
no goals
Theorem: Relation.LinearOrder.coRel_iff_reflRel
Proof state before:
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝¹ : StableEq α
inst✝ : ComplementedRel r
x y : α
cxy : coRel r x y
hxy : r x y
⊢ reflRel r x y
Tactic:
left
Proof state after:
case h
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝¹ : StableEq α
inst✝ : ComplementedRel r
x y : α
cxy : coRel r x y
hxy : r x y
⊢ r x y
Theorem: Relation.LinearOrder.coRel_iff_reflRel
Proof state before:
case h
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝¹ : StableEq α
inst✝ : ComplementedRel r
x y : α
cxy : coRel r x y
hxy : r x y
⊢ r x y
Tactic:
exact hxy
Proof state after:
no goals
Theorem: Relation.LinearOrder.coRel_iff_reflRel
Proof state before:
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝¹ : StableEq α
inst✝ : ComplementedRel r
x y : α
cxy : coRel r x y
cyx : ¬r x y
⊢ reflRel r x y
Tactic:
right
Proof state after:
case h
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝¹ : StableEq α
inst✝ : ComplementedRel r
x y : α
cxy : coRel r x y
cyx : ¬r x y
⊢ x = y
Theorem: Relation.LinearOrder.coRel_iff_reflRel
Proof state before:
case h
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝¹ : StableEq α
inst✝ : ComplementedRel r
x y : α
cxy : coRel r x y
cyx : ¬r x y
⊢ x = y
Tactic:
by_contradiction
| assuming hne =>
  cases Connex.connex (r:=r) hne with
  | inl hxy => absurd cyx; exact hxy
  | inr hyx => absurd cxy; exact hyx
Proof state after:
no goals
Theorem: Relation.LinearOrder.coRel_iff_reflRel
Proof state before:
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝¹ : StableEq α
inst✝ : ComplementedRel r
x y : α
cxy : coRel r x y
cyx : ¬r x y
hne : ¬x = y
⊢ False
Tactic:
cases Connex.connex (r:=r) hne with
| inl hxy => absurd cyx; exact hxy
| inr hyx => absurd cxy; exact hyx
Proof state after:
no goals
Theorem: Relation.LinearOrder.coRel_iff_reflRel
Proof state before:
case inl
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝¹ : StableEq α
inst✝ : ComplementedRel r
x y : α
cxy : coRel r x y
cyx : ¬r x y
hne : ¬x = y
hxy : r x y
⊢ False
Tactic:
absurd cyx
Proof state after:
case inl
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝¹ : StableEq α
inst✝ : ComplementedRel r
x y : α
cxy : coRel r x y
cyx : ¬r x y
hne : ¬x = y
hxy : r x y
⊢ r x y
Theorem: Relation.LinearOrder.coRel_iff_reflRel
Proof state before:
case inl
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝¹ : StableEq α
inst✝ : ComplementedRel r
x y : α
cxy : coRel r x y
cyx : ¬r x y
hne : ¬x = y
hxy : r x y
⊢ r x y
Tactic:
exact hxy
Proof state after:
no goals
Theorem: Relation.LinearOrder.coRel_iff_reflRel
Proof state before:
case inr
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝¹ : StableEq α
inst✝ : ComplementedRel r
x y : α
cxy : coRel r x y
cyx : ¬r x y
hne : ¬x = y
hyx : r y x
⊢ False
Tactic:
absurd cxy
Proof state after:
case inr
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝¹ : StableEq α
inst✝ : ComplementedRel r
x y : α
cxy : coRel r x y
cyx : ¬r x y
hne : ¬x = y
hyx : r y x
⊢ r y x
Theorem: Relation.LinearOrder.coRel_iff_reflRel
Proof state before:
case inr
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝¹ : StableEq α
inst✝ : ComplementedRel r
x y : α
cxy : coRel r x y
cyx : ¬r x y
hne : ¬x = y
hyx : r y x
⊢ r y x
Tactic:
exact hyx
Proof state after:
no goals
Theorem: Relation.LinearOrder.coRel_iff_reflRel
Proof state before:
case mpr
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝¹ : StableEq α
inst✝ : ComplementedRel r
x y : α
⊢ reflRel r x y → coRel r x y
Tactic:
intro
| .inr rfl => exact Quasiorder.co_refl x
| .inl hxy => exact Asymmetric.asymm hxy
Proof state after:
no goals