awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.FunctorCategory
Goal:
C : Type u
inst : Category.{v, u} C
D : Type w
inst_1 : Category.{z, w} D
inst_2 : Abelian.{z, w} D
F G : Functor.{v, z, u, w} C D
α : F ⟶ G
X : C
h :
  α.app X =
    CategoryStruct.comp (Y := Functor.obj (Functor.obj (evaluation C D) X) (cokernel (X := kernel α) (kernel.ι α)))
      (Functor.map (Functor.obj (evaluation C D) X) (cokernel.π (kernel.ι α)))
      (CategoryStruct.comp (Y := (Abelian.image α).obj X) (NatTrans.app (coimageImageComparison α) X)
        (Functor.map (Functor.obj (evaluation C D) X) (kernel.ι (cokernel.π α))))
⊢ α.app X =
    CategoryStruct.comp (Y := cokernel (X := (kernel α).obj X) (NatTrans.app (kernel.ι α) X))
      (cokernel.π (NatTrans.app (kernel.ι α) X))
      (CategoryStruct.comp (Y := (Abelian.coimage α).obj X)
        (cokernelComparison (kernel.ι α) (Functor.obj (evaluation C D) X))
        (CategoryStruct.comp (Y := (Abelian.image α).obj X) (NatTrans.app (coimageImageComparison α) X)
          (Functor.map (Functor.obj (evaluation C D) X) (kernel.ι (cokernel.π α)))))

Tactic:
erw [π_comp_cokernelComparison_assoc _ ((evaluation C D).obj X)]

Premises used: CategoryTheory.Limits.π_comp_cokernelComparison_assoc, CategoryTheory.evaluation, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Abelian.FunctorCategory
Goal:
C : Type u
inst : Category.{v, u} C
D : Type w
inst_1 : Category.{z, w} D
inst_2 : Abelian.{z, w} D
F G : Functor.{v, z, u, w} C D
α : F ⟶ G
X : C
rw :
  (CategoryStruct.comp (Y := Abelian.coimage α) (coimage.π α)
        (CategoryStruct.comp (Y := Abelian.image α) (coimageImageComparison α) (image.ι α))).app
    X
| α.app X

Tactic:
rw [← coimage_image_factorisation α]

Premises used: CategoryTheory.Abelian.coimage_image_factorisation
-- Module: Mathlib.CategoryTheory.Abelian.FunctorCategory
Goal:
C : Type u
inst : Category.{v, u} C
D : Type w
inst_1 : Category.{z, w} D
inst_2 : Abelian.{z, w} D
F G : Functor.{v, z, u, w} C D
α : F ⟶ G
X : C
h :
  (CategoryStruct.comp (Y := Abelian.coimage α) (coimage.π α)
          (CategoryStruct.comp (Y := Abelian.image α) (coimageImageComparison α) (image.ι α))).app
      X =
    CategoryStruct.comp (Y := Functor.obj (Functor.obj (evaluation C D) X) (cokernel (X := kernel α) (kernel.ι α)))
      (Functor.map (Functor.obj (evaluation C D) X) (cokernel.π (kernel.ι α)))
      (CategoryStruct.comp (Y := (Abelian.image α).obj X) (NatTrans.app (coimageImageComparison α) X)
        (Functor.map (Functor.obj (evaluation C D) X) (kernel.ι (cokernel.π α))))
⊢ α.app X =
    CategoryStruct.comp (Y := Functor.obj (Functor.obj (evaluation C D) X) (cokernel (X := kernel α) (kernel.ι α)))
      (Functor.map (Functor.obj (evaluation C D) X) (cokernel.π (kernel.ι α)))
      (CategoryStruct.comp (Y := (Abelian.image α).obj X) (NatTrans.app (coimageImageComparison α) X)
        (Functor.map (Functor.obj (evaluation C D) X) (kernel.ι (cokernel.π α))))

Tactic:
conv_lhs => rw [← coimage_image_factorisation α]

