∀ {ι : Type v} (α : ι → TopCat) (i : ι) (x : ↑(∏ᶜ α)),
  (CategoryTheory.ConcreteCategory.hom (TopCat.piIsoPi α).hom) x i =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π α i)) x