awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Fubini
Goal:
J : Type u_1
K : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} K
C : Type u_3
inst_2 : Category.{v_3, u_3} C
G : J × K ⥤ C
inst_3 : HasLimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasLimitsOfShape.{v_1, u_1, v_3, u_3} J C
inst_5 : HasLimit (obj curry G ⋙ lim)
j : J
k : K
⊢ Eq (α := limit (obj curry G ⋙ lim) ⟶ ((obj curry (Prod.swap K J ⋙ G)).obj k).obj j)
    (Iso.inv (limitCurrySwapCompLimIsoLimitCurryCompLim G) ≫
      limit.π (obj curry (Prod.swap K J ⋙ G) ⋙ lim) k ≫ limit.π ((obj curry (Prod.swap K J ⋙ G)).obj k) j)
    (limit.π (obj curry G ⋙ lim) j ≫ limit.π ((obj curry G).obj j) k)

Tactic:
simp [limitCurrySwapCompLimIsoLimitCurryCompLim]

Premises used: CategoryTheory.Limits.limitCurrySwapCompLimIsoLimitCurryCompLim
-- Module: Mathlib.CategoryTheory.Limits.Fubini
Goal:
J : Type u_1
K : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} K
C : Type u_3
inst_2 : Category.{v_3, u_3} C
G : J × K ⥤ C
inst_3 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasColimitsOfShape.{v_1, u_1, v_3, u_3} J C
inst_5 : HasColimit (obj curry G ⋙ colim)
j : J
k : K
dsimp :
  Eq (α := G.obj (j, k) ⟶ colimit (obj curry G ⋙ colim))
    (colimit.ι ((obj curry (Prod.swap K J ⋙ G)).obj k) j ≫
      CategoryStruct.comp (Y := colimit (obj curry (Prod.swap K J ⋙ G) ⋙ colim))
        (colimit.ι (obj curry (Prod.swap K J ⋙ G) ⋙ colim) k)
        ((Iso.inv (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)) ≫
            Iso.hom (HasColimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G)))) ≫
          Iso.hom (colimitIsoColimitCurryCompColim G)))
    (colimit.ι ((obj curry G).obj j) k ≫ colimit.ι (obj curry G ⋙ colim) j)
⊢ Eq (α := ((obj curry (Prod.swap K J ⋙ G)).obj k).obj j ⟶ colimit (obj curry G ⋙ colim))
    (colimit.ι ((obj curry (Prod.swap K J ⋙ G)).obj k) j ≫
      colimit.ι (obj curry (Prod.swap K J ⋙ G) ⋙ colim) k ≫
        Iso.hom (colimitCurrySwapCompColimIsoColimitCurryCompColim G))
    (colimit.ι ((obj curry G).obj j) k ≫ colimit.ι (obj curry G ⋙ colim) j)

Tactic:
dsimp [colimitCurrySwapCompColimIsoColimitCurryCompColim]

Premises used: CategoryTheory.Limits.colimitCurrySwapCompColimIsoColimitCurryCompColim
-- Module: Mathlib.CategoryTheory.Limits.Fubini
Goal:
J : Type u_1
K : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} K
C : Type u_3
inst_2 : Category.{v_3, u_3} C
G : J × K ⥤ C
inst_3 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasColimitsOfShape.{v_1, u_1, v_3, u_3} J C
inst_5 : HasColimit (obj curry G ⋙ colim)
j : J
k : K
slice_lhs :
  Eq (α := G.obj (j, k) ⟶ colimit (obj curry G ⋙ colim))
    (CategoryStruct.comp (Y := colimit (Prod.swap K J ⋙ G))
        (colimit.ι ((obj curry (Prod.swap K J ⋙ G)).obj k) j ≫
            CategoryStruct.comp (Y := colimit (obj curry (Prod.swap K J ⋙ G) ⋙ colim))
              (colimit.ι (obj curry (Prod.swap K J ⋙ G) ⋙ colim) k)
              (Iso.inv (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G))) :
          G.obj (j, k) ⟶ colimit (Prod.swap K J ⋙ G))
        (Iso.hom (HasColimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G))) :
          colimit (Prod.swap K J ⋙ G) ⟶ colimit G) ≫
      Iso.hom (colimitIsoColimitCurryCompColim G))
    (colimit.ι ((obj curry G).obj j) k ≫ colimit.ι (obj curry G ⋙ colim) j)
