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