∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} (f : ι → Type u_2) (g : (i : ι) → f i → C)
  [inst_1 : ∀ (i : ι), CategoryTheory.Limits.HasProduct (g i)]
  [inst_2 : CategoryTheory.Limits.HasProduct fun i => ∏ᶜ g i],
  (CategoryTheory.Limits.piPiIso f g).hom =
    CategoryTheory.Limits.Pi.lift fun x =>
      match x with
      | ⟨i, x⟩ =>
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun i => ∏ᶜ g i) i)
          (CategoryTheory.Limits.Pi.π (g i) x)