case inl
α : Type u_1
r r₁ r₂ : α → α → Prop
t : Set α
a b : α
h : Set.Subsingleton ∅
⊢ maximals r ∅ = ∅

case inr.intro
α : Type u_1
r r₁ r₂ : α → α → Prop
t : Set α
a b x : α
h : Set.Subsingleton {x}
⊢ maximals r {x} = {x}
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a b : α
h : Set.Subsingleton s
⊢ maximals r s = s
rcases h.eq_empty_or_singleton with (rfl | ⟨x, rfl⟩)
no goals
case inl
α : Type u_1
r r₁ r₂ : α → α → Prop
t : Set α
a b : α
h : Set.Subsingleton ∅
⊢ maximals r ∅ = ∅

case inr.intro
α : Type u_1
r r₁ r₂ : α → α → Prop
t : Set α
a b x : α
h : Set.Subsingleton {x}
⊢ maximals r {x} = {x}
exacts [minimals_empty _, maximals_singleton _ _]