Premises used: CategoryTheory.Abelian.coimage_image_factorisation
-- Module: Mathlib.CategoryTheory.Abelian.FunctorCategory
Goal:
C : Type u
inst : Category.{v, u} C
D : Type w
inst_1 : Category.{z, w} D
inst_2 : Abelian.{z, w} D
F G : Functor.{v, z, u, w} C D
α : F ⟶ G
X : C
⊢ (CategoryStruct.comp (Y := Abelian.coimage α) (coimage.π α)
          (CategoryStruct.comp (Y := Abelian.image α) (coimageImageComparison α) (image.ι α))).app
      X =
    CategoryStruct.comp (Y := Functor.obj (Functor.obj (evaluation C D) X) (cokernel (X := kernel α) (kernel.ι α)))
      (Functor.map (Functor.obj (evaluation C D) X) (cokernel.π (kernel.ι α)))
      (CategoryStruct.comp (Y := (Abelian.image α).obj X) (NatTrans.app (coimageImageComparison α) X)
        (Functor.map (Functor.obj (evaluation C D) X) (kernel.ι (cokernel.π α))))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Abelian.FunctorCategory
Goal:
C : Type u
inst : Category.{v, u} C
D : Type w
inst_1 : Category.{z, w} D
inst_2 : Abelian.{z, w} D
F G : Functor.{v, z, u, w} C D
α : F ⟶ G
X : C
⊢ Eq (α := (Abelian.coimage α).obj X ⟶ (Abelian.image α).obj X) (NatTrans.app (coimageImageComparison α) X)
    (Iso.hom (coimageObjIso α X) ≫ coimageImageComparison (α.app X) ≫ Iso.inv (imageObjIso α X))

