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