case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set (Set α)
H : ∀ (t : Set α), t ∈ s → Set.Finite t
a✝ : Fintype ↑s
⊢ Set.Finite (⋃₀ s)
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set (Set α)
hs : Set.Finite s
H : ∀ (t : Set α), t ∈ s → Set.Finite t
⊢ Set.Finite (⋃₀ s)
cases hs
case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set (Set α)
H : ∀ (t : Set α), t ∈ s → Set.Finite t
a✝ : Fintype ↑s
this : ∀ (i : ↑s), Finite ↑↑i
⊢ Set.Finite (⋃₀ s)
case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set (Set α)
H : ∀ (t : Set α), t ∈ s → Set.Finite t
a✝ : Fintype ↑s
⊢ Set.Finite (⋃₀ s)
haveI := fun i : s => (H i i.2).to_subtype
no goals
case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set (Set α)
H : ∀ (t : Set α), t ∈ s → Set.Finite t
a✝ : Fintype ↑s
this : ∀ (i : ↑s), Finite ↑↑i
⊢ Set.Finite (⋃₀ s)
apply toFinite