α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b : α
ht : IsAntichain r t
h : minimals r s ⊆ t
hs : ∀ ⦃a : α⦄, a ∈ t → ∃ b, b ∈ minimals r s ∧ r a b
a : α
ha : a ∈ t
⊢ a ∈ minimals r s
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a b : α
ht : IsAntichain r t
h : minimals r s ⊆ t
hs : ∀ ⦃a : α⦄, a ∈ t → ∃ b, b ∈ minimals r s ∧ r a b
⊢ minimals r s = t
refine' h.antisymm fun a ha => _
case intro.intro
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b✝ : α
ht : IsAntichain r t
h : minimals r s ⊆ t
hs : ∀ ⦃a : α⦄, a ∈ t → ∃ b, b ∈ minimals r s ∧ r a b
a : α
ha : a ∈ t
b : α
hb : b ∈ minimals r s
hr : r a b
⊢ a ∈ minimals r s
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b : α
ht : IsAntichain r t
h : minimals r s ⊆ t
hs : ∀ ⦃a : α⦄, a ∈ t → ∃ b, b ∈ minimals r s ∧ r a b
a : α
ha : a ∈ t
⊢ a ∈ minimals r s
obtain ⟨b, hb, hr⟩ := hs ha
no goals
case intro.intro
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b✝ : α
ht : IsAntichain r t
h : minimals r s ⊆ t
hs : ∀ ⦃a : α⦄, a ∈ t → ∃ b, b ∈ minimals r s ∧ r a b
a : α
ha : a ∈ t
b : α
hb : b ∈ minimals r s
hr : r a b
⊢ a ∈ minimals r s
rwa [of_not_not fun hab => ht ha (h hb) hab hr]