α : Type u_1
β : Type u_2
γ : Type ?u.51492
inst✝ : Fintype α
s : Finset β
h : Fintype.card α ≤ Fintype.card { x // x ∈ s }
⊢ ∃ f, Set.range ↑f ⊆ ↑s
α : Type u_1
β : Type u_2
γ : Type ?u.51492
inst✝ : Fintype α
s : Finset β
h : Fintype.card α ≤ card s
⊢ ∃ f, Set.range ↑f ⊆ ↑s
rw [← Fintype.card_coe] at h
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.51492
inst✝ : Fintype α
s : Finset β
h : Fintype.card α ≤ Fintype.card { x // x ∈ s }
f : α ↪ { x // x ∈ s }
⊢ ∃ f, Set.range ↑f ⊆ ↑s
α : Type u_1
β : Type u_2
γ : Type ?u.51492
inst✝ : Fintype α
s : Finset β
h : Fintype.card α ≤ Fintype.card { x // x ∈ s }
⊢ ∃ f, Set.range ↑f ⊆ ↑s
rcases nonempty_of_card_le h with ⟨f⟩
no goals
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.51492
inst✝ : Fintype α
s : Finset β
h : Fintype.card α ≤ Fintype.card { x // x ∈ s }
f : α ↪ { x // x ∈ s }
⊢ ∃ f, Set.range ↑f ⊆ ↑s
exact ⟨f.trans (Embedding.subtype _), by simp [Set.range_subset_iff]⟩
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.51492
inst✝ : Fintype α
s : Finset β
h : Fintype.card α ≤ Fintype.card { x // x ∈ s }
f : α ↪ { x // x ∈ s }
⊢ Set.range ↑(Embedding.trans f (subtype fun x => x ∈ s)) ⊆ ↑s
simp [Set.range_subset_iff]