α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : Set ι
inst✝ : Finite ↑s
t : ι → Set α
H : ∀ (i : ι), i ∈ s → Finite ↑(t i)
⊢ Finite ↑(⋃ (x : ↑s), t ↑x)
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : Set ι
inst✝ : Finite ↑s
t : ι → Set α
H : ∀ (i : ι), i ∈ s → Finite ↑(t i)
⊢ Finite ↑(⋃ (x : ι) (_ : x ∈ s), t x)
rw [biUnion_eq_iUnion]
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : Set ι
inst✝ : Finite ↑s
t : ι → Set α
H : ∀ (i : ι), i ∈ s → Finite ↑(t i)
this : ∀ (i : ↑s), Finite ↑(t ↑i)
⊢ Finite ↑(⋃ (x : ↑s), t ↑x)
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : Set ι
inst✝ : Finite ↑s
t : ι → Set α
H : ∀ (i : ι), i ∈ s → Finite ↑(t i)
⊢ Finite ↑(⋃ (x : ↑s), t ↑x)
haveI : ∀ i : s, Finite (t i) := fun i => H i i.property
no goals
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : Set ι
inst✝ : Finite ↑s
t : ι → Set α
H : ∀ (i : ι), i ∈ s → Finite ↑(t i)
this : ∀ (i : ↑s), Finite ↑(t ↑i)
⊢ Finite ↑(⋃ (x : ↑s), t ↑x)
infer_instance