Theorem: refl_of_symm_serial_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
⊢ Reflexive rel
Tactic:
rintro w₁
State after:
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
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₁ : α
⊢ rel w₁ w₁
Tactic:
obtain ⟨w₂, r₁₂⟩ := hSerial w₁
State after:
case intro
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
w₁ w₂ : α
r₁₂ : rel w₁ w₂
⊢ rel w₁ w₁

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

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