awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.FunctorCategory (goal)
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 := equalizer (Y := cokernel (α.app X)) (cokernel.π (α.app X)) 0)
      (CategoryStruct.comp (Y := coequalizer (X := kernel (α.app X)) (kernel.ι (α.app X)) 0)
        (cokernel.π (kernel.ι (α.app X))) (coimageImageComparison (α.app X)))
      (kernel.ι (cokernel.π (α.app X))) =
    CategoryStruct.comp (Y := equalizer (Y := cokernel (α.app X)) (cokernel.π (α.app X)) 0)
      (cokernel.π (kernel.ι (α.app X)) ≫
        Iso.inv (coimageObjIso α X) ≫ NatTrans.app (coimageImageComparison α) X ≫ Iso.hom (imageObjIso α X))
      (kernel.ι (cokernel.π (α.app X)))
have h : CategoryStruct.comp (Y := equalizer (Y := cokernel (α.app X)) (cokernel.π (α.app X)) 0)
    (CategoryStruct.comp (Y := coequalizer (X := kernel (α.app X)) (kernel.ι (α.app X)) 0)
      (cokernel.π (kernel.ι (α.app X))) (coimageImageComparison (α.app X)))
    (kernel.ι (cokernel.π (α.app X))) =
  CategoryStruct.comp (Y := equalizer (Y := cokernel (α.app X)) (cokernel.π (α.app X)) 0)
    (CategoryStruct.comp (Y := coequalizer (X := kernel (α.app X)) (kernel.ι (α.app X)) 0)
      (cokernel.π (kernel.ι (α.app X)))
      (CategoryStruct.comp (Y := (Abelian.coimage α).obj X)
        (CategoryStruct.comp (Y := cokernel (X := (kernel α).obj X) (NatTrans.app (kernel.ι α) X))
          (cokernel.desc (kernel.ι (α.app X)) (𝟙 (F.obj X) ≫ cokernel.π (NatTrans.app (kernel.ι α) X)) sorry)
          (Iso.inv (PreservesCokernel.iso (Functor.obj (evaluation C D) X) (kernel.ι α))))
        (CategoryStruct.comp (Y := (Abelian.image α).obj X) (NatTrans.app (coimageImageComparison α) X)
          (CategoryStruct.comp (Y := kernel (Y := (cokernel α).obj X) (NatTrans.app (cokernel.π α) X))
            (Iso.hom (PreservesKernel.iso (Functor.obj (evaluation C D) X) (cokernel.π α)))
            (kernel.map (NatTrans.app (cokernel.π α) X) (cokernel.π (α.app X)) (𝟙 (G.obj X))
              (Iso.hom (PreservesCokernel.iso (Functor.obj (evaluation C D) X) α)) sorry)))))
    (kernel.ι (cokernel.π (α.app X)))
Tactic: dsimp [imageObjIso, coimageObjIso, cokernel.map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.FunctorCategory (goal)
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 := equalizer (Y := cokernel (α.app X)) (cokernel.π (α.app X)) 0)
      (CategoryStruct.comp (Y := coequalizer (X := kernel (α.app X)) (kernel.ι (α.app X)) 0)
        (cokernel.π (kernel.ι (α.app X))) (coimageImageComparison (α.app X)))
      (kernel.ι (cokernel.π (α.app X))) =
    CategoryStruct.comp (Y := equalizer (Y := cokernel (α.app X)) (cokernel.π (α.app X)) 0)
      (CategoryStruct.comp (Y := coequalizer (X := kernel (α.app X)) (kernel.ι (α.app X)) 0)
        (cokernel.π (kernel.ι (α.app X)))
        (CategoryStruct.comp (Y := (Abelian.coimage α).obj X)
          (CategoryStruct.comp (Y := cokernel (X := (kernel α).obj X) (NatTrans.app (kernel.ι α) X))
            (cokernel.desc (kernel.ι (α.app X)) (𝟙 (F.obj X) ≫ cokernel.π (NatTrans.app (kernel.ι α) X)) ⋯)
            (Iso.inv (PreservesCokernel.iso (Functor.obj (evaluation C D) X) (kernel.ι α))))
          (CategoryStruct.comp (Y := (Abelian.image α).obj X) (NatTrans.app (coimageImageComparison α) X)
            (CategoryStruct.comp (Y := kernel (Y := (cokernel α).obj X) (NatTrans.app (cokernel.π α) X))
              (Iso.hom (PreservesKernel.iso (Functor.obj (evaluation C D) X) (cokernel.π α)))
              (kernel.map (NatTrans.app (cokernel.π α) X) (cokernel.π (α.app X)) (𝟙 (G.obj X))
                (Iso.hom (PreservesCokernel.iso (Functor.obj (evaluation C D) X) α)) ⋯)))))
      (kernel.ι (cokernel.π (α.app X)))
have h : α.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)
        (CategoryStruct.comp (Y := kernel (Y := (cokernel α).obj X) (NatTrans.app (cokernel.π α) X))
          (kernelComparison (cokernel.π α) (Functor.obj (evaluation C D) X))
          (kernel.ι (NatTrans.app (cokernel.π α) X)))))
