no goals
α : Type u_2
β : Type u_1
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : card s ≤ card t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
this : Inhabited { x // x ∈ s }
f' : { x // x ∈ s } → { x // x ∈ t } := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
g : { x // x ∈ t } → { x // x ∈ s } := surjInv (_ : ∀ (x : { x // x ∈ t }), ∃ a, f' a = x)
hg : Injective g
x : { x // x ∈ s }
⊢ card (attach s) ≤ card (attach t)
simpa