no goals
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : Set ι
hs : Set.Finite s
t : ι → Set α
ht : ∀ (i : ι), i ∈ s → Set.Finite (t i)
⊢ Set.Finite (⋃ (i : ι) (_ : i ∈ s), t i)
classical
  cases hs
  haveI := fintypeBiUnion s t fun i hi => (ht i hi).fintype
  apply toFinite
case intro
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : Set ι
t : ι → Set α
ht : ∀ (i : ι), i ∈ s → Set.Finite (t i)
a✝ : Fintype ↑s
⊢ Set.Finite (⋃ (i : ι) (_ : i ∈ s), t i)
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : Set ι
hs : Set.Finite s
t : ι → Set α
ht : ∀ (i : ι), i ∈ s → Set.Finite (t i)
⊢ Set.Finite (⋃ (i : ι) (_ : i ∈ s), t i)
cases hs
case intro
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : Set ι
t : ι → Set α
ht : ∀ (i : ι), i ∈ s → Set.Finite (t i)
a✝ : Fintype ↑s
this : Fintype ↑(⋃ (x : ι) (_ : x ∈ s), t x)
⊢ Set.Finite (⋃ (i : ι) (_ : i ∈ s), t i)
case intro
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : Set ι
t : ι → Set α
ht : ∀ (i : ι), i ∈ s → Set.Finite (t i)
a✝ : Fintype ↑s
⊢ Set.Finite (⋃ (i : ι) (_ : i ∈ s), t i)
haveI := fintypeBiUnion s t fun i hi => (ht i hi).fintype
no goals
case intro
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : Set ι
t : ι → Set α
ht : ∀ (i : ι), i ∈ s → Set.Finite (t i)
a✝ : Fintype ↑s
this : Fintype ↑(⋃ (x : ι) (_ : x ∈ s), t x)
⊢ Set.Finite (⋃ (i : ι) (_ : i ∈ s), t i)
apply toFinite