α : Type u_1
β : Type u_2
s t : Set α
a b x y✝ : α
f : α → β
y : β
hs : autoParam (Set.Finite s) _auto✝
⊢ y ∈ f '' s → ncard {x | x ∈ s ∧ f x = y} ≠ 0
α : Type u_1
β : Type u_2
s t : Set α
a b x y✝ : α
f : α → β
y : β
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard {x | x ∈ s ∧ f x = y} ≠ 0 ↔ y ∈ f '' s
refine' ⟨nonempty_of_ncard_ne_zero, _⟩
case intro.intro
α : Type u_1
β : Type u_2
s t : Set α
a b x y : α
f : α → β
hs : autoParam (Set.Finite s) _auto✝
z : α
hz : z ∈ s
⊢ ncard {x | x ∈ s ∧ f x = f z} ≠ 0
α : Type u_1
β : Type u_2
s t : Set α
a b x y✝ : α
f : α → β
y : β
hs : autoParam (Set.Finite s) _auto✝
⊢ y ∈ f '' s → ncard {x | x ∈ s ∧ f x = y} ≠ 0
rintro ⟨z, hz, rfl⟩
no goals
case intro.intro
α : Type u_1
β : Type u_2
s t : Set α
a b x y : α
f : α → β
hs : autoParam (Set.Finite s) _auto✝
z : α
hz : z ∈ s
⊢ ncard {x | x ∈ s ∧ f x = f z} ≠ 0
exact @ncard_ne_zero_of_mem _ ({ x ∈ s | f x = f z }) z (mem_sep hz rfl)
  (hs.subset (sep_subset _ _))