Theorem: Lean4Axiomatic.Relation.trans_failR (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 y z := trans (symm ‹R x y›) ‹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
this : R y 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
this : R y z
⊢ False
Tactic:
exact ‹¬ R y z› ‹R y z›
State after:
no goals