α : Type u_1
inst✝ : PartialOrder α
s : Set α
hs : IsAntichain (fun x x_1 => x ≤ x_1) s
x : α
hx : x ∈ s
z : α
hy : x ∈ s
hz : z ∈ Icc x x
⊢ z ∈ s
α : Type u_1
inst✝ : PartialOrder α
s : Set α
hs : IsAntichain (fun x x_1 => x ≤ x_1) s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : α
hz : z ∈ Icc x y
⊢ z ∈ s
obtain rfl := hs.eq hx hy (hz.1.trans hz.2)
α : Type u_1
inst✝ : PartialOrder α
s : Set α
hs : IsAntichain (fun x x_1 => x ≤ x_1) s
x : α
hx : x ∈ s
z : α
hy : x ∈ s
hz : z = x
⊢ z ∈ s
α : Type u_1
inst✝ : PartialOrder α
s : Set α
hs : IsAntichain (fun x x_1 => x ≤ x_1) s
x : α
hx : x ∈ s
z : α
hy : x ∈ s
hz : z ∈ Icc x x
⊢ z ∈ s
rw [Icc_self, mem_singleton_iff] at hz
no goals
α : Type u_1
inst✝ : PartialOrder α
s : Set α
hs : IsAntichain (fun x x_1 => x ≤ x_1) s
x : α
hx : x ∈ s
z : α
hy : x ∈ s
hz : z = x
⊢ z ∈ s
rwa [hz]