case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
ht : t ⊆ s
a✝ : Fintype ↑s
⊢ Set.Finite t
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
hs : Set.Finite s
t : Set α
ht : t ⊆ s
⊢ Set.Finite t
cases hs
case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
ht : t ⊆ s
a✝ : Fintype ↑s
this : Finite ↑t
⊢ Set.Finite t
case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
ht : t ⊆ s
a✝ : Fintype ↑s
⊢ Set.Finite t
haveI := Finite.Set.subset _ ht
no goals
case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
ht : t ⊆ s
a✝ : Fintype ↑s
this : Finite ↑t
⊢ Set.Finite t
apply toFinite