ι : Type ?u.80471
α : Type u_1
β : Type ?u.80477
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝ : IsRefl α r
hs : Set.Finite s
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
⊢ ∃ m n, m < n ∧ r (f m) (f n)
ι : Type ?u.80471
α : Type u_1
β : Type ?u.80477
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
inst✝ : IsRefl α r
hs : Set.Finite s
⊢ PartiallyWellOrderedOn s r
intro f hf
case intro.intro.intro
ι : Type ?u.80471
α : Type u_1
β : Type ?u.80477
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝ : IsRefl α r
hs : Set.Finite s
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
m n : ℕ
hmn : m < n
h : f m = f n
⊢ ∃ m n, m < n ∧ r (f m) (f n)
ι : Type ?u.80471
α : Type u_1
β : Type ?u.80477
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝ : IsRefl α r
hs : Set.Finite s
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
⊢ ∃ m n, m < n ∧ r (f m) (f n)
obtain ⟨m, n, hmn, h⟩ := hs.exists_lt_map_eq_of_forall_mem hf
no goals
case intro.intro.intro
ι : Type ?u.80471
α : Type u_1
β : Type ?u.80477
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝ : IsRefl α r
hs : Set.Finite s
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
m n : ℕ
hmn : m < n
h : f m = f n
⊢ ∃ m n, m < n ∧ r (f m) (f n)
exact ⟨m, n, hmn, h.subst <| refl (f m)⟩