awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
Goal:
J : Type u₁
K : Type u₂
inst : SmallCategory J
inst_1 : Category.{v₂, u₂} K
inst_2 : Small.{v, u₂} K
inst_3 : FinCategory J
F : J × K ⥤ Type v
inst_4 : IsFiltered.{v₂, u₂} K
C : Type u
inst_5 : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_6 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_7 : ConcreteCategory C FC (CC := CC)
inst_8 : PreservesFiniteLimits (forget C (FC := FC) (CC := CC))
inst_9 : PreservesColimitsOfShape.{v₂, u₂, v, v, u, v + 1} K (forget C (FC := FC) (CC := CC))
inst_10 : HasFiniteLimits.{v, u} C
inst_11 : HasColimitsOfShape.{v₂, u₂, v, u} K C
inst_12 : ReflectsIsomorphisms (forget C (FC := FC) (CC := CC))
h :
  ∀ (J : Type v) {𝒥 : SmallCategory J} (x : FinCategory J),
    PreservesLimitsOfShape (C := Functor.{v₂, v, u₂, u} K C) J colim
⊢ PreservesFiniteLimits (C := Functor.{v₂, v, u₂, u} K C) colim

Tactic:
apply preservesFiniteLimits_of_preservesFiniteLimitsOfSize.{v}
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
Goal:
J_1 : Type u₁
K : Type u₂
inst : SmallCategory J_1
inst_1 : Category.{v₂, u₂} K
inst_2 : Small.{v, u₂} K
inst_3 : FinCategory J_1
F : J_1 × K ⥤ Type v
inst_4 : IsFiltered.{v₂, u₂} K
C : Type u
inst_5 : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_6 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_7 : ConcreteCategory C FC (CC := CC)
inst_8 : PreservesFiniteLimits (forget C (FC := FC) (CC := CC))
inst_9 : PreservesColimitsOfShape.{v₂, u₂, v, v, u, v + 1} K (forget C (FC := FC) (CC := CC))
inst_10 : HasFiniteLimits.{v, u} C
inst_11 : HasColimitsOfShape.{v₂, u₂, v, u} K C
inst_12 : ReflectsIsomorphisms (forget C (FC := FC) (CC := CC))
J : Type v
h : ∀ {𝒥 : SmallCategory J} (x : FinCategory J), PreservesLimitsOfShape (C := Functor.{v₂, v, u₂, u} K C) J colim
⊢ ∀ {𝒥 : SmallCategory J} (x : FinCategory J), PreservesLimitsOfShape (C := Functor.{v₂, v, u₂, u} K C) J colim

Tactic:
_
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
Goal:
J_1 : Type u₁
K : Type u₂
inst : SmallCategory J_1
inst_1 : Category.{v₂, u₂} K
inst_2 : Small.{v, u₂} K
inst_3 : FinCategory J_1
F : J_1 × K ⥤ Type v
inst_4 : IsFiltered.{v₂, u₂} K
C : Type u
inst_5 : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_6 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_7 : ConcreteCategory C FC (CC := CC)
inst_8 : PreservesFiniteLimits (forget C (FC := FC) (CC := CC))
inst_9 : PreservesColimitsOfShape.{v₂, u₂, v, v, u, v + 1} K (forget C (FC := FC) (CC := CC))
inst_10 : HasFiniteLimits.{v, u} C
inst_11 : HasColimitsOfShape.{v₂, u₂, v, u} K C
inst_12 : ReflectsIsomorphisms (forget C (FC := FC) (CC := CC))
J : Type v
𝒥 : SmallCategory J
h : ∀ (x : FinCategory J), PreservesLimitsOfShape (C := Functor.{v₂, v, u₂, u} K C) J colim
⊢ ∀ (x : FinCategory J), PreservesLimitsOfShape (C := Functor.{v₂, v, u₂, u} K C) J colim

