α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b : α
h : IsAntichain r s
a : α
ha hb : a ∈ s
hab : r a a
⊢ r a a
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b✝ : α
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : r a b
⊢ r b a
obtain rfl := h.eq ha hb hab
no goals
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b : α
h : IsAntichain r s
a : α
ha hb : a ∈ s
hab : r a a
⊢ r a a
exact hab