Theorem: extensive_of_reflex_antisymm_eucl (Logic/Vorspiel/BinaryRelations.lean)

State before:
α : Type u
rel : α → α → Prop
hRefl✝ : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl✝ : Euclidean rel
hRefl : Reflexive rel
hAntisymm : Antisymmetric rel
hEucl : Euclidean rel
⊢ Extensive rel
Tactic:
intro x y rxy
State after:
α : Type u
rel : α → α → Prop
hRefl✝ : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl✝ : Euclidean rel
hRefl : Reflexive rel
hAntisymm : Antisymmetric rel
hEucl : Euclidean rel
x y : α
rxy : rel x y
⊢ x = y

State before:
α : Type u
rel : α → α → Prop
hRefl✝ : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl✝ : Euclidean rel
hRefl : Reflexive rel
hAntisymm : Antisymmetric rel
hEucl : Euclidean rel
x y : α
rxy : rel x y
⊢ x = y
Tactic:
have rxx := hRefl x
State after:
α : Type u
rel : α → α → Prop
hRefl✝ : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl✝ : Euclidean rel
hRefl : Reflexive rel
hAntisymm : Antisymmetric rel
hEucl : Euclidean rel
x y : α
rxy : rel x y
rxx : rel x x
⊢ x = y

State before:
α : Type u
rel : α → α → Prop
hRefl✝ : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl✝ : Euclidean rel
hRefl : Reflexive rel
hAntisymm : Antisymmetric rel
hEucl : Euclidean rel
x y : α
rxy : rel x y
rxx : rel x x
⊢ x = y
Tactic:
exact hAntisymm rxy (hEucl rxx rxy)
State after:
no goals