Tactic: simp only [coimage_image_factorisation, PreservesKernel.iso_hom, Category.assoc,
    kernel.lift_ι, Category.comp_id, PreservesCokernel.iso_inv,
    cokernel.π_desc_assoc, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.FunctorCategory (goal)
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
⊢ α.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)
          (CategoryStruct.comp (Y := kernel (Y := (cokernel α).obj X) (NatTrans.app (cokernel.π α) X))
            (kernelComparison (cokernel.π α) (Functor.obj (evaluation C D) X))
            (kernel.ι (NatTrans.app (cokernel.π α) X)))))
have h : α.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 [kernelComparison_comp_ι _ ((evaluation C D).obj X)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.FunctorCategory (goal)
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
⊢ α.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.π α)))))
have 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.π α))))
Tactic: erw [π_comp_cokernelComparison_assoc _ ((evaluation C D).obj X)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.FunctorCategory (goal)
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
| α.app X
have rw : (CategoryStruct.comp (Y := Abelian.coimage α) (coimage.π α)
      (CategoryStruct.comp (Y := Abelian.image α) (coimageImageComparison α) (image.ι α))).app
  X
Tactic: rw [← coimage_image_factorisation α]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.FunctorCategory (goal)
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
⊢ α.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.π α))))
have 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.π α))))
Tactic: conv_lhs => rw [← coimage_image_factorisation α]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.FunctorCategory (goal)
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) (Y := (Abelian.image α).obj X_1)
    (NatTrans.app (coimageImageComparison α) X_1)
have rw : IsIso (X := (Abelian.coimage α).obj X_1)
  (Iso.hom (coimageObjIso α X_1) ≫ coimageImageComparison (α.app X_1) ≫ Iso.inv (imageObjIso α X_1))
Tactic: rw [coimageImageComparison_app']
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.FunctorCategory (hypothesis)
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
⊢ IsIso (X := Abelian.coimage α) (Y := Abelian.image α) (coimageImageComparison α)
have this : ∀ (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
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic (goal)
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
⊢ Nonempty (IsLimit (F := G ⋙ colim) (mapCone colim c))
have val : IsLimit (F := G ⋙ colim) (mapCone colim c)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic (goal)
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
⊢ IsLimit (F := G ⋙ colim) (mapCone colim c)
have val : IsLimit (F := (G ⋙ colim) ⋙ F) (F.mapCone (mapCone colim c))
Tactic: apply isLimitOfReflects F
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic (goal)
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
⊢ IsLimit (F := (G ⋙ colim) ⋙ F) (F.mapCone (mapCone colim c))
have 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))
Tactic: refine (IsLimit.equivOfNatIsoOfIso (isoWhiskerLeft G (preservesColimitNatIso F).symm)
        ((_ ⋙ colim).mapCone c) _ ?_) (isLimitOfPreserves _ hc)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic (goal)
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
⊢ Nonempty (IsColimit (F := G ⋙ lim) (mapCocone lim c))
have val : IsColimit (F := G ⋙ lim) (mapCocone lim c)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic (goal)
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
⊢ IsColimit (F := G ⋙ lim) (mapCocone lim c)
have val : IsColimit (F := (G ⋙ lim) ⋙ F) (F.mapCocone (mapCocone lim c))
Tactic: apply isColimitOfReflects F
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic (goal)
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
⊢ IsColimit (F := (G ⋙ lim) ⋙ F) (F.mapCocone (mapCocone lim c))
have 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))
Tactic: refine (IsColimit.equivOfNatIsoOfIso (isoWhiskerLeft G (preservesLimitNatIso F).symm)
        ((_ ⋙ lim).mapCocone c) _ ?_) (isColimitOfPreserves _ hc)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic (goal)
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
⊢ 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))
have 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)
Tactic: refine Cocone.ext ((preservesLimitNatIso F).symm.app _) fun i ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic (goal)
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 (α := (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)
have val : 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: simp only [Functor.comp_obj, lim_obj, Functor.mapCocone_pt, isoWhiskerLeft_inv, Iso.symm_inv,
        Cocone.precompose_obj_pt, whiskeringRight_obj_obj, Functor.const_obj_obj,
        Cocone.precompose_obj_ι, NatTrans.comp_app, whiskerLeft_app, preservesLimitNatIso_hom_app,
        Functor.mapCocone_ι_app, Functor.comp_map, whiskeringRight_obj_map, lim_map, Iso.app_hom,
        Iso.symm_hom, preservesLimitNatIso_inv_app, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic (goal)
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 (α := 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)))
have 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))
Tactic: rw [← Iso.eq_inv_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic (hypothesis)
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
⊢ HasExactColimitsOfShape.{v_2, v_1, u_2, u_1} J D
have this : HasColimitsOfShape.{v_1, u_1, v_2, u_2} J D
Tactic: haveI : HasColimitsOfShape J D := Adjunction.hasColimitsOfShape_of_equivalence e.inverse
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic (goal)
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
have 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
Tactic: refine ⟨⟨fun _ _ _ => ⟨@fun K => ?_⟩⟩⟩