α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : Infinite α
s : Set β
f : α → β
hi : Injective f
hf : (range fun x => f x) ⊆ s
⊢ Set.Infinite s
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : Infinite α
s : Set β
f : α → β
hi : Injective f
hf : ∀ (x : α), f x ∈ s
⊢ Set.Infinite s
rw [← range_subset_iff] at hf
no goals
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : Infinite α
s : Set β
f : α → β
hi : Injective f
hf : (range fun x => f x) ⊆ s
⊢ Set.Infinite s
exact (infinite_range_of_injective hi).mono hf