∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (α : Type w)
  [inst_1 : CategoryTheory.Limits.HasFiniteProducts C] {X Y : CategoryTheory.Functor (CategoryTheory.Discrete α) C}
  (β : X ⟶ Y) (x : (Finset (CategoryTheory.Discrete α))ᵒᵖ),
  ((CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset C α).map β).app x =
    CategoryTheory.Limits.Pi.map fun x_1 => β.app ↑x_1