Theorem: eucl_of_symm_trans (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
⊢ Euclidean rel
Tactic:
intro w₁ w₂ w₃ r₁₂ r₁₃
State after:
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
w₁ w₂ w₃ : α
r₁₂ : rel w₁ w₂
r₁₃ : rel w₁ w₃
⊢ rel w₃ w₂

State before:
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
w₁ w₂ w₃ : α
r₁₂ : rel w₁ w₂
r₁₃ : rel w₁ w₃
⊢ rel w₃ w₂
Tactic:
have r₂₁ := hSymm r₁₂
State after:
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
w₁ w₂ w₃ : α
r₁₂ : rel w₁ w₂
r₁₃ : rel w₁ w₃
r₂₁ : rel w₂ w₁
⊢ rel w₃ w₂

State before:
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
w₁ w₂ w₃ : α
r₁₂ : rel w₁ w₂
r₁₃ : rel w₁ w₃
r₂₁ : rel w₂ w₁
⊢ rel w₃ w₂
Tactic:
exact hSymm $ hTrans r₂₁ r₁₃
State after:
no goals