Tactic:
_
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
Goal:
J_1 : Type u₁
K : Type u₂
inst : SmallCategory J_1
inst_1 : Category.{v₂, u₂} K
inst_2 : Small.{v, u₂} K
inst_3 : FinCategory J_1
F : J_1 × K ⥤ Type v
inst_4 : IsFiltered.{v₂, u₂} K
C : Type u
inst_5 : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_6 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_7 : ConcreteCategory C FC (CC := CC)
inst_8 : PreservesFiniteLimits (forget C (FC := FC) (CC := CC))
inst_9 : PreservesColimitsOfShape.{v₂, u₂, v, v, u, v + 1} K (forget C (FC := FC) (CC := CC))
inst_10 : HasFiniteLimits.{v, u} C
inst_11 : HasColimitsOfShape.{v₂, u₂, v, u} K C
inst_12 : ReflectsIsomorphisms (forget C (FC := FC) (CC := CC))
J : Type v
𝒥 : SmallCategory J
x : FinCategory J
⊢ PreservesLimitsOfShape (C := Functor.{v₂, v, u₂, u} K C) J colim

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u₁
inst_1 : Category.{v₁, u₁} J
K : Type u₂
inst_2 : Category.{v₂, u₂} K
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} J C
inst_4 : HasColimitsOfShape.{v₂, u₂, v, u} K C
inst_5 : PreservesLimitsOfShape (C := Functor.{v₂, v, u₂, u} K C) J colim
F : J ⥤ Functor.{v₂, v, u₂, u} K C
a : K
b : J
⊢ CategoryStruct.comp (Y := colimit (limit F)) (colimit.ι (limit F) a : (limit F).obj a ⟶ colimit (limit F))
      (CategoryStruct.comp (Y := limit (colimit F.flip))
          (Iso.hom (colimitLimitIso F) : colimit (limit F) ⟶ limit (colimit F.flip))
          (limit.π (colimit F.flip) b : limit (colimit F.flip) ⟶ (colimit F.flip).obj b) :
        colimit (limit F) ⟶ (colimit F.flip).obj b) =
    NatTrans.app (limit.π F b) a ≫ NatTrans.app (colimit.ι F.flip a) b

Tactic:
simp [colimitLimitIso]

