α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝¹ : IsTrans α r
inst✝ : IsAntisymm α r
hs : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → r a b
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ a = b
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝¹ : IsTrans α r
inst✝ : IsAntisymm α r
hs : Chain r s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ a = b
rw [chain_iff_pairwise] at hs
no goals
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝¹ : IsTrans α r
inst✝ : IsAntisymm α r
hs : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → r a b
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ a = b
exact antisymm (hs a ha b hb) (hs b hb a ha)