Theorem: trans_of_refl_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
⊢ Transitive rel
Tactic:
have hSymm := symm_of_refl_eucl hRefl hEucl
State after:
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm✝ : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
hSymm : Symmetric rel
⊢ Transitive rel

State before:
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm✝ : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
hSymm : Symmetric rel
⊢ Transitive rel
Tactic:
exact trans_of_symm_eucl hSymm hEucl
State after:
no goals