α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : LinearOrder α
inst✝ : Infinite α
t : Set β
f : α → β
hf : MapsTo (fun a => f a) univ t
ht : Set.Finite t
⊢ ∃ a b, a < b ∧ f a = f b
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : LinearOrder α
inst✝ : Infinite α
t : Set β
f : α → β
hf : ∀ (a : α), f a ∈ t
ht : Set.Finite t
⊢ ∃ a b, a < b ∧ f a = f b
rw [← maps_univ_to] at hf
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : LinearOrder α
inst✝ : Infinite α
t : Set β
f : α → β
hf : MapsTo (fun a => f a) univ t
ht : Set.Finite t
a b : α
h : a < b ∧ f a = f b
⊢ ∃ a b, a < b ∧ f a = f b
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : LinearOrder α
inst✝ : Infinite α
t : Set β
f : α → β
hf : MapsTo (fun a => f a) univ t
ht : Set.Finite t
⊢ ∃ a b, a < b ∧ f a = f b
obtain ⟨a, -, b, -, h⟩ := infinite_univ.exists_lt_map_eq_of_mapsTo hf ht
no goals
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : LinearOrder α
inst✝ : Infinite α
t : Set β
f : α → β
hf : MapsTo (fun a => f a) univ t
ht : Set.Finite t
a b : α
h : a < b ∧ f a = f b
⊢ ∃ a b, a < b ∧ f a = f b
exact ⟨a, b, h⟩