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
x : limit (obj curry F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e :
  ∀ (j : J),
    Eq (α := (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι ((obj curry F).obj j) (k j)) :
            (a : (fun (X : Type v) ↦ X) (((curry.obj F).obj j).obj (k j))) →
              (fun (X : Type v) ↦ X) (colimit ((curry.obj F).obj j)))
          (y j) :
        (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (limit.π (obj curry F ⋙ colim) j) :
            (a : (fun (X : Type v) ↦ X) (limit (curry.obj F ⋙ colim))) →
              (fun (X : Type v) ↦ X) ((curry.obj F ⋙ colim).obj j))
          x :
        (fun (X : Type v) ↦ X) ((obj curry F ⋙ colim).obj j))
k' : K
g : (j : J) → k j ⟶ k'
kf : {j j' : J} → (j ⟶ j') → K
gf hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f
wf :
  ∀ {j j' : J} (f : j ⟶ j'),
    Eq (α := (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j' ×ₘ g j' ≫ gf f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj (j', k j'))) → (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
          (y j') :
        (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ×ₘ g j ≫ hf f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj (j, k j))) → (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
          (y j) :
        (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
k'' : K
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k''
s : ∀ {j₁ j₂ j₃ j₄ : J} (f : j₁ ⟶ j₂) (f' : j₃ ⟶ j₄), gf f ≫ i f = hf f' ≫ i f'
h :
  ∀ (j j' : J) (f : j ⟶ j'),
    Eq (α := (fun (X : Type v) ↦ X) (((obj curry (swap K J ⋙ F)).obj k'').obj j'))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (((obj curry (swap K J ⋙ F)).obj k'').map f) :
            (a : (fun (X : Type v) ↦ X) (((curry.obj (swap K J ⋙ F)).obj k'').obj j)) →
              (fun (X : Type v) ↦ X) (((curry.obj (swap K J ⋙ F)).obj k'').obj j'))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j ×ₘ g j ≫ gf (𝟙 j) ≫ i (𝟙 j))) :
                (a : (fun (X : Type v) ↦ X) (F.obj (j, k j))) → (fun (X : Type v) ↦ X) (F.obj (j, k'')))
              (y j) :
            (fun (X : Type v) ↦ X) (F.obj (j, k''))) :
        (fun (X : Type v) ↦ X) (((obj curry (swap K J ⋙ F)).obj k'').obj j'))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j' ×ₘ g j' ≫ gf (𝟙 j') ≫ i (𝟙 j'))) :
            (a : (fun (X : Type v) ↦ X) (F.obj (j', k j'))) → (fun (X : Type v) ↦ X) (F.obj (j', k'')))
          (y j') :
        (fun (X : Type v) ↦ X) (F.obj (j', k'')))
x₁ : (j : J) → ((obj curry (swap K J ⋙ F)).obj k'').obj j
⊢ limit ((obj curry (swap K J ⋙ F)).obj k'')

Tactic:
apply Limit.mk

Premises used: CategoryTheory.Limits.Types.Limit.mk
-- 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
x : limit (obj curry F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e :
  ∀ (j : J),
    Eq (α := (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι ((obj curry F).obj j) (k j)) :
            (a : (fun (X : Type v) ↦ X) (((curry.obj F).obj j).obj (k j))) →
              (fun (X : Type v) ↦ X) (colimit ((curry.obj F).obj j)))
          (y j) :
        (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (limit.π (obj curry F ⋙ colim) j) :
            (a : (fun (X : Type v) ↦ X) (limit (curry.obj F ⋙ colim))) →
              (fun (X : Type v) ↦ X) ((curry.obj F ⋙ colim).obj j))
          x :
        (fun (X : Type v) ↦ X) ((obj curry F ⋙ colim).obj j))
k' : K
g : (j : J) → k j ⟶ k'
kf : {j j' : J} → (j ⟶ j') → K
gf hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f
wf :
  ∀ {j j' : J} (f : j ⟶ j'),
    Eq (α := (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j' ×ₘ g j' ≫ gf f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj (j', k j'))) → (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
          (y j') :
        (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ×ₘ g j ≫ hf f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj (j, k j))) → (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
          (y j) :
        (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
k'' : K
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k''
s : ∀ {j₁ j₂ j₃ j₄ : J} (f : j₁ ⟶ j₂) (f' : j₃ ⟶ j₄), gf f ≫ i f = hf f' ≫ i f'
⊢ (j : J) → ((obj curry (swap K J ⋙ F)).obj k'').obj j

Tactic:
exact fun j => F.map (𝟙 j ×ₘ (g j ≫ gf (𝟙 j) ≫ i (𝟙 j))) (y j)

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Prod.mkHom, CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.comp, DFunLike.coe
-- 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
x : limit (obj curry F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e :
  ∀ (j : J),
    Eq (α := (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι ((obj curry F).obj j) (k j)) :
            (a : (fun (X : Type v) ↦ X) (((curry.obj F).obj j).obj (k j))) →
              (fun (X : Type v) ↦ X) (colimit ((curry.obj F).obj j)))
          (y j) :
        (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (limit.π (obj curry F ⋙ colim) j) :
            (a : (fun (X : Type v) ↦ X) (limit (curry.obj F ⋙ colim))) →
              (fun (X : Type v) ↦ X) ((curry.obj F ⋙ colim).obj j))
          x :
        (fun (X : Type v) ↦ X) ((obj curry F ⋙ colim).obj j))
k' : K
g : (j : J) → k j ⟶ k'
kf : {j j' : J} → (j ⟶ j') → K
gf hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f
wf :
  ∀ {j j' : J} (f : j ⟶ j'),
    Eq (α := (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j' ×ₘ g j' ≫ gf f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj (j', k j'))) → (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
          (y j') :
        (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ×ₘ g j ≫ hf f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj (j, k j))) → (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
          (y j) :
        (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
k'' : K
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k''
s : ∀ {j₁ j₂ j₃ j₄ : J} (f : j₁ ⟶ j₂) (f' : j₃ ⟶ j₄), gf f ≫ i f = hf f' ≫ i f'
j j' : J
f : j ⟶ j'
h :
  Eq (α := F.obj (j', k''))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ×ₘ g j ≫ gf (𝟙 j) ≫ i (𝟙 j))) :
          (a : F.obj (j, k j)) → F.obj (j', k''))
        (y j) :
      F.obj (j', k''))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j' ×ₘ g j' ≫ gf (𝟙 j') ≫ i (𝟙 j'))) :
          (a : F.obj (j', k j')) → F.obj (j', k''))
        (y j') :
      F.obj (j', k''))
⊢ Eq (α := F.obj (j', k''))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ×ₘ 𝟙 k'')) : (a : F.obj (j, k'')) → F.obj (j', k''))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j ×ₘ g j ≫ gf (𝟙 j) ≫ i (𝟙 j))) :
              (a : F.obj (j, k j)) → F.obj (j, k''))
            (y j) :
          F.obj (j, k'')) :
      F.obj (j', k''))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j' ×ₘ g j' ≫ gf (𝟙 j') ≫ i (𝟙 j'))) :
          (a : F.obj (j', k j')) → F.obj (j', k''))
        (y j') :
      F.obj (j', k''))

Tactic:
simp only [← comp_apply, ← Functor.map_comp, prod_comp, id_comp, comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.comp_apply, CategoryTheory.Functor.map_comp, CategoryTheory.prod_comp, CategoryTheory.Category.id_comp
-- 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
x : limit (obj curry F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e :
  ∀ (j : J),
    Eq (α := (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι ((obj curry F).obj j) (k j)) :
            (a : (fun (X : Type v) ↦ X) (((curry.obj F).obj j).obj (k j))) →
              (fun (X : Type v) ↦ X) (colimit ((curry.obj F).obj j)))
          (y j) :
        (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (limit.π (obj curry F ⋙ colim) j) :
            (a : (fun (X : Type v) ↦ X) (limit (curry.obj F ⋙ colim))) →
              (fun (X : Type v) ↦ X) ((curry.obj F ⋙ colim).obj j))
          x :
        (fun (X : Type v) ↦ X) ((obj curry F ⋙ colim).obj j))
k' : K
g : (j : J) → k j ⟶ k'
kf : {j j' : J} → (j ⟶ j') → K
gf hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f
wf :
  ∀ {j j' : J} (f : j ⟶ j'),
    Eq (α := (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j' ×ₘ g j' ≫ gf f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj (j', k j'))) → (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
          (y j') :
        (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ×ₘ g j ≫ hf f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj (j, k j))) → (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
          (y j) :
        (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
k'' : K
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k''
s : ∀ {j₁ j₂ j₃ j₄ : J} (f : j₁ ⟶ j₂) (f' : j₃ ⟶ j₄), gf f ≫ i f = hf f' ≫ i f'
j j' : J
f : j ⟶ j'
rw rw₁ :
  Eq (α := (fun (X : Type v) ↦ X) (F.obj (j', k'')))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ×ₘ g j ≫ hf f ≫ i f)) :
          (a : (fun (X : Type v) ↦ X) (F.obj (j, k j))) → (fun (X : Type v) ↦ X) (F.obj (j', k'')))
        (y j) :
      (fun (X : Type v) ↦ X) (F.obj (j', k'')))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ×ₘ g j ≫ hf f ≫ i f)) :
          (a : (fun (X : Type v) ↦ X) (F.obj (j, k j))) → (fun (X : Type v) ↦ X) (F.obj (j', k'')))
        (y j) :
      (fun (X : Type v) ↦ X) (F.obj (j', k'')))
⊢ Eq (α := (fun (X : Type v) ↦ X) (F.obj (j', k'')))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ×ₘ g j ≫ gf (𝟙 j) ≫ i (𝟙 j))) :
          (a : (fun (X : Type v) ↦ X) (F.obj (j, k j))) → (fun (X : Type v) ↦ X) (F.obj (j', k'')))
        (y j) :
      (fun (X : Type v) ↦ X) (F.obj (j', k'')))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ×ₘ g j ≫ hf f ≫ i f)) :
          (a : (fun (X : Type v) ↦ X) (F.obj (j, k j))) → (fun (X : Type v) ↦ X) (F.obj (j', k'')))
        (y j) :
      (fun (X : Type v) ↦ X) (F.obj (j', k'')))

Tactic:
rw [s (𝟙 j) f]

Premises used: CategoryTheory.CategoryStruct.id
-- 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
⊢ IsIso (X := colimit (obj curry (swap K J ⋙ F) ⋙ lim)) (Y := limit (obj curry F ⋙ colim))
    (colimitLimitToLimitColimit F)

Tactic:
(isIso_iff_bijective _).mpr
    ⟨colimitLimitToLimitColimit_injective F, colimitLimitToLimitColimit_surjective F⟩

Premises used: Iff.mpr, CategoryTheory.isIso_iff_bijective, And.intro, CategoryTheory.Limits.colimitLimitToLimitColimit_injective, CategoryTheory.Limits.colimitLimitToLimitColimit_surjective
-- 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_1 : J × K ⥤ Type v
inst_4 : IsFiltered.{v₂, u₂} K
F : J ⥤ Functor.{v₂, v, u₂, v + 1} K (Type v)
this :
  IsIso (X := colimit (obj curry (swap K J ⋙ obj uncurry F) ⋙ lim)) (Y :=
    obj lim (obj (𝟭 (J ⥤ Functor.{v₂, v, u₂, v + 1} K (Type v))) F ⋙ colim))
    (CategoryStruct.comp (Y := limit (obj curry (obj uncurry F) ⋙ colim)) (colimitLimitToLimitColimit (obj uncurry F))
        (map lim (whiskerRight (Iso.inv (Iso.app (Equivalence.unitIso currying) F)) colim)) :
      colimit (obj curry (swap K J ⋙ obj uncurry F) ⋙ lim) ⟶
        obj lim (obj (𝟭 (J ⥤ Functor.{v₂, v, u₂, v + 1} K (Type v))) F ⋙ colim))
⊢ IsIso (X := Cone.pt (F := F ⋙ colim) (mapCone colim (limit.cone F))) (Y := (limit.cone (F ⋙ colim)).pt)
    (ConeMorphism.hom (colimitLimitToLimitColimitCone F) :
      Cone.pt (F := F ⋙ colim) (mapCone colim (limit.cone F)) ⟶ (limit.cone (F ⋙ colim)).pt)

Tactic:
apply IsIso.comp_isIso

Premises used: CategoryTheory.IsIso.comp_isIso
-- 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_1 : J × K ⥤ Type v
inst_4 : IsFiltered.{v₂, u₂} K
F : J ⥤ Functor.{v₂, v, u₂, v + 1} K (Type v)
suffices :
  IsIso (X := colimit (obj curry (swap K J ⋙ obj uncurry F) ⋙ lim)) (Y :=
    obj lim (obj (𝟭 (J ⥤ Functor.{v₂, v, u₂, v + 1} K (Type v))) F ⋙ colim))
    (CategoryStruct.comp (Y := limit (obj curry (obj uncurry F) ⋙ colim)) (colimitLimitToLimitColimit (obj uncurry F))
        (map lim (whiskerRight (Iso.inv (Iso.app (Equivalence.unitIso currying) F)) colim)) :
      colimit (obj curry (swap K J ⋙ obj uncurry F) ⋙ lim) ⟶
        obj lim (obj (𝟭 (J ⥤ Functor.{v₂, v, u₂, v + 1} K (Type v))) F ⋙ colim))
⊢ IsIso (X := Cone.pt (F := F ⋙ colim) (mapCone colim (limit.cone F))) (Y := (limit.cone (F ⋙ colim)).pt)
    (ConeMorphism.hom (colimitLimitToLimitColimitCone F) :
      Cone.pt (F := F ⋙ colim) (mapCone colim (limit.cone F)) ⟶ (limit.cone (F ⋙ colim)).pt)

Tactic:
suffices IsIso (colimitLimitToLimitColimit (uncurry.obj F) ≫
        lim.map (whiskerRight (currying.unitIso.app F).inv colim)) by
      apply IsIso.comp_isIso
-- 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_1 : J × K ⥤ Type v
inst_4 : IsFiltered.{v₂, u₂} K
F : J ⥤ Functor.{v₂, v, u₂, v + 1} K (Type v)
⊢ IsIso (X := colimit (obj curry (swap K J ⋙ obj uncurry F) ⋙ lim)) (Y :=
    obj lim (obj (𝟭 (J ⥤ Functor.{v₂, v, u₂, v + 1} K (Type v))) F ⋙ colim))
    (CategoryStruct.comp (Y := limit (obj curry (obj uncurry F) ⋙ colim)) (colimitLimitToLimitColimit (obj uncurry F))
        (map lim (whiskerRight (Iso.inv (Iso.app (Equivalence.unitIso currying) F)) colim)) :
      colimit (obj curry (swap K J ⋙ obj uncurry F) ⋙ lim) ⟶
        obj lim (obj (𝟭 (J ⥤ Functor.{v₂, v, u₂, v + 1} K (Type v))) F ⋙ colim))

Tactic:
infer_instance
-- 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_1 : J × K ⥤ Type v
inst_4 : IsFiltered.{v₂, u₂} K
F : J ⥤ Functor.{v₂, v, u₂, v + 1} K (Type v)
⊢ IsIso (X := Cone.pt (F := F ⋙ colim) (mapCone colim (limit.cone F))) (Y := (limit.cone (F ⋙ colim)).pt)
    (ConeMorphism.hom (colimitLimitToLimitColimitCone F) :
      Cone.pt (F := F ⋙ colim) (mapCone colim (limit.cone F)) ⟶ (limit.cone (F ⋙ colim)).pt)

Tactic:
have : IsIso (colimitLimitToLimitColimitCone F).hom := by
    suffices IsIso (colimitLimitToLimitColimit (uncurry.obj F) ≫
        lim.map (whiskerRight (currying.unitIso.app F).inv colim)) by
      apply IsIso.comp_isIso
    infer_instance
-- 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_1 : J × K ⥤ Type v
inst_4 : IsFiltered.{v₂, u₂} K
F : J ⥤ Functor.{v₂, v, u₂, v + 1} K (Type v)
this :
  IsIso (X := Cone.pt (F := F ⋙ colim) (mapCone colim (limit.cone F))) (Y := (limit.cone (F ⋙ colim)).pt)
    (ConeMorphism.hom (colimitLimitToLimitColimitCone F) :
      Cone.pt (F := F ⋙ colim) (mapCone colim (limit.cone F)) ⟶ (limit.cone (F ⋙ colim)).pt)
⊢ IsIso (C := Cone (F ⋙ colim)) (X := mapCone colim (limit.cone F)) (Y := limit.cone (F ⋙ colim))
    (colimitLimitToLimitColimitCone F : mapCone colim (limit.cone F) ⟶ limit.cone (F ⋙ colim))

Tactic:
apply Cone.cone_iso_of_hom_iso

Premises used: CategoryTheory.Limits.Cone.cone_iso_of_hom_iso
-- 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
h :
  ∀ (J : Type v₂) {𝒥 : SmallCategory J} (x : FinCategory J),
    PreservesLimitsOfShape (C := Functor.{v₂, v, u₂, v + 1} K (Type v)) J colim
⊢ PreservesFiniteLimits (C := Functor.{v₂, v, u₂, v + 1} K (Type v)) 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
J : Type v₂
h :
  ∀ {𝒥 : SmallCategory J} (x : FinCategory J),
    PreservesLimitsOfShape (C := Functor.{v₂, v, u₂, v + 1} K (Type v)) J colim
⊢ ∀ {𝒥 : SmallCategory J} (x : FinCategory J),
    PreservesLimitsOfShape (C := Functor.{v₂, v, u₂, v + 1} K (Type v)) 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
J : Type v₂
𝒥 : SmallCategory J
h : ∀ (x : FinCategory J), PreservesLimitsOfShape (C := Functor.{v₂, v, u₂, v + 1} K (Type v)) J colim
⊢ ∀ (x : FinCategory J), PreservesLimitsOfShape (C := Functor.{v₂, v, u₂, v + 1} K (Type v)) 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
J : Type v₂
𝒥 : SmallCategory J
x : FinCategory J
⊢ PreservesLimitsOfShape (C := Functor.{v₂, v, u₂, v + 1} K (Type v)) J colim

Tactic:
⟨fun {F} => ⟨fun {c} hc => ⟨IsLimit.ofIsoLimit (limit.isLimit _) ?_⟩⟩⟩

Premises used: CategoryTheory.Limits.colim, CategoryTheory.Functor.comp, Nonempty.intro, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.PreservesLimitsOfShape.mk, CategoryTheory.Limits.PreservesLimit.mk, CategoryTheory.Limits.IsLimit.ofIsoLimit
-- 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
J : Type v₂
𝒥 : SmallCategory J
x : FinCategory J
h :
  {F : J ⥤ Functor.{v₂, v, u₂, v + 1} K (Type v)} →
    {c : Cone F} → (hc : IsLimit c) → limit.cone (F ⋙ colim) ≅ mapCone colim c
⊢ PreservesLimitsOfShape (C := Functor.{v₂, v, u₂, v + 1} K (Type v)) J colim

Tactic:
refine ⟨fun {F} => ⟨fun {c} hc => ⟨IsLimit.ofIsoLimit (limit.isLimit _) ?_⟩⟩⟩
-- 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_1 : J_1 × K ⥤ Type v
inst_4 : IsFiltered.{v₂, u₂} K
J : Type v₂
𝒥 : SmallCategory J
x : FinCategory J
F : J ⥤ Functor.{v₂, v, u₂, v + 1} K (Type v)
c : Cone F
hc : IsLimit c
h : mapCone colim c ≅ limit.cone (F ⋙ colim)
⊢ limit.cone (F ⋙ colim) ≅ mapCone colim c

Tactic:
symm
-- 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_1 : J_1 × K ⥤ Type v
inst_4 : IsFiltered.{v₂, u₂} K
J : Type v₂
𝒥 : SmallCategory J
x : FinCategory J
F : J ⥤ Functor.{v₂, v, u₂, v + 1} K (Type v)
c : Cone F
hc : IsLimit c
trans : Iso (C := Cone (F ⋙ colim)) (mapCone colim c) (mapCone colim (limit.cone F))
trans₁ : mapCone colim (limit.cone F) ≅ limit.cone (F ⋙ colim)
⊢ mapCone colim c ≅ limit.cone (F ⋙ colim)

Tactic:
trans colim.mapCone (limit.cone F)

Premises used: CategoryTheory.Limits.colim, CategoryTheory.Limits.limit.cone, CategoryTheory.Functor.mapCone
-- 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_1 : J_1 × K ⥤ Type v
inst_4 : IsFiltered.{v₂, u₂} K
J : Type v₂
𝒥 : SmallCategory J
x : FinCategory J
F : J ⥤ Functor.{v₂, v, u₂, v + 1} K (Type v)
c : Cone F
hc : IsLimit c
⊢ Iso (C := Cone (F ⋙ colim)) (mapCone colim c) (mapCone colim (limit.cone F))

Tactic:
exact Functor.mapIso _ (hc.uniqueUpToIso (limit.isLimit F))

Premises used: CategoryTheory.Limits.IsLimit.uniqueUpToIso, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Functor.mapIso
-- 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_1 : J_1 × K ⥤ Type v
inst_4 : IsFiltered.{v₂, u₂} K
J : Type v₂
𝒥 : SmallCategory J
x : FinCategory J
F : J ⥤ Functor.{v₂, v, u₂, v + 1} K (Type v)
c : Cone F
hc : IsLimit c
⊢ mapCone colim (limit.cone F) ≅ limit.cone (F ⋙ colim)

Tactic:
exact asIso (colimitLimitToLimitColimitCone F)

Premises used: CategoryTheory.Limits.colimitLimitToLimitColimitCone, CategoryTheory.asIso
-- 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 : HasLimitsOfShape.{u₁, u₁, v, u} J C
inst_9 : HasColimitsOfShape.{v₂, u₂, v, u} K C
inst_10 : ReflectsLimitsOfShape J (forget C (FC := FC) (CC := CC))
inst_11 : PreservesColimitsOfShape.{v₂, u₂, v, v, u, v + 1} K (forget C (FC := FC) (CC := CC))
inst_12 : PreservesLimitsOfShape J (forget C (FC := FC) (CC := CC))
⊢ PreservesLimitsOfShape (C := Functor.{v₂, v, u₂, u} K C) J colim

Tactic:
haveI : PreservesLimitsOfShape J ((colim : (K ⥤ C) ⥤ _) ⋙ forget C) :=
    preservesLimitsOfShape_of_natIso (preservesColimitNatIso _).symm
  preservesLimitsOfShape_of_reflects_of_preserves _ (forget C)

Premises used: CategoryTheory.Limits.colim, CategoryTheory.forget, CategoryTheory.Limits.preservesLimitsOfShape_of_reflects_of_preserves