Tactic:
simp only [coimageImageComparison_app, Iso.hom_inv_id_assoc, Iso.hom_inv_id, Category.assoc,
    Category.comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Abelian.FunctorCategory.coimageImageComparison_app, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id, CategoryTheory.Iso.hom_inv_id_assoc
-- Module: Mathlib.CategoryTheory.Abelian.FunctorCategory
Goal:
C : Type u
inst : Category.{v, u} C
D : Type w
inst_1 : Category.{z, w} D
inst_2 : Abelian.{z, w} D
F G : Functor.{v, z, u, w} C D
α : F ⟶ G
X X_1 : C
rw :
  IsIso (X := (Abelian.coimage α).obj X_1)
    (Iso.hom (coimageObjIso α X_1) ≫ coimageImageComparison (α.app X_1) ≫ Iso.inv (imageObjIso α X_1))
⊢ IsIso (X := (Abelian.coimage α).obj X_1) (Y := (Abelian.image α).obj X_1)
    (NatTrans.app (coimageImageComparison α) X_1)

Tactic:
rw [coimageImageComparison_app']

Premises used: CategoryTheory.Abelian.FunctorCategory.coimageImageComparison_app'
-- Module: Mathlib.CategoryTheory.Abelian.FunctorCategory
Goal:
C : Type u
inst : Category.{v, u} C
D : Type w
inst_1 : Category.{z, w} D
inst_2 : Abelian.{z, w} D
F G : Functor.{v, z, u, w} C D
α : F ⟶ G
X X_1 : C
⊢ IsIso (X := (Abelian.coimage α).obj X_1)
    (Iso.hom (coimageObjIso α X_1) ≫ coimageImageComparison (α.app X_1) ≫ Iso.inv (imageObjIso α X_1))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.FunctorCategory
Goal:
C : Type u
inst : Category.{v, u} C
D : Type w
inst_1 : Category.{z, w} D
inst_2 : Abelian.{z, w} D
F G : Functor.{v, z, u, w} C D
α : F ⟶ G
X : C
⊢ ∀ (X : C),
    IsIso (X := (Abelian.coimage α).obj X) (Y := (Abelian.image α).obj X) (NatTrans.app (coimageImageComparison α) X)

Tactic:
have : ∀ X : C, IsIso ((Abelian.coimageImageComparison α).app X) := by
    intros
    rw [coimageImageComparison_app']
    infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.FunctorCategory
Goal:
C : Type u
inst : Category.{v, u} C
D : Type w
inst_1 : Category.{z, w} D
inst_2 : Abelian.{z, w} D
F G : Functor.{v, z, u, w} C D
α : F ⟶ G
X : C
this :
  ∀ (X : C),
    IsIso (X := (Abelian.coimage α).obj X) (Y := (Abelian.image α).obj X) (NatTrans.app (coimageImageComparison α) X)
⊢ IsIso (X := Abelian.coimage α) (Y := Abelian.image α) (coimageImageComparison α)

Tactic:
apply NatIso.isIso_of_isIso_app

Premises used: CategoryTheory.NatIso.isIso_of_isIso_app
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
J : Type u_2
inst_1 : Category.{v_1, u_2} J
inst_2 : Category.{v_2, u_1} D
inst_3 : HasColimitsOfShape.{v_1, u_2, v, u} J C
inst_4 : HasColimitsOfShape.{v_1, u_2, v_2, u_1} J D
inst_5 : HasExactColimitsOfShape.{v_2, v_1, u_1, u_2} J D
F : Functor.{v, v_2, u, u_1} C D
inst_6 : PreservesFiniteLimits F
inst_7 : ReflectsFiniteLimits F
inst_8 : HasFiniteLimits.{v, u} C
inst_9 : PreservesColimitsOfShape.{v_1, u_2, v, v_2, u, u_1} J F
I : Type
inst_10 : SmallCategory I
inst_11 : FinCategory I
G : I ⥤ Functor.{v_1, v, u_2, u} J C
c : Cone G
hc : IsLimit c
val : IsLimit (F := G ⋙ colim) (mapCone colim c)
⊢ Nonempty (IsLimit (F := G ⋙ colim) (mapCone colim c))

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
J : Type u_2
inst_1 : Category.{v_1, u_2} J
inst_2 : Category.{v_2, u_1} D
inst_3 : HasColimitsOfShape.{v_1, u_2, v, u} J C
inst_4 : HasColimitsOfShape.{v_1, u_2, v_2, u_1} J D
inst_5 : HasExactColimitsOfShape.{v_2, v_1, u_1, u_2} J D
F : Functor.{v, v_2, u, u_1} C D
inst_6 : PreservesFiniteLimits F
inst_7 : ReflectsFiniteLimits F
inst_8 : HasFiniteLimits.{v, u} C
inst_9 : PreservesColimitsOfShape.{v_1, u_2, v, v_2, u, u_1} J F
I : Type
inst_10 : SmallCategory I
inst_11 : FinCategory I
G : I ⥤ Functor.{v_1, v, u_2, u} J C
c : Cone G
hc : IsLimit c
val : IsLimit (F := (G ⋙ colim) ⋙ F) (F.mapCone (mapCone colim c))
⊢ IsLimit (F := G ⋙ colim) (mapCone colim c)

Tactic:
apply isLimitOfReflects F

Premises used: CategoryTheory.Limits.isLimitOfReflects
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
J : Type u_2
inst_1 : Category.{v_1, u_2} J
inst_2 : Category.{v_2, u_1} D
inst_3 : HasColimitsOfShape.{v_1, u_2, v, u} J C
inst_4 : HasColimitsOfShape.{v_1, u_2, v_2, u_1} J D
inst_5 : HasExactColimitsOfShape.{v_2, v_1, u_1, u_2} J D
F : Functor.{v, v_2, u, u_1} C D
inst_6 : PreservesFiniteLimits F
inst_7 : ReflectsFiniteLimits F
inst_8 : HasFiniteLimits.{v, u} C
inst_9 : PreservesColimitsOfShape.{v_1, u_2, v, v_2, u, u_1} J F
I : Type
inst_10 : SmallCategory I
inst_11 : FinCategory I
G : I ⥤ Functor.{v_1, v, u_2, u} J C
c : Cone G
hc : IsLimit c
val :
  Iso (C := Cone (G ⋙ colim ⋙ F))
    (obj (C := Cone (G ⋙ obj (whiskeringRight J C D) F ⋙ colim))
      (Cone.postcompose (Iso.hom (G.isoWhiskerLeft (Iso.symm (preservesColimitNatIso F)))))
      (mapCone (obj (whiskeringRight J C D) F ⋙ colim) c))
    (F.mapCone (mapCone colim c))
⊢ IsLimit (F := (G ⋙ colim) ⋙ F) (F.mapCone (mapCone colim c))

Tactic:
refine (IsLimit.equivOfNatIsoOfIso (isoWhiskerLeft G (preservesColimitNatIso F).symm)
        ((_ ⋙ colim).mapCone c) _ ?_) (isLimitOfPreserves _ hc)

Premises used: CategoryTheory.preservesColimitNatIso, CategoryTheory.Limits.colim, CategoryTheory.Functor.comp, CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.Iso.symm, CategoryTheory.Functor.mapCone, DFunLike.coe, CategoryTheory.Limits.isLimitOfPreserves, CategoryTheory.Limits.IsLimit.equivOfNatIsoOfIso
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
J : Type u_2
inst_1 : Category.{v_1, u_2} J
inst_2 : Category.{v_2, u_1} D
inst_3 : HasColimitsOfShape.{v_1, u_2, v, u} J C
inst_4 : HasColimitsOfShape.{v_1, u_2, v_2, u_1} J D
inst_5 : HasExactColimitsOfShape.{v_2, v_1, u_1, u_2} J D
F : Functor.{v, v_2, u, u_1} C D
inst_6 : PreservesFiniteLimits F
inst_7 : ReflectsFiniteLimits F
inst_8 : HasFiniteLimits.{v, u} C
inst_9 : PreservesColimitsOfShape.{v_1, u_2, v, v_2, u, u_1} J F
I : Type
inst_10 : SmallCategory I
inst_11 : FinCategory I
G : I ⥤ Functor.{v_1, v, u_2, u} J C
c : Cone G
hc : IsLimit c
⊢ Iso (C := Cone (G ⋙ colim ⋙ F))
    (obj (C := Cone (G ⋙ obj (whiskeringRight J C D) F ⋙ colim))
      (Cone.postcompose (Iso.hom (G.isoWhiskerLeft (Iso.symm (preservesColimitNatIso F)))))
      (mapCone (obj (whiskeringRight J C D) F ⋙ colim) c))
    (F.mapCone (mapCone colim c))

Tactic:
exact Cone.ext ((preservesColimitNatIso F).symm.app _)
        fun i ↦ (preservesColimitNatIso F).inv.naturality _

Premises used: CategoryTheory.Limits.Cone.ext
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
J : Type u_2
inst_1 : Category.{v_1, u_1} D
inst_2 : Category.{v_2, u_2} J
inst_3 : HasLimitsOfShape.{v_2, u_2, v, u} J C
inst_4 : HasLimitsOfShape.{v_2, u_2, v_1, u_1} J D
inst_5 : HasExactLimitsOfShape.{v_1, v_2, u_1, u_2} J D
F : Functor.{v, v_1, u, u_1} C D
inst_6 : PreservesFiniteColimits F
inst_7 : ReflectsFiniteColimits F
inst_8 : HasFiniteColimits.{v, u} C
inst_9 : PreservesLimitsOfShape.{v_2, u_2, v, v_1, u, u_1} J F
I : Type
inst_10 : SmallCategory I
inst_11 : FinCategory I
G : I ⥤ Functor.{v_2, v, u_2, u} J C
c : Cocone G
hc : IsColimit c
val : IsColimit (F := G ⋙ lim) (mapCocone lim c)
⊢ Nonempty (IsColimit (F := G ⋙ lim) (mapCocone lim c))

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
J : Type u_2
inst_1 : Category.{v_1, u_1} D
inst_2 : Category.{v_2, u_2} J
inst_3 : HasLimitsOfShape.{v_2, u_2, v, u} J C
inst_4 : HasLimitsOfShape.{v_2, u_2, v_1, u_1} J D
inst_5 : HasExactLimitsOfShape.{v_1, v_2, u_1, u_2} J D
F : Functor.{v, v_1, u, u_1} C D
inst_6 : PreservesFiniteColimits F
inst_7 : ReflectsFiniteColimits F
inst_8 : HasFiniteColimits.{v, u} C
inst_9 : PreservesLimitsOfShape.{v_2, u_2, v, v_1, u, u_1} J F
I : Type
inst_10 : SmallCategory I
inst_11 : FinCategory I
G : I ⥤ Functor.{v_2, v, u_2, u} J C
c : Cocone G
hc : IsColimit c
val : IsColimit (F := (G ⋙ lim) ⋙ F) (F.mapCocone (mapCocone lim c))
⊢ IsColimit (F := G ⋙ lim) (mapCocone lim c)

Tactic:
apply isColimitOfReflects F

Premises used: CategoryTheory.Limits.isColimitOfReflects
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
J : Type u_2
inst_1 : Category.{v_1, u_1} D
inst_2 : Category.{v_2, u_2} J
inst_3 : HasLimitsOfShape.{v_2, u_2, v, u} J C
inst_4 : HasLimitsOfShape.{v_2, u_2, v_1, u_1} J D
inst_5 : HasExactLimitsOfShape.{v_1, v_2, u_1, u_2} J D
F : Functor.{v, v_1, u, u_1} C D
inst_6 : PreservesFiniteColimits F
inst_7 : ReflectsFiniteColimits F
inst_8 : HasFiniteColimits.{v, u} C
inst_9 : PreservesLimitsOfShape.{v_2, u_2, v, v_1, u, u_1} J F
I : Type
inst_10 : SmallCategory I
inst_11 : FinCategory I
G : I ⥤ Functor.{v_2, v, u_2, u} J C
c : Cocone G
hc : IsColimit c
val :
  Iso (C := Cocone (G ⋙ lim ⋙ F))
    (obj (C := Cocone (G ⋙ obj (whiskeringRight J C D) F ⋙ lim))
      (Cocone.precompose (Iso.inv (G.isoWhiskerLeft (Iso.symm (preservesLimitNatIso F)))))
      (mapCocone (obj (whiskeringRight J C D) F ⋙ lim) c))
    (F.mapCocone (mapCocone lim c))
⊢ IsColimit (F := (G ⋙ lim) ⋙ F) (F.mapCocone (mapCocone lim c))

Tactic:
refine (IsColimit.equivOfNatIsoOfIso (isoWhiskerLeft G (preservesLimitNatIso F).symm)
        ((_ ⋙ lim).mapCocone c) _ ?_) (isColimitOfPreserves _ hc)

Premises used: CategoryTheory.Functor.mapCocone, CategoryTheory.Limits.IsColimit.equivOfNatIsoOfIso, CategoryTheory.Functor.comp, CategoryTheory.Limits.lim, CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.preservesLimitNatIso, CategoryTheory.Iso.symm, DFunLike.coe, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
J : Type u_2
inst_1 : Category.{v_1, u_1} D
inst_2 : Category.{v_2, u_2} J
inst_3 : HasLimitsOfShape.{v_2, u_2, v, u} J C
inst_4 : HasLimitsOfShape.{v_2, u_2, v_1, u_1} J D
inst_5 : HasExactLimitsOfShape.{v_1, v_2, u_1, u_2} J D
F : Functor.{v, v_1, u, u_1} C D
inst_6 : PreservesFiniteColimits F
inst_7 : ReflectsFiniteColimits F
inst_8 : HasFiniteColimits.{v, u} C
inst_9 : PreservesLimitsOfShape.{v_2, u_2, v, v_1, u, u_1} J F
I : Type
inst_10 : SmallCategory I
inst_11 : FinCategory I
G : I ⥤ Functor.{v_2, v, u_2, u} J C
c : Cocone G
hc : IsColimit c
val :
  ∀ (i : I),
    Eq (α :=
      (G ⋙ lim ⋙ F).obj i ⟶ Cocone.pt (F := G ⋙ lim ⋙ F) (F.mapCocone (mapCocone lim c) : Cocone ((G ⋙ lim) ⋙ F)))
      (CategoryStruct.comp (Y :=
        Cocone.pt (F := G ⋙ lim ⋙ F)
          (obj (C := Cocone (G ⋙ obj (whiskeringRight J C D) F ⋙ lim))
            (Cocone.precompose (Iso.inv (G.isoWhiskerLeft (Iso.symm (preservesLimitNatIso F)))))
            (mapCocone (obj (whiskeringRight J C D) F ⋙ lim) c)))
        (NatTrans.app
            (Cocone.ι
              (obj (C := Cocone (G ⋙ obj (whiskeringRight J C D) F ⋙ lim))
                (Cocone.precompose (Iso.inv (G.isoWhiskerLeft (Iso.symm (preservesLimitNatIso F)))))
                (mapCocone (obj (whiskeringRight J C D) F ⋙ lim) c)))
            i :
          (G ⋙ lim ⋙ F).obj i ⟶
            obj.{0, v_1, 0, u_1}
              (obj (const I)
                (Cocone.pt (F := G ⋙ lim ⋙ F)
                  (obj (C := Cocone (G ⋙ obj (whiskeringRight J C D) F ⋙ lim))
                    (Cocone.precompose (Iso.inv (G.isoWhiskerLeft (Iso.symm (preservesLimitNatIso F)))))
                    (mapCocone (obj (whiskeringRight J C D) F ⋙ lim) c))))
              i)
        (Iso.hom (Iso.app (Iso.symm (preservesLimitNatIso F)) c.pt)))
      (NatTrans.app (Cocone.ι (F.mapCocone (mapCocone lim c))) i)
⊢ Iso (C := Cocone (G ⋙ lim ⋙ F))
    (obj (C := Cocone (G ⋙ obj (whiskeringRight J C D) F ⋙ lim))
      (Cocone.precompose (Iso.inv (G.isoWhiskerLeft (Iso.symm (preservesLimitNatIso F)))))
      (mapCocone (obj (whiskeringRight J C D) F ⋙ lim) c))
    (F.mapCocone (mapCocone lim c))

Tactic:
refine Cocone.ext ((preservesLimitNatIso F).symm.app _) fun i ↦ ?_

Premises used: CategoryTheory.Limits.Cocone.ext
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
J : Type u_2
inst_1 : Category.{v_1, u_1} D
inst_2 : Category.{v_2, u_2} J
inst_3 : HasLimitsOfShape.{v_2, u_2, v, u} J C
inst_4 : HasLimitsOfShape.{v_2, u_2, v_1, u_1} J D
inst_5 : HasExactLimitsOfShape.{v_1, v_2, u_1, u_2} J D
F : Functor.{v, v_1, u, u_1} C D
inst_6 : PreservesFiniteColimits F
inst_7 : ReflectsFiniteColimits F
inst_8 : HasFiniteColimits.{v, u} C
inst_9 : PreservesLimitsOfShape.{v_2, u_2, v, v_1, u, u_1} J F
I : Type
inst_10 : SmallCategory I
inst_11 : FinCategory I
G : I ⥤ Functor.{v_2, v, u_2, u} J C
c : Cocone G
hc : IsColimit c
i : I
val :
  Eq (α := limit (G.obj i ⋙ F) ⟶ F.obj (limit c.pt))
    (CategoryStruct.comp (Y := limit (c.pt ⋙ F))
        (limMap (whiskerRight (c.ι.app i) F) : limit (G.obj i ⋙ F) ⟶ limit (c.pt ⋙ F))
        (Iso.inv (preservesLimitIso F c.pt) : limit (c.pt ⋙ F) ⟶ F.obj (limit c.pt)) :
      limit (G.obj i ⋙ F) ⟶ F.obj (limit c.pt))
    (CategoryStruct.comp (Y := F.obj (limit (G.obj i))) (Iso.inv (preservesLimitIso F (G.obj i)))
        (F.map (limMap (c.ι.app i))) :
      limit (G.obj i ⋙ F) ⟶ F.obj (limit c.pt))
⊢ Eq (α := F.obj (limit (G.obj i)) ⟶ F.obj (limit c.pt))
    (CategoryStruct.comp (Y := limit (G.obj i ⋙ F))
      (Iso.hom (preservesLimitIso F (G.obj i)) : F.obj (limit (G.obj i)) ⟶ limit (G.obj i ⋙ F))
      (CategoryStruct.comp (Y := limit (c.pt ⋙ F))
          (limMap (whiskerRight (c.ι.app i) F) : limit (G.obj i ⋙ F) ⟶ limit (c.pt ⋙ F))
          (Iso.inv (preservesLimitIso F c.pt) : limit (c.pt ⋙ F) ⟶ F.obj (limit c.pt)) :
        limit (G.obj i ⋙ F) ⟶ F.obj (limit c.pt)))
    (F.map (limMap (c.ι.app i)))

Tactic:
rw [← Iso.eq_inv_comp]

Premises used: CategoryTheory.Iso.eq_inv_comp
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
J : Type u_2
inst_1 : Category.{v_1, u_1} D
inst_2 : Category.{v_2, u_2} J
inst_3 : HasLimitsOfShape.{v_2, u_2, v, u} J C
inst_4 : HasLimitsOfShape.{v_2, u_2, v_1, u_1} J D
inst_5 : HasExactLimitsOfShape.{v_1, v_2, u_1, u_2} J D
F : Functor.{v, v_1, u, u_1} C D
inst_6 : PreservesFiniteColimits F
inst_7 : ReflectsFiniteColimits F
inst_8 : HasFiniteColimits.{v, u} C
inst_9 : PreservesLimitsOfShape.{v_2, u_2, v, v_1, u, u_1} J F
I : Type
inst_10 : SmallCategory I
inst_11 : FinCategory I
G : I ⥤ Functor.{v_2, v, u_2, u} J C
c : Cocone G
hc : IsColimit c
i : I
⊢ Eq (α := limit (G.obj i ⋙ F) ⟶ F.obj (limit c.pt))
    (CategoryStruct.comp (Y := limit (c.pt ⋙ F))
        (limMap (whiskerRight (c.ι.app i) F) : limit (G.obj i ⋙ F) ⟶ limit (c.pt ⋙ F))
        (Iso.inv (preservesLimitIso F c.pt) : limit (c.pt ⋙ F) ⟶ F.obj (limit c.pt)) :
      limit (G.obj i ⋙ F) ⟶ F.obj (limit c.pt))
    (CategoryStruct.comp (Y := F.obj (limit (G.obj i))) (Iso.inv (preservesLimitIso F (G.obj i)))
        (F.map (limMap (c.ι.app i))) :
      limit (G.obj i ⋙ F) ⟶ F.obj (limit c.pt))

Tactic:
(preservesLimitNatIso F).inv.naturality _

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Limits.limit, CategoryTheory.Functor.whiskerRight, CategoryTheory.Limits.IsLimit.map, CategoryTheory.NatTrans.naturality, CategoryTheory.preservesLimitNatIso, CategoryTheory.Limits.limMap, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
J : Type u_2
inst_1 : Category.{v_1, u_1} D
inst_2 : Category.{v_2, u_2} J
inst_3 : HasLimitsOfShape.{v_2, u_2, v, u} J C
inst_4 : HasLimitsOfShape.{v_2, u_2, v_1, u_1} J D
inst_5 : HasExactLimitsOfShape.{v_1, v_2, u_1, u_2} J D
F : Functor.{v, v_1, u, u_1} C D
inst_6 : PreservesFiniteColimits F
inst_7 : ReflectsFiniteColimits F
inst_8 : HasFiniteColimits.{v, u} C
inst_9 : PreservesLimitsOfShape.{v_2, u_2, v, v_1, u, u_1} J F
I : Type
inst_10 : SmallCategory I
inst_11 : FinCategory I
G : I ⥤ Functor.{v_2, v, u_2, u} J C
c : Cocone G
hc : IsColimit c
i : I
⊢ Eq (α := limit (G.obj i ⋙ F) ⟶ F.obj (limit c.pt))
    (CategoryStruct.comp (Y := limit (c.pt ⋙ F))
        (limMap (whiskerRight (c.ι.app i) F) : limit (G.obj i ⋙ F) ⟶ limit (c.pt ⋙ F))
        (Iso.inv (preservesLimitIso F c.pt) : limit (c.pt ⋙ F) ⟶ F.obj (limit c.pt)) :
      limit (G.obj i ⋙ F) ⟶ F.obj (limit c.pt))
    (CategoryStruct.comp (Y := F.obj (limit (G.obj i))) (Iso.inv (preservesLimitIso F (G.obj i)))
        (F.map (limMap (c.ι.app i))) :
      limit (G.obj i ⋙ F) ⟶ F.obj (limit c.pt))

Tactic:
exact (preservesLimitNatIso F).inv.naturality _

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.preservesLimitNatIso, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u_1
J' : Type u_2
inst_1 : Category.{v_1, u_1} J
inst_2 : Category.{v_2, u_2} J'
e : Equivalence.{v_1, v_2, u_1, u_2} J J'
inst_3 : HasColimitsOfShape.{v_1, u_1, v, u} J C
inst_4 : HasExactColimitsOfShape.{v, v_1, u, u_1} J C
⊢ HasExactColimitsOfShape.{v, v_2, u, u_2} J' C

Tactic:
haveI : HasColimitsOfShape J' C := hasColimitsOfShape_of_equivalence e
  ⟨preservesFiniteLimits_of_natIso (Functor.Final.colimIso e.functor)⟩

Premises used: CategoryTheory.Equivalence.functor, CategoryTheory.HasExactColimitsOfShape.mk, CategoryTheory.Functor.Final.colimIso, CategoryTheory.Limits.preservesFiniteLimits_of_natIso
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u_1
inst_1 : Category.{v_1, u_1} J
D : Type u_2
inst_2 : Category.{v_2, u_2} D
e : Equivalence.{v, v_2, u, u_2} C D
inst_3 : HasColimitsOfShape.{v_1, u_1, v, u} J C
inst_4 : HasExactColimitsOfShape.{v, v_1, u, u_1} J C
⊢ HasColimitsOfShape.{v_1, u_1, v_2, u_2} J D

Tactic:
haveI : HasColimitsOfShape J D := Adjunction.hasColimitsOfShape_of_equivalence e.inverse
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u_1
inst_1 : Category.{v_1, u_1} J
D : Type u_2
inst_2 : Category.{v_2, u_2} D
e : Equivalence.{v, v_2, u, u_2} C D
inst_3 : HasColimitsOfShape.{v_1, u_1, v, u} J C
inst_4 : HasExactColimitsOfShape.{v, v_1, u, u_1} J C
this : HasColimitsOfShape.{v_1, u_1, v_2, u_2} J D
⊢ HasExactColimitsOfShape.{v_2, v_1, u_2, u_1} J D

Tactic:
⟨⟨fun _ _ _ => ⟨@fun K => ?_⟩⟩⟩

Premises used: CategoryTheory.Limits.PreservesFiniteLimits.mk, CategoryTheory.HasExactColimitsOfShape.mk, CategoryTheory.Limits.PreservesLimitsOfShape.mk
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u_1
inst_1 : Category.{v_1, u_1} J
D : Type u_2
inst_2 : Category.{v_2, u_2} D
e : Equivalence.{v, v_2, u, u_2} C D
inst_3 : HasColimitsOfShape.{v_1, u_1, v, u} J C
inst_4 : HasExactColimitsOfShape.{v, v_1, u, u_1} J C
this : HasColimitsOfShape.{v_1, u_1, v_2, u_2} J D
refine :
  ∀ (x : Type) (x_1 : SmallCategory x) (x_2 : FinCategory x) (K : x ⥤ Functor.{v_1, v_2, u_1, u_2} J D),
    PreservesLimit K colim
⊢ HasExactColimitsOfShape.{v_2, v_1, u_2, u_1} J D

Tactic:
refine ⟨⟨fun _ _ _ => ⟨@fun K => ?_⟩⟩⟩
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u_1
inst_1 : Category.{v_1, u_1} J
D : Type u_2
inst_2 : Category.{v_2, u_2} D
e : Equivalence.{v, v_2, u, u_2} C D
inst_3 : HasColimitsOfShape.{v_1, u_1, v, u} J C
inst_4 : HasExactColimitsOfShape.{v, v_1, u, u_1} J C
this : HasColimitsOfShape.{v_1, u_1, v_2, u_2} J D
x : Type
x_1 : SmallCategory x
x_2 : FinCategory x
K : x ⥤ Functor.{v_1, v_2, u_1, u_2} J D
⊢ PreservesLimit K colim

Tactic:
preservesLimit_of_natIso K (?_ : e.congrRight.inverse ⋙ colim ⋙ e.functor ≅ colim)

Premises used: CategoryTheory.Limits.preservesLimit_of_natIso