case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
δ : Type u_1
inst✝ : Finite δ
κ : δ → Type u_2
t : (d : δ) → Set (κ d)
ht : ∀ (d : δ), Set.Finite (t d)
val✝ : Fintype δ
⊢ Set.Finite (Set.pi univ t)
α : Type u
β : Type v
ι : Sort w
γ : Type x
δ : Type u_1
inst✝ : Finite δ
κ : δ → Type u_2
t : (d : δ) → Set (κ d)
ht : ∀ (d : δ), Set.Finite (t d)
⊢ Set.Finite (Set.pi univ t)
cases _root_.nonempty_fintype δ
case intro.intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
δ : Type u_1
inst✝ : Finite δ
κ : δ → Type u_2
val✝ : Fintype δ
t : (i : δ) → Finset (κ i)
⊢ Set.Finite (Set.pi univ fun i => ↑(t i))
case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
δ : Type u_1
inst✝ : Finite δ
κ : δ → Type u_2
t : (d : δ) → Set (κ d)
ht : ∀ (d : δ), Set.Finite (t d)
val✝ : Fintype δ
⊢ Set.Finite (Set.pi univ t)
lift t to ∀ d, Finset (κ d) using ht
no goals
case intro.intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
δ : Type u_1
inst✝ : Finite δ
κ : δ → Type u_2
val✝ : Fintype δ
t : (i : δ) → Finset (κ i)
⊢ Set.Finite (Set.pi univ fun i => ↑(t i))
classical
  rw [← Fintype.coe_piFinset]
  apply Finset.finite_toSet
case intro.intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
δ : Type u_1
inst✝ : Finite δ
κ : δ → Type u_2
val✝ : Fintype δ
t : (i : δ) → Finset (κ i)
⊢ Set.Finite ↑(Fintype.piFinset fun i => t i)
case intro.intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
δ : Type u_1
inst✝ : Finite δ
κ : δ → Type u_2
val✝ : Fintype δ
t : (i : δ) → Finset (κ i)
⊢ Set.Finite (Set.pi univ fun i => ↑(t i))
rw [← Fintype.coe_piFinset]
no goals
case intro.intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
δ : Type u_1
inst✝ : Finite δ
κ : δ → Type u_2
val✝ : Fintype δ
t : (i : δ) → Finset (κ i)
⊢ Set.Finite ↑(Fintype.piFinset fun i => t i)
apply Finset.finite_toSet