no goals
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b✝ : α
inst✝ : PartialOrder α
hs : IsAntichain (fun x x_1 => x ≤ x_1) s
a : α
x✝ : a ∈ minimals (fun x x_1 => x ≤ x_1) ↑(upperClosure s)
b : α
hb : b ∈ s
hba : b ≤ a
right✝ : ∀ ⦃b : α⦄, b ∈ ↑(upperClosure s) → (fun x x_1 => x ≤ x_1) b a → (fun x x_1 => x ≤ x_1) a b
⊢ a ∈ s
rwa [eq_of_mem_minimals ‹a ∈ _› (subset_upperClosure hb) hba]
no goals
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b✝ : α
inst✝ : PartialOrder α
hs : IsAntichain (fun x x_1 => x ≤ x_1) s
a : α
ha : a ∈ s
b : α
x✝ : b ∈ ↑(upperClosure s)
hba : (fun x x_1 => x ≤ x_1) b a
c : α
hc : c ∈ s
hcb : c ≤ b
⊢ (fun x x_1 => x ≤ x_1) a b
rwa [hs.eq' ha hc (hcb.trans hba)]