⊢ Eq (α := G.obj (j, k) ⟶ colimit (obj curry G ⋙ colim))
    (colimit.ι ((obj curry (Prod.swap K J ⋙ G)).obj k) j ≫
      CategoryStruct.comp (Y := colimit (obj curry (Prod.swap K J ⋙ G) ⋙ colim))
        (colimit.ι (obj curry (Prod.swap K J ⋙ G) ⋙ colim) k)
        ((Iso.inv (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)) ≫
            Iso.hom (HasColimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G)))) ≫
          Iso.hom (colimitIsoColimitCurryCompColim G)))
    (colimit.ι ((obj curry G).obj j) k ≫ colimit.ι (obj curry G ⋙ colim) j)

Tactic:
slice_lhs 1 3 => simp only []
-- Module: Mathlib.CategoryTheory.Limits.Fubini
Goal:
J : Type u_1
K : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} K
C : Type u_3
inst_2 : Category.{v_3, u_3} C
G : J × K ⥤ C
inst_3 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasColimitsOfShape.{v_1, u_1, v_3, u_3} J C
inst_5 : HasColimit (obj curry G ⋙ colim)
j : J
k : K
⊢ Eq (α := G.obj (j, k) ⟶ colimit (obj curry G ⋙ colim))
    (CategoryStruct.comp (Y := colimit (Prod.swap K J ⋙ G))
        (colimit.ι ((obj curry (Prod.swap K J ⋙ G)).obj k) j ≫
            CategoryStruct.comp (Y := colimit (obj curry (Prod.swap K J ⋙ G) ⋙ colim))
              (colimit.ι (obj curry (Prod.swap K J ⋙ G) ⋙ colim) k)
              (Iso.inv (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G))) :
          G.obj (j, k) ⟶ colimit (Prod.swap K J ⋙ G))
        (Iso.hom (HasColimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G))) :
          colimit (Prod.swap K J ⋙ G) ⟶ colimit G) ≫
      Iso.hom (colimitIsoColimitCurryCompColim G))
    (colimit.ι ((obj curry G).obj j) k ≫ colimit.ι (obj curry G ⋙ colim) j)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Fubini
