case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
p : α → Prop
a✝ : Fintype ↑s
⊢ Set.Finite {a | a ∈ s ∧ p a}
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
hs : Set.Finite s
p : α → Prop
⊢ Set.Finite {a | a ∈ s ∧ p a}
cases hs
no goals
case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
p : α → Prop
a✝ : Fintype ↑s
⊢ Set.Finite {a | a ∈ s ∧ p a}
apply toFinite