α : Type u_1
β : Type ?u.1530
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a✝ b✝ : α
inst✝ : IsTrichotomous α r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ a = b
α : Type u_1
β : Type ?u.1530
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a b : α
inst✝ : IsTrichotomous α r
h : IsAntichain r s
⊢ Set.Subsingleton s
rintro a ha b hb
case inl
α : Type u_1
β : Type ?u.1530
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a✝ b✝ : α
inst✝ : IsTrichotomous α r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : r a b
⊢ a = b

case inr.inl
α : Type u_1
β : Type ?u.1530
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a✝ b✝ : α
inst✝ : IsTrichotomous α r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a = b
⊢ a = b

case inr.inr
α : Type u_1
β : Type ?u.1530
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a✝ b✝ : α
inst✝ : IsTrichotomous α r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : r b a
⊢ a = b
α : Type u_1
β : Type ?u.1530
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a✝ b✝ : α
inst✝ : IsTrichotomous α r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ a = b
obtain hab | hab | hab := trichotomous_of r a b
no goals
case inl
α : Type u_1
β : Type ?u.1530
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a✝ b✝ : α
inst✝ : IsTrichotomous α r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : r a b
⊢ a = b
exact h.eq ha hb hab
no goals
case inr.inl
α : Type u_1
β : Type ?u.1530
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a✝ b✝ : α
inst✝ : IsTrichotomous α r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a = b
⊢ a = b
exact hab
no goals
case inr.inr
α : Type u_1
β : Type ?u.1530
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a✝ b✝ : α
inst✝ : IsTrichotomous α r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : r b a
⊢ a = b
exact h.eq' ha hb hab