α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b : α
ht : IsAntichain r t
h : maximals r s ⊆ t
hs : ∀ ⦃a : α⦄, a ∈ t → ∃ b, b ∈ maximals r s ∧ r b a
a : α
ha : a ∈ t
⊢ a ∈ maximals r s
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a b : α
ht : IsAntichain r t
h : maximals r s ⊆ t
hs : ∀ ⦃a : α⦄, a ∈ t → ∃ b, b ∈ maximals r s ∧ r b a
⊢ maximals r s = t
refine' h.antisymm fun a ha => _
case intro.intro
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b✝ : α
ht : IsAntichain r t
h : maximals r s ⊆ t
hs : ∀ ⦃a : α⦄, a ∈ t → ∃ b, b ∈ maximals r s ∧ r b a
a : α
ha : a ∈ t
b : α
hb : b ∈ maximals r s
hr : r b a
⊢ a ∈ maximals r s
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b : α
ht : IsAntichain r t
h : maximals r s ⊆ t
hs : ∀ ⦃a : α⦄, a ∈ t → ∃ b, b ∈ maximals r s ∧ r b a
a : α
ha : a ∈ t
⊢ a ∈ maximals r s
obtain ⟨b, hb, hr⟩ := hs ha
no goals
case intro.intro
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b✝ : α
ht : IsAntichain r t
h : maximals r s ⊆ t
hs : ∀ ⦃a : α⦄, a ∈ t → ∃ b, b ∈ maximals r s ∧ r b a
a : α
ha : a ∈ t
b : α
hb : b ∈ maximals r s
hr : r b a
⊢ a ∈ maximals r s
rwa [of_not_not fun hab => ht (h hb) ha (Ne.symm hab) hr]