α : Type u_1
β : Type ?u.11422
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
t : Set α
a b : α
inst✝ : Preorder α
⊢ IsAntichain (fun x x_1 => x ≤ x_1) {a} ∧ IsGreatest {a} a
α : Type u_1
β : Type ?u.11422
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a b : α
inst✝ : Preorder α
⊢ s = {a} → IsAntichain (fun x x_1 => x ≤ x_1) s ∧ IsGreatest s a
rintro rfl
no goals
α : Type u_1
β : Type ?u.11422
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
t : Set α
a b : α
inst✝ : Preorder α
⊢ IsAntichain (fun x x_1 => x ≤ x_1) {a} ∧ IsGreatest {a} a
exact ⟨isAntichain_singleton _ _, isGreatest_singleton⟩