Theorem: Lean4Axiomatic.Relation.trans_failL (Lean4Axiomatic/Relation/Equivalence/Core.lean)

State before:
α : Sort u
R : α → α → Prop
inst✝¹ : Symmetric R
inst✝ : Transitive R
x y z : α
⊢ ¬R x y → R y z → ¬R x z
Tactic:
intro (_ : ¬ R x y) (_ : R y z) (_ : R x z)
State after:
α : Sort u
R : α → α → Prop
inst✝¹ : Symmetric R
inst✝ : Transitive R
x y z : α
x✝² : ¬R x y
x✝¹ : R y z
x✝ : R x z
⊢ False

State before:
α : Sort u
R : α → α → Prop
inst✝¹ : Symmetric R
inst✝ : Transitive R
x y z : α
x✝² : ¬R x y
x✝¹ : R y z
x✝ : R x z
⊢ False
Tactic:
have : R x y := trans ‹R x z› (symm ‹R y z›)
State after:
α : Sort u
R : α → α → Prop
inst✝¹ : Symmetric R
inst✝ : Transitive R
x y z : α
x✝² : ¬R x y
x✝¹ : R y z
x✝ : R x z
this : R x y
⊢ False

State before:
α : Sort u
R : α → α → Prop
inst✝¹ : Symmetric R
inst✝ : Transitive R
x y z : α
x✝² : ¬R x y
x✝¹ : R y z
x✝ : R x z
this : R x y
⊢ False
Tactic:
exact ‹¬ R x y› ‹R x y›
State after:
no goals