case intro
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : Set ι
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (hi : i ∈ s), Set.Finite (t i hi)
a✝ : Fintype ↑s
⊢ Set.Finite (⋃ (i : ι) (h : i ∈ s), t i h)
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : Set ι
hs : Set.Finite s
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (hi : i ∈ s), Set.Finite (t i hi)
⊢ Set.Finite (⋃ (i : ι) (h : i ∈ s), t i h)
cases hs
case intro
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : Set ι
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (hi : i ∈ s), Set.Finite (t i hi)
a✝ : Fintype ↑s
⊢ Set.Finite (⋃ (x : ↑s), t ↑x (_ : ↑x ∈ s))
case intro
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : Set ι
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (hi : i ∈ s), Set.Finite (t i hi)
a✝ : Fintype ↑s
⊢ Set.Finite (⋃ (i : ι) (h : i ∈ s), t i h)
rw [biUnion_eq_iUnion]
no goals
case intro
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : Set ι
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (hi : i ∈ s), Set.Finite (t i hi)
a✝ : Fintype ↑s
⊢ Set.Finite (⋃ (x : ↑s), t ↑x (_ : ↑x ∈ s))
apply finite_iUnion fun i : s => ht i.1 i.2