-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
α : Type u
I : α → Type u
inst : (i : α) → SmallCategory (I i)
inst_1 : ∀ (i : α), IsFiltered.{u, u} (I i)
F : (i : α) → I i ⥤ Type u
ky : (i : α) → I i
yk₀ : (pointwiseProduct (I := I) F).obj ky
ky' : (i : α) → I i
yk₀' : (pointwiseProduct (I := I) F).obj ky'
k : (i : α) → I i := IsFiltered.max ky ky'
yk : ∏ᶜ (Functor.pi (C := I) (D := fun (i : α) ↦ Type u) F).obj k :=
  (hom (FC := TypeCat.Fun) ((pointwiseProduct (I := I) F).map (IsFiltered.leftToMax ky ky')) :
      (a : (fun (X : Type u) ↦ X) ((pointwiseProduct F).obj ky)) →
        (fun (X : Type u) ↦ X) ((pointwiseProduct F).obj (IsFiltered.max ky ky')))
    yk₀
yk' : ∏ᶜ (Functor.pi (C := I) (D := fun (i : α) ↦ Type u) F).obj k :=
  (hom (FC := TypeCat.Fun) ((pointwiseProduct (I := I) F).map (IsFiltered.rightToMax ky ky')) :
      (a : (fun (X : Type u) ↦ X) ((pointwiseProduct F).obj ky')) →
        (fun (X : Type u) ↦ X) ((pointwiseProduct F).obj (IsFiltered.max ky ky')))
    yk₀'
hyk₀ :
  Eq (α := (fun (X : Type u) ↦ X) (colimit (pointwiseProduct (I := I) F)))
    ((hom (FC := TypeCat.Fun) (colimit.ι (pointwiseProduct (I := I) F) ky) :
          (a : (fun (X : Type u) ↦ X) ((pointwiseProduct F).obj ky)) →
            (fun (X : Type u) ↦ X) (colimit (pointwiseProduct F)))
        yk₀ :
      (fun (X : Type u) ↦ X) (colimit (pointwiseProduct (I := I) F)))
    ((hom (FC := TypeCat.Fun) (colimit.ι (pointwiseProduct (I := I) F) k) :
          (a : (fun (X : Type u) ↦ X) ((pointwiseProduct F).obj k)) →
            (fun (X : Type u) ↦ X) (colimit (pointwiseProduct F)))
        yk :
      (fun (X : Type u) ↦ X) (colimit (pointwiseProduct (I := I) F)))
hyk₀' :
  Eq (α := (fun (X : Type u) ↦ X) (colimit (pointwiseProduct (I := I) F)))
    ((hom (FC := TypeCat.Fun) (colimit.ι (pointwiseProduct (I := I) F) ky') :
          (a : (fun (X : Type u) ↦ X) ((pointwiseProduct F).obj ky')) →
            (fun (X : Type u) ↦ X) (colimit (pointwiseProduct F)))
        yk₀' :
      (fun (X : Type u) ↦ X) (colimit (pointwiseProduct (I := I) F)))
    ((hom (FC := TypeCat.Fun) (colimit.ι (pointwiseProduct (I := I) F) k) :
          (a : (fun (X : Type u) ↦ X) ((pointwiseProduct F).obj k)) →
            (fun (X : Type u) ↦ X) (colimit (pointwiseProduct F)))
        yk' :
      (fun (X : Type u) ↦ X) (colimit (pointwiseProduct (I := I) F)))
hy :
  Eq (α := ∏ᶜ fun (s : α) ↦ colimit (F s))
    ((hom (FC := TypeCat.Fun) (colimitPointwiseProductToProductColimit (I := I) F) :
          (a : colimit (pointwiseProduct F)) → ∏ᶜ fun (s : α) ↦ colimit (F s))
        ((hom (FC := TypeCat.Fun) (colimit.ι (pointwiseProduct (I := I) F) k) :
              (a : ∏ᶜ (Functor.pi F).obj k) → colimit (pointwiseProduct F))
            yk :
          colimit (pointwiseProduct (I := I) F)) :
      ∏ᶜ fun (s : α) ↦ colimit (F s))
    ((hom (FC := TypeCat.Fun) (colimitPointwiseProductToProductColimit (I := I) F) :
          (a : colimit (pointwiseProduct F)) → ∏ᶜ fun (s : α) ↦ colimit (F s))
        ((hom (FC := TypeCat.Fun) (colimit.ι (pointwiseProduct (I := I) F) k) :
              (a : ∏ᶜ (Functor.pi F).obj k) → colimit (pointwiseProduct F))
            yk' :
          colimit (pointwiseProduct (I := I) F)) :
      ∏ᶜ fun (s : α) ↦ colimit (F s))
s : α
hy₁ :
  Eq (α := colimit (F s))
    ((hom (FC := TypeCat.Fun) (Pi.π (fun (s : α) ↦ colimit (F s)) s) :
          (a : ∏ᶜ fun (s : α) ↦ colimit (F s)) → colimit (F s))
        ((hom (FC := TypeCat.Fun) (colimitPointwiseProductToProductColimit (I := I) F) :
              (a : colimit (pointwiseProduct F)) → ∏ᶜ fun (s : α) ↦ colimit (F s))
            ((hom (FC := TypeCat.Fun) (colimit.ι (pointwiseProduct (I := I) F) k) :
                  (a : ∏ᶜ (Functor.pi F).obj k) → colimit (pointwiseProduct F))
                yk :
              colimit (pointwiseProduct (I := I) F)) :
          ∏ᶜ fun (s : α) ↦ colimit (F s)) :
      colimit (F s))
    ((hom (FC := TypeCat.Fun) (colimit.ι (F s) (k s)) : (a : (F s).obj (k s)) → colimit (F s))
        ((hom (FC := TypeCat.Fun) (Pi.π ((Functor.pi (C := I) (D := fun (i : α) ↦ Type u) F).obj k) s) :
              (a : ∏ᶜ (Functor.pi F).obj k) → (F s).obj (k s))
            yk :
          (F s).obj (k s)) :
      colimit (F s))
i₀ : I s
f₀ g₀ : k s ⟶ i₀
h₀ :
  Eq (α := (fun (X : Type u) ↦ X) ((F s).obj i₀))
    ((hom (FC := TypeCat.Fun) ((F s).map f₀) :
          (a : (fun (X : Type u) ↦ X) ((F s).obj (k s))) → (fun (X : Type u) ↦ X) ((F s).obj i₀))
        ((hom (FC := TypeCat.Fun) (Pi.π ((Functor.pi (C := I) (D := fun (i : α) ↦ Type u) F).obj k) s) :
            (a : ∏ᶜ (Functor.pi F).obj k) → (F s).obj (k s))
          yk) :
      (fun (X : Type u) ↦ X) ((F s).obj i₀))
    ((hom (FC := TypeCat.Fun) ((F s).map g₀) :
          (a : (fun (X : Type u) ↦ X) ((F s).obj (k s))) → (fun (X : Type u) ↦ X) ((F s).obj i₀))
        ((hom (FC := TypeCat.Fun) (Pi.π ((Functor.pi (C := I) (D := fun (i : α) ↦ Type u) F).obj k) s) :
            (a : ∏ᶜ (Functor.pi F).obj k) → (F s).obj (k s))
          yk') :
      (fun (X : Type u) ↦ X) ((F s).obj i₀))
refine :
  Eq (α := (fun (X : Type u) ↦ X) ((F s).obj (IsFiltered.coeq f₀ g₀)))
    ((hom (FC := TypeCat.Fun) ((F s).map (f₀ ≫ IsFiltered.coeqHom f₀ g₀)) :
          (a : (fun (X : Type u) ↦ X) ((F s).obj (k s))) → (fun (X : Type u) ↦ X) ((F s).obj (IsFiltered.coeq f₀ g₀)))
        ((hom (FC := TypeCat.Fun) (Pi.π (fun (s : α) ↦ (F s).obj (k s)) s) :
            (a : (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ (F s).obj (k s))) → (fun (X : Type u) ↦ X) ((F s).obj (k s)))
          yk) :
      (fun (X : Type u) ↦ X) ((F s).obj (IsFiltered.coeq f₀ g₀)))
    ((hom (FC := TypeCat.Fun) ((F s).map (f₀ ≫ IsFiltered.coeqHom f₀ g₀)) :
          (a : (fun (X : Type u) ↦ X) ((F s).obj (k s))) → (fun (X : Type u) ↦ X) ((F s).obj (IsFiltered.coeq f₀ g₀)))
        ((hom (FC := TypeCat.Fun) (Pi.π (fun (s : α) ↦ (F s).obj (k s)) s) :
            (a : (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ (F s).obj (k s))) → (fun (X : Type u) ↦ X) ((F s).obj (k s)))
          yk') :
      (fun (X : Type u) ↦ X) ((F s).obj (IsFiltered.coeq f₀ g₀)))
⊢ ∃ (i' : I s) (hi' : k s ⟶ i'),
    Eq (α := (fun (X : Type u) ↦ X) ((F s).obj i'))
      ((hom (FC := TypeCat.Fun) ((F s).map hi') :
            (a : (fun (X : Type u) ↦ X) ((F s).obj (k s))) → (fun (X : Type u) ↦ X) ((F s).obj i'))
          ((hom (FC := TypeCat.Fun) (Pi.π (fun (s : α) ↦ (F s).obj (k s)) s) :
              (a : (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ (F s).obj (k s))) →
                (fun (X : Type u) ↦ X) ((F s).obj (k s)))
            yk) :
        (fun (X : Type u) ↦ X) ((F s).obj i'))
      ((hom (FC := TypeCat.Fun) ((F s).map hi') :
            (a : (fun (X : Type u) ↦ X) ((F s).obj (k s))) → (fun (X : Type u) ↦ X) ((F s).obj i'))
          ((hom (FC := TypeCat.Fun) (Pi.π (fun (s : α) ↦ (F s).obj (k s)) s) :
              (a : (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ (F s).obj (k s))) →
                (fun (X : Type u) ↦ X) ((F s).obj (k s)))
            yk') :
        (fun (X : Type u) ↦ X) ((F s).obj i'))

Tactic:
refine ⟨IsFiltered.coeq f₀ g₀, f₀ ≫ IsFiltered.coeqHom f₀ g₀, ?_⟩