case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
t : Set β
ht : Set.Finite t
a✝ : Fintype ↑s
⊢ Set.Finite (s ×ˢ t)
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
t : Set β
hs : Set.Finite s
ht : Set.Finite t
⊢ Set.Finite (s ×ˢ t)
cases hs
case intro.intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
t : Set β
a✝¹ : Fintype ↑s
a✝ : Fintype ↑t
⊢ Set.Finite (s ×ˢ t)
case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
t : Set β
ht : Set.Finite t
a✝ : Fintype ↑s
⊢ Set.Finite (s ×ˢ t)
cases ht
no goals
case intro.intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
t : Set β
a✝¹ : Fintype ↑s
a✝ : Fintype ↑t
⊢ Set.Finite (s ×ˢ t)
apply toFinite