α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : Finite ι
f : ι → Set α
H : ∀ (i : ι), Set.Finite (f i)
this : (i : ι) → Fintype ↑(f i)
⊢ Set.Finite (⋃ (i : ι), f i)
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : Finite ι
f : ι → Set α
H : ∀ (i : ι), Set.Finite (f i)
⊢ Set.Finite (⋃ (i : ι), f i)
haveI := fun i => (H i).fintype
no goals
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : Finite ι
f : ι → Set α
H : ∀ (i : ι), Set.Finite (f i)
this : (i : ι) → Fintype ↑(f i)
⊢ Set.Finite (⋃ (i : ι), f i)
apply toFinite