ι : Type ?u.49249
α : Type u_1
β : Type ?u.49255
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
ha : IsAntichain r s
hp : PartiallyWellOrderedOn s r
hi : Set.Infinite s
⊢ False
ι : Type ?u.49249
α : Type u_1
β : Type ?u.49255
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
ha : IsAntichain r s
hp : PartiallyWellOrderedOn s r
⊢ Set.Finite s
refine' not_infinite.1 fun hi => _
case intro.intro.intro
ι : Type ?u.49249
α : Type u_1
β : Type ?u.49255
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
ha : IsAntichain r s
hp : PartiallyWellOrderedOn s r
hi : Set.Infinite s
m n : ℕ
hmn : m < n
h : r ↑(↑(Infinite.natEmbedding s hi) m) ↑(↑(Infinite.natEmbedding s hi) n)
⊢ False
ι : Type ?u.49249
α : Type u_1
β : Type ?u.49255
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
ha : IsAntichain r s
hp : PartiallyWellOrderedOn s r
hi : Set.Infinite s
⊢ False
obtain ⟨m, n, hmn, h⟩ := hp (fun n => hi.natEmbedding _ n) fun n => (hi.natEmbedding _ n).2
no goals
case intro.intro.intro
ι : Type ?u.49249
α : Type u_1
β : Type ?u.49255
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
ha : IsAntichain r s
hp : PartiallyWellOrderedOn s r
hi : Set.Infinite s
m n : ℕ
hmn : m < n
h : r ↑(↑(Infinite.natEmbedding s hi) m) ↑(↑(Infinite.natEmbedding s hi) n)
⊢ False
exact hmn.ne ((hi.natEmbedding _).injective <| Subtype.val_injective <|
  ha.eq (hi.natEmbedding _ m).2 (hi.natEmbedding _ n).2 h)