Goal:
J : Type u_1
K : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} K
C : Type u_3
inst_2 : Category.{v_3, u_3} C
G : J × K ⥤ C
inst_3 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasColimitsOfShape.{v_1, u_1, v_3, u_3} J C
inst_5 : HasColimit (obj curry G ⋙ colim)
j : J
k : K
dsimp :
  Eq (α := G.obj (j, k) ⟶ colimit (obj curry (Prod.swap K J ⋙ G) ⋙ colim))
    (colimit.ι ((obj curry G).obj j) k ≫
      CategoryStruct.comp (Y := colimit (obj curry G ⋙ colim)) (colimit.ι (obj curry G ⋙ colim) j)
        (Iso.inv (colimitIsoColimitCurryCompColim G) ≫
          Iso.inv (HasColimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G))) ≫
            Iso.hom (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G))))
    (colimit.ι ((obj curry (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (obj curry (Prod.swap K J ⋙ G) ⋙ colim) k)
⊢ colimit.ι ((obj curry G).obj j) k ≫
      CategoryStruct.comp (Y := colimit (obj curry G ⋙ colim)) (colimit.ι (obj curry G ⋙ colim) j)
        (Iso.inv (colimitCurrySwapCompColimIsoColimitCurryCompColim G)) =
    colimit.ι ((obj curry (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (obj curry (Prod.swap K J ⋙ G) ⋙ colim) k

Tactic:
dsimp [colimitCurrySwapCompColimIsoColimitCurryCompColim]

Premises used: CategoryTheory.Limits.colimitCurrySwapCompColimIsoColimitCurryCompColim
-- Module: Mathlib.CategoryTheory.Limits.Fubini
Goal:
J : Type u_1
K : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} K
C : Type u_3
inst_2 : Category.{v_3, u_3} C
G : J × K ⥤ C
inst_3 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasColimitsOfShape.{v_1, u_1, v_3, u_3} J C
inst_5 : HasColimit (obj curry G ⋙ colim)
j : J
k : K
slice_lhs :
  Eq (α := G.obj (j, k) ⟶ colimit (obj curry (Prod.swap K J ⋙ G) ⋙ colim))
    (CategoryStruct.comp (Y := colimit G)
        (colimit.ι ((obj curry G).obj j) k ≫
            CategoryStruct.comp (Y := colimit (obj curry G ⋙ colim)) (colimit.ι (obj curry G ⋙ colim) j)
              (Iso.inv (colimitIsoColimitCurryCompColim G)) :
          G.obj (j, k) ⟶ colimit G)
        (Iso.inv (HasColimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G))) :
          colimit G ⟶ colimit (Prod.swap K J ⋙ G)) ≫
      Iso.hom (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)))
    (colimit.ι ((obj curry (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (obj curry (Prod.swap K J ⋙ G) ⋙ colim) k)
⊢ Eq (α := G.obj (j, k) ⟶ colimit (obj curry (Prod.swap K J ⋙ G) ⋙ colim))
    (colimit.ι ((obj curry G).obj j) k ≫
      CategoryStruct.comp (Y := colimit (obj curry G ⋙ colim)) (colimit.ι (obj curry G ⋙ colim) j)
        (Iso.inv (colimitIsoColimitCurryCompColim G) ≫
          Iso.inv (HasColimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G))) ≫
            Iso.hom (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G))))
    (colimit.ι ((obj curry (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (obj curry (Prod.swap K J ⋙ G) ⋙ colim) k)

Tactic:
slice_lhs 1 3 => simp only []
-- Module: Mathlib.CategoryTheory.Limits.Fubini
Goal:
J : Type u_1
K : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} K
C : Type u_3
inst_2 : Category.{v_3, u_3} C
G : J × K ⥤ C
inst_3 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasColimitsOfShape.{v_1, u_1, v_3, u_3} J C
inst_5 : HasColimit (obj curry G ⋙ colim)
j : J
k : K
rw :
  Eq (α := G.obj (j, k) ⟶ colimit (obj curry (Prod.swap K J ⋙ G) ⋙ colim))
    (CategoryStruct.comp (Y :=
        G.obj (obj (Equivalence.inverse (Prod.braiding K J) ⋙ Equivalence.functor (Prod.braiding K J)) (j, k)))
        (G.map (NatTrans.app (Equivalence.counitInv (Prod.braiding K J)) (j, k)))
        (NatTrans.app (Iso.hom (Iso.refl (Prod.swap K J ⋙ G))) (obj (Equivalence.inverse (Prod.braiding K J)) (j, k)) ≫
          colimit.ι (Prod.swap K J ⋙ G) (obj (Equivalence.inverse (Prod.braiding K J)) (j, k))) ≫
      Iso.hom (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)))
    (colimit.ι ((obj curry (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (obj curry (Prod.swap K J ⋙ G) ⋙ colim) k)
⊢ Eq (α := G.obj (j, k) ⟶ colimit (obj curry (Prod.swap K J ⋙ G) ⋙ colim))
    (CategoryStruct.comp (Y := colimit G)
        (colimit.ι ((obj curry G).obj j) k ≫
            CategoryStruct.comp (Y := colimit (obj curry G ⋙ colim)) (colimit.ι (obj curry G ⋙ colim) j)
              (Iso.inv (colimitIsoColimitCurryCompColim G)) :
          G.obj (j, k) ⟶ colimit G)
        (Iso.inv (HasColimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G))) :
          colimit G ⟶ colimit (Prod.swap K J ⋙ G)) ≫
      Iso.hom (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)))
    (colimit.ι ((obj curry (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (obj curry (Prod.swap K J ⋙ G) ⋙ colim) k)

Tactic:
rw [colimitIsoColimitCurryCompColim_ι_ι_inv, HasColimit.ι_isoOfEquivalence_inv]

Premises used: CategoryTheory.Limits.HasColimit.ι_isoOfEquivalence_inv, CategoryTheory.Limits.colimitIsoColimitCurryCompColim_ι_ι_inv
-- Module: Mathlib.CategoryTheory.Limits.Fubini
Goal:
J : Type u_1
K : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} K
C : Type u_3
inst_2 : Category.{v_3, u_3} C
G : J × K ⥤ C
inst_3 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasColimitsOfShape.{v_1, u_1, v_3, u_3} J C
inst_5 : HasColimit (obj curry G ⋙ colim)
j : J
k : K
dsimp :
  Eq (α := G.obj (j, k) ⟶ colimit (obj curry (Prod.swap K J ⋙ G) ⋙ colim))
    ((G.map (Prod.mkHom (𝟙 j) (𝟙 k)) ≫ 𝟙 (G.obj (j, k)) ≫ colimit.ι (Prod.swap K J ⋙ G) (k, j)) ≫
      Iso.hom (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)))
    (colimit.ι ((obj curry (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (obj curry (Prod.swap K J ⋙ G) ⋙ colim) k)
⊢ Eq (α := G.obj (j, k) ⟶ colimit (obj curry (Prod.swap K J ⋙ G) ⋙ colim))
    (CategoryStruct.comp (Y :=
        G.obj (obj (Equivalence.inverse (Prod.braiding K J) ⋙ Equivalence.functor (Prod.braiding K J)) (j, k)))
        (G.map (NatTrans.app (Equivalence.counitInv (Prod.braiding K J)) (j, k)))
        (NatTrans.app (Iso.hom (Iso.refl (Prod.swap K J ⋙ G))) (obj (Equivalence.inverse (Prod.braiding K J)) (j, k)) ≫
          colimit.ι (Prod.swap K J ⋙ G) (obj (Equivalence.inverse (Prod.braiding K J)) (j, k))) ≫
      Iso.hom (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)))
    (colimit.ι ((obj curry (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (obj curry (Prod.swap K J ⋙ G) ⋙ colim) k)

Tactic:
dsimp [Equivalence.counitInv]

Premises used: CategoryTheory.Equivalence.counitInv
-- Module: Mathlib.CategoryTheory.Limits.Fubini
Goal:
J : Type u_1
K : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} K
C : Type u_3
inst_2 : Category.{v_3, u_3} C
G : J × K ⥤ C
inst_3 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasColimitsOfShape.{v_1, u_1, v_3, u_3} J C
inst_5 : HasColimit (obj curry G ⋙ colim)
j : J
k : K
rw :
  Eq (α := G.obj (j, k) ⟶ colimit (obj curry (Prod.swap K J ⋙ G) ⋙ colim))
    ((𝟙 (G.obj (j, k)) ≫ 𝟙 (G.obj (j, k)) ≫ colimit.ι (Prod.swap K J ⋙ G) (k, j)) ≫
      Iso.hom (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)))
    (colimit.ι ((obj curry (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (obj curry (Prod.swap K J ⋙ G) ⋙ colim) k)
⊢ Eq (α := G.obj (j, k) ⟶ colimit (obj curry (Prod.swap K J ⋙ G) ⋙ colim))
    ((G.map (Prod.mkHom (𝟙 j) (𝟙 k)) ≫ 𝟙 (G.obj (j, k)) ≫ colimit.ι (Prod.swap K J ⋙ G) (k, j)) ≫
      Iso.hom (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)))
    (colimit.ι ((obj curry (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (obj curry (Prod.swap K J ⋙ G) ⋙ colim) k)

Tactic:
rw [CategoryTheory.Bifunctor.map_id]

Premises used: CategoryTheory.Bifunctor.map_id
-- Module: Mathlib.CategoryTheory.Limits.Fubini
Goal:
J : Type u_1
K : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} K
C : Type u_3
inst_2 : Category.{v_3, u_3} C
G : J × K ⥤ C
inst_3 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasColimitsOfShape.{v_1, u_1, v_3, u_3} J C
inst_5 : HasColimit (obj curry G ⋙ colim)
j : J
k : K
⊢ Eq (α := G.obj (j, k) ⟶ colimit (obj curry (Prod.swap K J ⋙ G) ⋙ colim))
    ((𝟙 (G.obj (j, k)) ≫ 𝟙 (G.obj (j, k)) ≫ colimit.ι (Prod.swap K J ⋙ G) (k, j)) ≫
      Iso.hom (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)))
    (colimit.ι ((obj curry (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (obj curry (Prod.swap K J ⋙ G) ⋙ colim) k)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.FullSubcategory
Goal:
J : Type w
inst : Category.{w', w} J
C : Type u
inst_1 : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : ObjectProperty.IsClosedUnderLimitsOfShape.{w', w, v, u} P J
F : Functor.{w', v, w, u} J P.FullSubcategory
inst_3 : HasLimit (F ⋙ P.ι)
⊢ HasLimit F

Tactic:
have : CreatesLimit F P.ι :=
    createsLimitFullSubcategoryInclusionOfClosed J P F
  hasLimit_of_created F P.ι

Premises used: CategoryTheory.hasLimit_of_created, CategoryTheory.ObjectProperty.ι, CategoryTheory.Limits.createsLimitFullSubcategoryInclusionOfClosed
-- Module: Mathlib.CategoryTheory.Limits.FullSubcategory
Goal:
J : Type w
inst : Category.{w', w} J
C : Type u
inst_1 : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : ObjectProperty.IsClosedUnderLimitsOfShape.{w', w, v, u} P J
inst_3 : HasLimitsOfShape.{w', w, v, u} J C
⊢ HasLimitsOfShape.{w', w, v, u} J P.FullSubcategory

Tactic:
{ has_limit := fun F => hasLimit_of_closedUnderLimits J P F }

Premises used: CategoryTheory.Limits.HasLimitsOfShape.mk, CategoryTheory.Limits.hasLimit_of_closedUnderLimits
-- Module: Mathlib.CategoryTheory.Limits.FullSubcategory
Goal:
J : Type w
inst : Category.{w', w} J
C : Type u
inst_1 : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : ObjectProperty.IsClosedUnderColimitsOfShape.{w', w, v, u} P J
F : Functor.{w', v, w, u} J P.FullSubcategory
inst_3 : HasColimit (F ⋙ P.ι)
⊢ HasColimit F

Tactic:
have : CreatesColimit F P.ι :=
    createsColimitFullSubcategoryInclusionOfClosed J P F
  hasColimit_of_created F P.ι

Premises used: CategoryTheory.ObjectProperty.ι, CategoryTheory.Limits.createsColimitFullSubcategoryInclusionOfClosed, CategoryTheory.hasColimit_of_created
-- Module: Mathlib.CategoryTheory.Limits.FullSubcategory
Goal:
J : Type w
inst : Category.{w', w} J
C : Type u
inst_1 : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : ObjectProperty.IsClosedUnderColimitsOfShape.{w', w, v, u} P J
inst_3 : HasColimitsOfShape.{w', w, v, u} J C
⊢ HasColimitsOfShape.{w', w, v, u} J P.FullSubcategory

Tactic:
{ has_colimit := fun F => hasColimit_of_closedUnderColimits J P F }

Premises used: CategoryTheory.Limits.HasColimitsOfShape.mk, CategoryTheory.Limits.hasColimit_of_closedUnderColimits
-- Module: Mathlib.CategoryTheory.Limits.FullSubcategory
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
J : Type w
inst_1 : Category.{w', w} J
inst_2 : HasColimitsOfShape.{w', w, v, u} J P.FullSubcategory
inst_3 : P.IsClosedUnderIsomorphisms
inst_4 : PreservesColimitsOfShape.{w', w, v, v, u, u} J P.ι
X : C
p : ColimitOfShape.{w', w, v, u} P J X
⊢ P X

Tactic:
P.prop_of_iso (IsColimit.coconePointUniqueUpToIso
      (isColimitOfPreserves P.ι (colimit.isColimit (P.lift p.diag p.prop_diag_obj)))
        p.isColimit) (colimit (P.lift p.diag p.prop_diag_obj)).property

Premises used: CategoryTheory.Limits.ColimitPresentation.isColimit, CategoryTheory.ObjectProperty.ι, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.ObjectProperty.prop_of_iso, CategoryTheory.ObjectProperty.lift, CategoryTheory.Limits.colimit, CategoryTheory.ObjectProperty.ColimitOfShape.prop_diag_obj, CategoryTheory.Limits.ColimitPresentation.diag, CategoryTheory.Limits.isColimitOfPreserves, CategoryTheory.ObjectProperty.ColimitOfShape.toColimitPresentation, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
-- Module: Mathlib.CategoryTheory.Limits.FullSubcategory
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
J : Type w
inst_1 : Category.{w', w} J
inst_2 : HasColimitsOfShape.{w', w, v, u} J P.FullSubcategory
inst_3 : P.IsClosedUnderIsomorphisms
inst_4 : PreservesColimitsOfShape.{w', w, v, v, u, u} J P.ι
X : C
p : ColimitOfShape.{w', w, v, u} P J X
⊢ P X

Tactic:
exact P.prop_of_iso (IsColimit.coconePointUniqueUpToIso
      (isColimitOfPreserves P.ι (colimit.isColimit (P.lift p.diag p.prop_diag_obj)))
        p.isColimit) (colimit (P.lift p.diag p.prop_diag_obj)).property

Premises used: CategoryTheory.Limits.ColimitPresentation.isColimit, CategoryTheory.ObjectProperty.ι, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.ObjectProperty.prop_of_iso, CategoryTheory.ObjectProperty.lift, CategoryTheory.Limits.colimit, CategoryTheory.ObjectProperty.ColimitOfShape.prop_diag_obj, CategoryTheory.Limits.ColimitPresentation.diag, CategoryTheory.Limits.isColimitOfPreserves, CategoryTheory.ObjectProperty.ColimitOfShape.toColimitPresentation, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
-- Module: Mathlib.CategoryTheory.Limits.FullSubcategory
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
J : Type w
inst_1 : Category.{w', w} J
inst_2 : HasLimitsOfShape.{w', w, v, u} J P.FullSubcategory
inst_3 : P.IsClosedUnderIsomorphisms
inst_4 : PreservesLimitsOfShape.{w', w, v, v, u, u} J P.ι
X : C
p : LimitOfShape.{w', w, v, u} P J X
⊢ P X

Tactic:
P.prop_of_iso (IsLimit.conePointUniqueUpToIso
      (isLimitOfPreserves P.ι (limit.isLimit (P.lift p.diag p.prop_diag_obj)))
        p.isLimit) (limit (P.lift p.diag p.prop_diag_obj)).property

Premises used: CategoryTheory.ObjectProperty.LimitOfShape.prop_diag_obj, CategoryTheory.ObjectProperty.ι, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.ObjectProperty.prop_of_iso, CategoryTheory.ObjectProperty.lift, CategoryTheory.Limits.limit.isLimit, CategoryTheory.ObjectProperty.LimitOfShape.toLimitPresentation, CategoryTheory.Limits.limit, CategoryTheory.Limits.LimitPresentation.isLimit, CategoryTheory.Limits.LimitPresentation.diag, CategoryTheory.Limits.isLimitOfPreserves
-- Module: Mathlib.CategoryTheory.Limits.FullSubcategory
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
J : Type w
inst_1 : Category.{w', w} J
inst_2 : HasLimitsOfShape.{w', w, v, u} J P.FullSubcategory
inst_3 : P.IsClosedUnderIsomorphisms
inst_4 : PreservesLimitsOfShape.{w', w, v, v, u, u} J P.ι
X : C
p : LimitOfShape.{w', w, v, u} P J X
⊢ P X

Tactic:
exact P.prop_of_iso (IsLimit.conePointUniqueUpToIso
      (isLimitOfPreserves P.ι (limit.isLimit (P.lift p.diag p.prop_diag_obj)))
        p.isLimit) (limit (P.lift p.diag p.prop_diag_obj)).property

Premises used: CategoryTheory.ObjectProperty.LimitOfShape.prop_diag_obj, CategoryTheory.ObjectProperty.ι, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.ObjectProperty.prop_of_iso, CategoryTheory.ObjectProperty.lift, CategoryTheory.Limits.limit.isLimit, CategoryTheory.ObjectProperty.LimitOfShape.toLimitPresentation, CategoryTheory.Limits.limit, CategoryTheory.Limits.LimitPresentation.isLimit, CategoryTheory.Limits.LimitPresentation.diag, CategoryTheory.Limits.isLimitOfPreserves
-- Module: Mathlib.CategoryTheory.Limits.FullSubcategory
Goal:
J : Type w
inst : Category.{w', w} J
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : HasLimitsOfShape.{w', w, v₁, u₁} J C
inst_4 : PreservesLimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F
inst_5 : F.Full
inst_6 : F.Faithful
G : Functor.{w', v₂, w, u₂} J D
inst_7 : HasLimit G
hG : ∀ (j : J), F.essImage (G.obj j)
⊢ F.essImage (limit G)

Tactic:
⟨limit (Functor.essImage.liftFunctor G F hG),
      ⟨IsLimit.conePointsIsoOfNatIso
        (isLimitOfPreserves F (limit.isLimit _)) (limit.isLimit _)
        (Functor.essImage.liftFunctorCompIso _ _ _)⟩⟩

Premises used: CategoryTheory.Functor.essImage.liftFunctorCompIso, CategoryTheory.Functor.essImage, Nonempty.intro, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.limit, CategoryTheory.Functor.essImage.liftFunctor, Exists.intro, CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso, CategoryTheory.Limits.isLimitOfPreserves
-- Module: Mathlib.CategoryTheory.Limits.FullSubcategory
Goal:
J : Type w
inst : Category.{w', w} J
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : HasLimitsOfShape.{w', w, v₁, u₁} J C
inst_4 : PreservesLimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F
inst_5 : F.Full
inst_6 : F.Faithful
G : Functor.{w', v₂, w, u₂} J D
inst_7 : HasLimit G
hG : ∀ (j : J), F.essImage (G.obj j)
⊢ F.essImage (limit G)

Tactic:
exact ⟨limit (Functor.essImage.liftFunctor G F hG),
      ⟨IsLimit.conePointsIsoOfNatIso
        (isLimitOfPreserves F (limit.isLimit _)) (limit.isLimit _)
        (Functor.essImage.liftFunctorCompIso _ _ _)⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.FullSubcategory
Goal:
J : Type w
inst : Category.{w', w} J
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : HasColimitsOfShape.{w', w, v₁, u₁} J C
inst_4 : PreservesColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F
inst_5 : F.Full
inst_6 : F.Faithful
G : Functor.{w', v₂, w, u₂} J D
inst_7 : HasColimit G
hG : ∀ (j : J), F.essImage (G.obj j)
⊢ F.essImage (colimit G)

Tactic:
⟨colimit (Functor.essImage.liftFunctor G F hG),
      ⟨IsColimit.coconePointsIsoOfNatIso
        (isColimitOfPreserves F (colimit.isColimit _)) (colimit.isColimit _)
        (Functor.essImage.liftFunctorCompIso _ _ _)⟩⟩

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Functor.essImage.liftFunctorCompIso, CategoryTheory.Functor.essImage, Nonempty.intro, CategoryTheory.Limits.colimit, CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso, CategoryTheory.Functor.essImage.liftFunctor, Exists.intro, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.CategoryTheory.Limits.FullSubcategory
Goal:
J : Type w
inst : Category.{w', w} J
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : HasColimitsOfShape.{w', w, v₁, u₁} J C
inst_4 : PreservesColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F
inst_5 : F.Full
inst_6 : F.Faithful
G : Functor.{w', v₂, w, u₂} J D
inst_7 : HasColimit G
hG : ∀ (j : J), F.essImage (G.obj j)
⊢ F.essImage (colimit G)

Tactic:
exact ⟨colimit (Functor.essImage.liftFunctor G F hG),
      ⟨IsColimit.coconePointsIsoOfNatIso
        (isColimitOfPreserves F (colimit.isColimit _)) (colimit.isColimit _)
        (Functor.essImage.liftFunctorCompIso _ _ _)⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
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
H : J ⥤ Functor.{v₂, v, u₂, u} K C
inst_3 : HasLimit H
c : Cone H
j : J
k : K
⊢ CategoryStruct.comp (Y := (limit H).obj k) (NatTrans.app (lift H c) k) (NatTrans.app (π H j) k) = (c.π.app j).app k

Tactic:
congr_app (limit.lift_π c j) k

Premises used: CategoryTheory.congr_app, CategoryTheory.Limits.limit.lift_π