Premises used: CategoryTheory.Limits.colimitLimitIso
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
C : Type u
inst : Category.{v, u} C
α : Type u_1
I : α → Type u_2
inst_1 : (i : α) → Category.{v_1, u_2} (I i)
inst_2 : HasProductsOfShape.{u_1, u, v} α C
F : (i : α) → Functor.{v_1, v, u_2, u} (I i) C
c c' : (i : α) → Cocone (F i)
e : (i : α) → c i ≅ c' i
i : (i : α) → I i
dsimp :
  Eq.{v + 1} (α :=
    piObj.{u_1, v, u} ((Functor.pi (C := I) (D := fun (i : α) ↦ C) F).obj i) ⟶
      piObj.{u_1, v, u} fun (i : α) ↦ (c' i).pt)
    (CategoryStruct.comp (Y := piObj.{u_1, v, u} fun (i : α) ↦ (c i).pt)
        (CategoryStruct.comp (Y :=
            piObj.{u_1, v, u}
              (Functor.obj
                (Functor.pi (C := I) (D := fun (i : α) ↦ C) fun (i : α) ↦ Functor.obj (Functor.const (I i)) (c i).pt)
                i))
            (Pi.map (NatTrans.app (NatTrans.pi (C := I) (D := fun (i : α) ↦ C) fun (i : α) ↦ (c i).ι) i))
            (𝟙 (piObj.{u_1, v, u} fun (i : α) ↦ (c i).pt)) :
          piObj.{u_1, v, u} ((Functor.pi (C := I) (D := fun (i : α) ↦ C) F).obj i) ⟶
            piObj.{u_1, v, u} fun (i : α) ↦ (c i).pt)
        (Iso.hom (Pi.mapIso fun (i : α) ↦ (Cocone.forget (F i)).mapIso (e i)) :
          Quiver.Hom.{v, u} (V := C) (piObj.{u_1, v, u} fun (i : α) ↦ (c i).pt)
            (piObj.{u_1, v, u} fun (i : α) ↦ (c' i).pt)) :
      piObj.{u_1, v, u} ((Functor.pi (C := I) (D := fun (i : α) ↦ C) F).obj i) ⟶
        piObj.{u_1, v, u} fun (i : α) ↦ (c' i).pt)
    (CategoryStruct.comp (Y :=
        piObj.{u_1, v, u}
          (Functor.obj
            (Functor.pi (C := I) (D := fun (i : α) ↦ C) fun (i : α) ↦ Functor.obj (Functor.const (I i)) (c' i).pt) i))
        (Pi.map (NatTrans.app (NatTrans.pi (C := I) (D := fun (i : α) ↦ C) fun (i : α) ↦ (c' i).ι) i))
        (𝟙 (piObj.{u_1, v, u} fun (i : α) ↦ (c' i).pt)) :
      piObj.{u_1, v, u} ((Functor.pi (C := I) (D := fun (i : α) ↦ C) F).obj i) ⟶
        piObj.{u_1, v, u} fun (i : α) ↦ (c' i).pt)
⊢ Eq (α :=
    (pointwiseProduct (I := I) F).obj i ⟶
      Cocone.pt (F := pointwiseProduct (I := I) F) (coconePointwiseProduct (I := I) c'))
    (CategoryStruct.comp (Y := Cocone.pt (F := pointwiseProduct (I := I) F) (coconePointwiseProduct (I := I) c))
        (NatTrans.app (Cocone.ι (coconePointwiseProduct (I := I) c)) i :
          (pointwiseProduct (I := I) F).obj i ⟶
            Functor.obj
              (Functor.obj (Functor.const ((i : α) → I i))
                (Cocone.pt (F := pointwiseProduct (I := I) F) (coconePointwiseProduct (I := I) c)))
              i)
        (Iso.hom (Pi.mapIso fun (i : α) ↦ (Cocone.forget (F i)).mapIso (e i))) :
      (pointwiseProduct (I := I) F).obj i ⟶
        Cocone.pt (F := pointwiseProduct (I := I) F) (coconePointwiseProduct (I := I) c'))
    (NatTrans.app (Cocone.ι (coconePointwiseProduct (I := I) c')) i :
      (pointwiseProduct (I := I) F).obj i ⟶
        Functor.obj
          (Functor.obj (Functor.const ((i : α) → I i))
            (Cocone.pt (F := pointwiseProduct (I := I) F) (coconePointwiseProduct (I := I) c')))
          i)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
C : Type u
inst : Category.{v, u} C
α : Type u_1
I : α → Type u_2
inst_1 : (i : α) → Category.{v_1, u_2} (I i)
inst_2 : HasProductsOfShape.{u_1, u, v} α C
F : (i : α) → Functor.{v_1, v, u_2, u} (I i) C
c c' : (i : α) → Cocone (F i)
e : (i : α) → c i ≅ c' i
i : (i : α) → I i
b : α
⊢ Eq.{v + 1} (α := piObj.{u_1, v, u} ((Functor.pi (C := I) (D := fun (i : α) ↦ C) F).obj i) ⟶ (c' b).pt)
    (CategoryStruct.comp (Y := piObj.{u_1, v, u} fun (i : α) ↦ (c' i).pt)
        (CategoryStruct.comp (Y := piObj.{u_1, v, u} fun (i : α) ↦ (c i).pt)
            (CategoryStruct.comp (Y :=
                piObj.{u_1, v, u}
                  (Functor.obj
                    (Functor.pi (C := I) (D := fun (i : α) ↦ C) fun (i : α) ↦
                      Functor.obj (Functor.const (I i)) (c i).pt)
                    i))
                (Pi.map (NatTrans.app (NatTrans.pi (C := I) (D := fun (i : α) ↦ C) fun (i : α) ↦ (c i).ι) i))
                (𝟙 (piObj.{u_1, v, u} fun (i : α) ↦ (c i).pt)) :
              piObj.{u_1, v, u} ((Functor.pi (C := I) (D := fun (i : α) ↦ C) F).obj i) ⟶
                piObj.{u_1, v, u} fun (i : α) ↦ (c i).pt)
            (Iso.hom (Pi.mapIso fun (i : α) ↦ (Cocone.forget (F i)).mapIso (e i)) :
              Quiver.Hom.{v, u} (V := C) (piObj.{u_1, v, u} fun (i : α) ↦ (c i).pt)
                (piObj.{u_1, v, u} fun (i : α) ↦ (c' i).pt)) :
          piObj.{u_1, v, u} ((Functor.pi (C := I) (D := fun (i : α) ↦ C) F).obj i) ⟶
            piObj.{u_1, v, u} fun (i : α) ↦ (c' i).pt)
        (Pi.π (fun (i : α) ↦ (c' i).pt) b : (piObj.{u_1, v, u} fun (i : α) ↦ (c' i).pt) ⟶ (c' b).pt) :
      piObj.{u_1, v, u} ((Functor.pi (C := I) (D := fun (i : α) ↦ C) F).obj i) ⟶ (c' b).pt)
    (CategoryStruct.comp (Y := piObj.{u_1, v, u} fun (i : α) ↦ (c' i).pt)
        (CategoryStruct.comp (Y :=
            piObj.{u_1, v, u}
              (Functor.obj
                (Functor.pi (C := I) (D := fun (i : α) ↦ C) fun (i : α) ↦ Functor.obj (Functor.const (I i)) (c' i).pt)
                i))
            (Pi.map (NatTrans.app (NatTrans.pi (C := I) (D := fun (i : α) ↦ C) fun (i : α) ↦ (c' i).ι) i))
            (𝟙 (piObj.{u_1, v, u} fun (i : α) ↦ (c' i).pt)) :
          piObj.{u_1, v, u} ((Functor.pi (C := I) (D := fun (i : α) ↦ C) F).obj i) ⟶
            piObj.{u_1, v, u} fun (i : α) ↦ (c' i).pt)
        (Pi.π (fun (i : α) ↦ (c' i).pt) b : (piObj.{u_1, v, u} fun (i : α) ↦ (c' i).pt) ⟶ (c' b).pt) :
      piObj.{u_1, v, u} ((Functor.pi (C := I) (D := fun (i : α) ↦ C) F).obj i) ⟶ (c' b).pt)

Tactic:
simp [Functor.pi]

Premises used: CategoryTheory.Functor.pi
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
C : Type u
inst : Category.{v, u} C
α : Type u_1
I : α → Type u_2
inst_1 : (i : α) → Category.{v_1, u_2} (I i)
inst_2 : HasProductsOfShape.{u_1, u, v} α C
F : (i : α) → Functor.{v_1, v, u_2, u} (I i) C
inst_3 : ∀ (i : α), HasColimit (F i)
inst_4 : HasColimit (pointwiseProduct (I := I) F)
k : (i : α) → I i
s : α
⊢ Eq (α := (pointwiseProduct (I := I) F).obj k ⟶ colimit (F s))
    (CategoryStruct.comp (Y := colimit (pointwiseProduct (I := I) F)) (colimit.ι (pointwiseProduct (I := I) F) k)
      (colimitPointwiseProductToProductColimit (I := I) F ≫ Pi.π (fun (s : α) ↦ colimit (F s)) s))
    (Pi.π ((Functor.pi (C := I) (D := fun (i : α) ↦ C) F).obj k) s ≫ colimit.ι (F s) (k s))

Tactic:
simp [colimitPointwiseProductToProductColimit, Functor.pi, Pi.functor]

Premises used: CategoryTheory.Limits.Pi.functor, CategoryTheory.Limits.colimitPointwiseProductToProductColimit, CategoryTheory.Functor.pi
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
α : Type u_3
I : α → Type u_4
inst_2 : (i : α) → Category.{u_5, u_4} (I i)
inst_3 : HasLimitsOfShape.{u_3, u_3, v_1, u_1} (Discrete α) C
F : (i : α) → I i ⥤ Functor.{v_2, v_1, u_2, u_1} D C
d : D
X Y : (i : α) → I i
f : X ⟶ Y
⊢ ∀ (b : α),
    Eq (α :=
      (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) d).obj X ⟶
        Functor.obj (Functor.pi (C := I) (D := fun (i : α) ↦ C) fun (s : α) ↦ F s ⋙ Functor.obj (evaluation D C) d) Y b)
      (CategoryStruct.comp (Y :=
        piObj.{u_3, v_1, u_1}
          (Functor.obj (Functor.pi (C := I) (D := fun (i : α) ↦ C) fun (s : α) ↦ F s ⋙ Functor.obj (evaluation D C) d)
            Y))
        ((pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) d).map f ≫
          Iso.hom
            ((fun (k : (i : α) → I i) ↦
                (piObjIso ((Functor.pi (C := I) (D := fun (i : α) ↦ Functor.{v_2, v_1, u_2, u_1} D C) F).obj k) d :
                  (∏ᶜ (Functor.pi (C := I) (D := fun (i : α) ↦ Functor.{v_2, v_1, u_2, u_1} D C) F).obj k).obj d ≅
                    piObj.{u_3, v_1, u_1} fun (s : α) ↦
                      ((Functor.pi (C := I) (D := fun (i : α) ↦ Functor.{v_2, v_1, u_2, u_1} D C) F).obj k s).obj d))
              Y))
        (Pi.π
          (Functor.obj (Functor.pi (C := I) (D := fun (i : α) ↦ C) fun (s : α) ↦ F s ⋙ Functor.obj (evaluation D C) d)
            Y)
          b))
      (CategoryStruct.comp (Y :=
        piObj.{u_3, v_1, u_1}
          (Functor.obj (Functor.pi (C := I) (D := fun (i : α) ↦ C) fun (s : α) ↦ F s ⋙ Functor.obj (evaluation D C) d)
            Y))
        (Iso.hom
              ((fun (k : (i : α) → I i) ↦
                  (piObjIso ((Functor.pi (C := I) (D := fun (i : α) ↦ Functor.{v_2, v_1, u_2, u_1} D C) F).obj k) d :
                    (∏ᶜ (Functor.pi (C := I) (D := fun (i : α) ↦ Functor.{v_2, v_1, u_2, u_1} D C) F).obj k).obj d ≅
                      piObj.{u_3, v_1, u_1} fun (s : α) ↦
                        ((Functor.pi (C := I) (D := fun (i : α) ↦ Functor.{v_2, v_1, u_2, u_1} D C) F).obj k s).obj d))
                X) ≫
            Functor.map (pointwiseProduct (I := I) fun (s : α) ↦ F s ⋙ Functor.obj (evaluation D C) d) f :
          (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) d).obj X ⟶
            Functor.obj (pointwiseProduct (I := I) fun (s : α) ↦ F s ⋙ Functor.obj (evaluation D C) d) Y)
        (Pi.π
          (Functor.obj (Functor.pi (C := I) (D := fun (i : α) ↦ C) fun (s : α) ↦ F s ⋙ Functor.obj (evaluation D C) d)
            Y)
          b))

Tactic:
simp [Functor.pi, ← NatTrans.comp_app]

Premises used: CategoryTheory.NatTrans.comp_app, CategoryTheory.Functor.pi
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
α : Type u_3
I : α → Type u_4
inst_2 : (i : α) → Category.{u_5, u_4} (I i)
inst_3 : HasLimitsOfShape.{u_3, u_3, v_1, u_1} (Discrete α) C
F : (i : α) → I i ⥤ Functor.{v_2, v_1, u_2, u_1} D C
inst_4 : ∀ (i : α), HasColimitsOfShape.{u_5, u_4, v_1, u_1} (I i) C
inst_5 : HasColimitsOfShape ((i : α) → I i) C
d : D
⊢ Eq (α :=
    colimit (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) d) ⟶
      piObj.{u_3, v_1, u_1} fun (x : α) ↦ (colimit (F x)).obj d)
    (CategoryStruct.comp (Y := (colimit (pointwiseProduct (I := I) F)).obj d)
          (Iso.inv (colimitObjIsoColimitCompEvaluation (pointwiseProduct (I := I) F) d) :
            colimit (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) d) ⟶
              (colimit (pointwiseProduct (I := I) F)).obj d)
          (NatTrans.app (colimitPointwiseProductToProductColimit (I := I) F) d :
            (colimit (pointwiseProduct (I := I) F)).obj d ⟶
              Functor.obj.{v_2, v_1, u_2, u_1} (∏ᶜ fun (s : α) ↦ colimit (F s)) d) ≫
        Iso.hom (piObjIso (fun (x : α) ↦ colimit (F x)) d) :
      colimit (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) d) ⟶
        piObj.{u_3, v_1, u_1} fun (x : α) ↦ (colimit (F x)).obj d)
    (CategoryStruct.comp (Y := piObj.{u_3, v_1, u_1} fun (s : α) ↦ colimit (F s ⋙ Functor.obj (evaluation D C) d))
        (CategoryStruct.comp (Y :=
            colimit (J := (i : α) → I i) (pointwiseProduct (I := I) fun (s : α) ↦ F s ⋙ Functor.obj (evaluation D C) d))
            (Iso.hom (HasColimit.isoOfNatIso (pointwiseProductCompEvaluation (I := I) F d)))
            (colimitPointwiseProductToProductColimit (I := I) fun (s : α) ↦ F s ⋙ Functor.obj (evaluation D C) d) :
          colimit (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) d) ⟶
            piObj.{u_3, v_1, u_1} fun (s : α) ↦ colimit (F s ⋙ Functor.obj (evaluation D C) d))
        (Iso.hom (Pi.mapIso fun (x : α) ↦ Iso.symm (colimitObjIsoColimitCompEvaluation (F x) d)) :
          Quiver.Hom.{v_1, u_1} (V := C)
            (piObj.{u_3, v_1, u_1} fun (x : α) ↦ colimit (F x ⋙ Functor.obj (evaluation D C) d))
            (piObj.{u_3, v_1, u_1} fun (x : α) ↦ (colimit (F x)).obj d)) :
      colimit (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) d) ⟶
        piObj.{u_3, v_1, u_1} fun (x : α) ↦ (colimit (F x)).obj d)

Tactic:
Pi.hom_ext _ _ (fun s => colimit.hom_ext (fun k => ?_))

Premises used: CategoryTheory.Limits.Pi.hom_ext, CategoryTheory.Limits.colimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
inst_1 : HasProductsOfShape.{u_2, u_1, v_1} ι C
inst_2 : IsIPCOfShape.{w, u_2, v_1, u_1} ι C
J : ι → Type w
inst_3 : (i : ι) → SmallCategory (J i)
inst_4 : ∀ (i : ι), IsFiltered.{w, w} (J i)
F : (i : ι) → Functor.{w, v_1, w, u_1} (J i) C
inst_5 : ∀ (i : ι), HasColimit (F i)
inst_6 : HasColimit (pointwiseProduct (I := J) F)
⊢ IsIso (X := colimit (pointwiseProduct (I := J) F)) (Y := piObj.{u_2, v_1, u_1} fun (s : ι) ↦ colimit (F s))
    (IsColimit.desc (colimit.isColimit (pointwiseProduct (I := J) F))
        (coconePointwiseProduct (I := J) fun (s : ι) ↦ colimit.cocone (F s)) :
      (colimit.cocone (pointwiseProduct (I := J) F)).pt ⟶
        Cocone.pt (J := (i : ι) → J i) (F := pointwiseProduct (I := J) F)
          (coconePointwiseProduct (I := J) fun (s : ι) ↦ colimit.cocone (F s)))

Tactic:
((colimit.isColimit (pointwiseProduct F)).nonempty_isColimit_iff_isIso_desc).mp ?_

Premises used: CategoryTheory.Limits.IsColimit.nonempty_isColimit_iff_isIso_desc, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.colimit, CategoryTheory.Limits.limit, Iff.mp, CategoryTheory.Limits.pointwiseProduct
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
inst_1 : HasProductsOfShape.{u_2, u_1, v_1} ι C
inst_2 : IsIPCOfShape.{w, u_2, v_1, u_1} ι C
J : ι → Type w
inst_3 : (i : ι) → SmallCategory (J i)
inst_4 : ∀ (i : ι), IsFiltered.{w, w} (J i)
F : (i : ι) → Functor.{w, v_1, w, u_1} (J i) C
inst_5 : ∀ (i : ι), HasColimit (F i)
inst_6 : HasColimit (pointwiseProduct (I := J) F)
refine :
  Nonempty
    (IsColimit (J := (i : ι) → J i) (C := C) (F := pointwiseProduct (I := J) F)
      (coconePointwiseProduct (I := J) fun (s : ι) ↦ colimit.cocone (F s)))
⊢ IsIso (X := colimit (pointwiseProduct (I := J) F)) (Y := piObj.{u_2, v_1, u_1} fun (s : ι) ↦ colimit (F s))
    (IsColimit.desc (colimit.isColimit (pointwiseProduct (I := J) F))
        (coconePointwiseProduct (I := J) fun (s : ι) ↦ colimit.cocone (F s)) :
      (colimit.cocone (pointwiseProduct (I := J) F)).pt ⟶
        Cocone.pt (J := (i : ι) → J i) (F := pointwiseProduct (I := J) F)
          (coconePointwiseProduct (I := J) fun (s : ι) ↦ colimit.cocone (F s)))

Tactic:
refine ((colimit.isColimit (pointwiseProduct F)).nonempty_isColimit_iff_isIso_desc).mp ?_

Premises used: CategoryTheory.Limits.IsColimit.nonempty_isColimit_iff_isIso_desc, CategoryTheory.Limits.colimit.isColimit, Iff.mp, CategoryTheory.Limits.pointwiseProduct
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
inst_1 : HasProductsOfShape.{u_2, u_1, v_1} ι C
inst_2 : IsIPCOfShape.{w, u_2, v_1, u_1} ι C
J : ι → Type w
inst_3 : (i : ι) → SmallCategory (J i)
inst_4 : ∀ (i : ι), IsFiltered.{w, w} (J i)
F : (i : ι) → Functor.{w, v_1, w, u_1} (J i) C
inst_5 : ∀ (i : ι), HasColimit (F i)
inst_6 : HasColimit (pointwiseProduct (I := J) F)
⊢ Nonempty
    (IsColimit (J := (i : ι) → J i) (C := C) (F := pointwiseProduct (I := J) F)
      (coconePointwiseProduct (I := J) fun (s : ι) ↦ colimit.cocone (F s)))

Tactic:
IsIPCOfShape.nonempty_isColimit fun i ↦ colimit.isColimit _

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.IsIPCOfShape.nonempty_isColimit
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
inst_1 : HasProductsOfShape.{u_2, u_1, v_1} ι C
inst_2 : IsIPCOfShape.{w, u_2, v_1, u_1} ι C
J : ι → Type w
inst_3 : (i : ι) → SmallCategory (J i)
inst_4 : ∀ (i : ι), IsFiltered.{w, w} (J i)
F : (i : ι) → Functor.{w, v_1, w, u_1} (J i) C
inst_5 : ∀ (i : ι), HasColimit (F i)
inst_6 : HasColimit (pointwiseProduct (I := J) F)
⊢ Nonempty
    (IsColimit (J := (i : ι) → J i) (C := C) (F := pointwiseProduct (I := J) F)
      (coconePointwiseProduct (I := J) fun (s : ι) ↦ colimit.cocone (F s)))

Tactic:
exact IsIPCOfShape.nonempty_isColimit fun i ↦ colimit.isColimit _

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.IsIPCOfShape.nonempty_isColimit
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
inst_1 : HasProductsOfShape.{u_2, u_1, v_1} ι C
H :
  ∀ ⦃J : ι → Type w⦄ [inst_2 : (i : ι) → SmallCategory (J i)] [∀ (i : ι), IsFiltered.{w, w} (J i)]
    (F : (i : ι) → Functor.{w, v_1, w, u_1} (J i) C) [∀ (i : ι), HasColimit (F i)],
    ∃ (c : (i : ι) → Cocone (F i)) (x : (i : ι) → IsColimit (c i)),
      Nonempty (IsColimit (F := pointwiseProduct (I := J) F) (coconePointwiseProduct (I := J) c))
J : ι → Type w
x : (i : ι) → SmallCategory (J i)
h : ∀ (i : ι), IsFiltered.{w, w} (J i)
F : (i : ι) → Functor.{w, v_1, w, u_1} (J i) C
c : (i : ι) → Cocone (F i)
hc : (i : ι) → IsColimit (c i)
⊢ ∀ (i : ι), HasColimit (F i)

Tactic:
have (i : ι) : HasColimit (F i) := ⟨_, hc i⟩
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
inst_1 : HasProductsOfShape.{u_2, u_1, v_1} ι C
H :
  ∀ ⦃J : ι → Type w⦄ [inst_2 : (i : ι) → SmallCategory (J i)] [∀ (i : ι), IsFiltered.{w, w} (J i)]
    (F : (i : ι) → Functor.{w, v_1, w, u_1} (J i) C) [∀ (i : ι), HasColimit (F i)],
    ∃ (c : (i : ι) → Cocone (F i)) (x : (i : ι) → IsColimit (c i)),
      Nonempty (IsColimit (F := pointwiseProduct (I := J) F) (coconePointwiseProduct (I := J) c))
J : ι → Type w
x : (i : ι) → SmallCategory (J i)
h : ∀ (i : ι), IsFiltered.{w, w} (J i)
F : (i : ι) → Functor.{w, v_1, w, u_1} (J i) C
c : (i : ι) → Cocone (F i)
hc : (i : ι) → IsColimit (c i)
this : ∀ (i : ι), HasColimit (F i)
obtain :
  ∀ (c' : (i : ι) → Cocone (F i)) (hc' : (i : ι) → IsColimit (c' i)),
    Nonempty (IsColimit (F := pointwiseProduct (I := J) F) (coconePointwiseProduct (I := J) c')) →
      Nonempty (IsColimit (F := pointwiseProduct (I := J) F) (coconePointwiseProduct (I := J) c))
⊢ Nonempty (IsColimit (F := pointwiseProduct (I := J) F) (coconePointwiseProduct (I := J) c))

Tactic:
obtain ⟨c', hc', _⟩ := H F