awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
refine : Iso (C := Functor.{v_1, v_2, u_1, u_2} J D ⥤ D) (Equivalence.inverse e.congrRight ⋙ colim ⋙ e.functor) colim
⊢ PreservesLimit K colim

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

Premises used: CategoryTheory.Limits.preservesLimit_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
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
apply :
  Iso (C := Functor.{v_1, v_2, u_1, u_2} J D ⥤ C)
    (obj (Equivalence.functor e.symm.congrRight) (Equivalence.inverse e.congrRight ⋙ colim ⋙ e.functor))
    (obj (Equivalence.functor e.symm.congrRight) colim)
⊢ Iso (C := Functor.{v_1, v_2, u_1, u_2} J D ⥤ D) (Equivalence.inverse e.congrRight ⋙ colim ⋙ e.functor) colim

Tactic:
apply e.symm.congrRight.fullyFaithfulFunctor.preimageIso

Premises used: CategoryTheory.Equivalence.fullyFaithfulFunctor, CategoryTheory.Equivalence.congrRight, CategoryTheory.Functor.FullyFaithful.preimageIso, CategoryTheory.Equivalence.symm
-- 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
⊢ Iso (C := Functor.{v_1, v_2, u_1, u_2} J D ⥤ C)
    (obj (Equivalence.functor e.symm.congrRight) (Equivalence.inverse e.congrRight ⋙ colim ⋙ e.functor))
    (obj (Equivalence.functor e.symm.congrRight) colim)

Tactic:
exact isoWhiskerLeft (_ ⋙ colim) e.unitIso.symm ≪≫ (preservesColimitNatIso e.inverse).symm

Premises used: CategoryTheory.preservesColimitNatIso, CategoryTheory.Equivalence.unitIso, CategoryTheory.Limits.colim, CategoryTheory.Functor.comp, CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.Iso.symm, CategoryTheory.Equivalence.inverse
-- 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 : HasLimitsOfShape.{v_1, u_1, v, u} J C
inst_4 : HasExactLimitsOfShape.{v, v_1, u, u_1} J C
⊢ HasExactLimitsOfShape.{v, v_2, u, u_2} J' C

Tactic:
haveI : HasLimitsOfShape J' C := hasLimitsOfShape_of_equivalence e
  ⟨preservesFiniteColimits_of_natIso (Functor.Initial.limIso e.functor)⟩

Premises used: CategoryTheory.Equivalence.functor, CategoryTheory.HasExactLimitsOfShape.mk, CategoryTheory.Functor.Initial.limIso, CategoryTheory.Limits.preservesFiniteColimits_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 : HasLimitsOfShape.{v_1, u_1, v, u} J C
inst_4 : HasExactLimitsOfShape.{v, v_1, u, u_1} J C
⊢ HasLimitsOfShape.{v_1, u_1, v_2, u_2} J D

Tactic:
haveI : HasLimitsOfShape J D := Adjunction.hasLimitsOfShape_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 : HasLimitsOfShape.{v_1, u_1, v, u} J C
inst_4 : HasExactLimitsOfShape.{v, v_1, u, u_1} J C
this : HasLimitsOfShape.{v_1, u_1, v_2, u_2} J D
⊢ HasExactLimitsOfShape.{v_2, v_1, u_2, u_1} J D

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

Premises used: CategoryTheory.Limits.PreservesFiniteColimits.mk, CategoryTheory.HasExactLimitsOfShape.mk, CategoryTheory.Limits.PreservesColimitsOfShape.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 : HasLimitsOfShape.{v_1, u_1, v, u} J C
inst_4 : HasExactLimitsOfShape.{v, v_1, u, u_1} J C
this : HasLimitsOfShape.{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),
    PreservesColimit K lim
⊢ HasExactLimitsOfShape.{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 : HasLimitsOfShape.{v_1, u_1, v, u} J C
inst_4 : HasExactLimitsOfShape.{v, v_1, u, u_1} J C
this : HasLimitsOfShape.{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
⊢ PreservesColimit K lim

Tactic:
preservesColimit_of_natIso K (?_ : e.congrRight.inverse ⋙ lim ⋙ e.functor ≅ lim)

Premises used: CategoryTheory.Limits.preservesColimit_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 : HasLimitsOfShape.{v_1, u_1, v, u} J C
inst_4 : HasExactLimitsOfShape.{v, v_1, u, u_1} J C
this : HasLimitsOfShape.{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
refine : Iso (C := Functor.{v_1, v_2, u_1, u_2} J D ⥤ D) (Equivalence.inverse e.congrRight ⋙ lim ⋙ e.functor) lim
⊢ PreservesColimit K lim

Tactic:
refine preservesColimit_of_natIso K (?_ : e.congrRight.inverse ⋙ lim ⋙ e.functor ≅ lim)

Premises used: CategoryTheory.Limits.preservesColimit_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 : HasLimitsOfShape.{v_1, u_1, v, u} J C
inst_4 : HasExactLimitsOfShape.{v, v_1, u, u_1} J C
this : HasLimitsOfShape.{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
apply :
  Iso (C := Functor.{v_1, v_2, u_1, u_2} J D ⥤ C)
    (obj (Equivalence.functor e.symm.congrRight) (Equivalence.inverse e.congrRight ⋙ lim ⋙ e.functor))
    (obj (Equivalence.functor e.symm.congrRight) lim)
⊢ Iso (C := Functor.{v_1, v_2, u_1, u_2} J D ⥤ D) (Equivalence.inverse e.congrRight ⋙ lim ⋙ e.functor) lim

Tactic:
apply e.symm.congrRight.fullyFaithfulFunctor.preimageIso

Premises used: CategoryTheory.Equivalence.fullyFaithfulFunctor, CategoryTheory.Equivalence.congrRight, CategoryTheory.Functor.FullyFaithful.preimageIso, CategoryTheory.Equivalence.symm
-- 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 : HasLimitsOfShape.{v_1, u_1, v, u} J C
inst_4 : HasExactLimitsOfShape.{v, v_1, u, u_1} J C
this : HasLimitsOfShape.{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
⊢ Iso (C := Functor.{v_1, v_2, u_1, u_2} J D ⥤ C)
    (obj (Equivalence.functor e.symm.congrRight) (Equivalence.inverse e.congrRight ⋙ lim ⋙ e.functor))
    (obj (Equivalence.functor e.symm.congrRight) lim)

Tactic:
exact isoWhiskerLeft (_ ⋙ lim) e.unitIso.symm ≪≫ (preservesLimitNatIso e.inverse).symm

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Functor.comp, CategoryTheory.Limits.lim, CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.preservesLimitNatIso, CategoryTheory.Iso.symm, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
F : Functor.{v, v'', u, u''} C D
G : Functor.{v'', v, u'', u} D C
adj : F ⊣ G
inst_2 : G.Full
inst_3 : G.Faithful
J : Type u'
inst_4 : Category.{v', u'} J
inst_5 : HasColimitsOfShape.{v', u', v, u} J C
inst_6 : HasColimitsOfShape.{v', u', v'', u''} J D
inst_7 : HasExactColimitsOfShape.{v, v', u, u'} J C
inst_8 : HasFiniteLimits.{v'', u''} D
inst_9 : PreservesFiniteLimits F
K : Type
x : SmallCategory K
x_1 : FinCategory K
H : K ⥤ Functor.{v', v'', u', u''} J D
⊢ PreservesLimitsOfSize.{0, 0, v'', v, u'', u} G

Tactic:
have : PreservesLimitsOfSize.{0, 0} G := adj.rightAdjoint_preservesLimits
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
F : Functor.{v, v'', u, u''} C D
G : Functor.{v'', v, u'', u} D C
adj : F ⊣ G
inst_2 : G.Full
inst_3 : G.Faithful
J : Type u'
inst_4 : Category.{v', u'} J
inst_5 : HasColimitsOfShape.{v', u', v, u} J C
inst_6 : HasColimitsOfShape.{v', u', v'', u''} J D
inst_7 : HasExactColimitsOfShape.{v, v', u, u'} J C
inst_8 : HasFiniteLimits.{v'', u''} D
inst_9 : PreservesFiniteLimits F
K : Type
x : SmallCategory K
x_1 : FinCategory K
H : K ⥤ Functor.{v', v'', u', u''} J D
this : PreservesLimitsOfSize.{0, 0, v'', v, u'', u} G
⊢ PreservesColimitsOfSize.{v', u', v, v'', u, u''} F

Tactic:
have : PreservesColimitsOfSize.{v', u'} F := adj.leftAdjoint_preservesColimits
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
F : Functor.{v, v'', u, u''} C D
G : Functor.{v'', v, u'', u} D C
adj : F ⊣ G
inst_2 : G.Full
inst_3 : G.Faithful
J : Type u'
inst_4 : Category.{v', u'} J
inst_5 : HasColimitsOfShape.{v', u', v, u} J C
inst_6 : HasColimitsOfShape.{v', u', v'', u''} J D
inst_7 : HasExactColimitsOfShape.{v, v', u, u'} J C
inst_8 : HasFiniteLimits.{v'', u''} D
inst_9 : PreservesFiniteLimits F
K : Type
x : SmallCategory K
x_1 : FinCategory K
H : K ⥤ Functor.{v', v'', u', u''} J D
this_1 : PreservesLimitsOfSize.{0, 0, v'', v, u'', u} G
this : PreservesColimitsOfSize.{v', u', v, v'', u, u''} F
e : Iso (C := Functor.{v', v'', u', u''} J D ⥤ D) (obj (whiskeringRight J D C) G ⋙ colim ⋙ F) colim :=
  isoWhiskerLeft (obj (whiskeringRight J D C) G) (preservesColimitNatIso F) ≪≫
    Iso.symm (associator (obj (whiskeringRight J D C) G) (obj (whiskeringRight J C D) F) colim) ≪≫
      isoWhiskerRight (G.whiskeringRightObjCompIso F) colim ≪≫
        isoWhiskerRight (mapIso (whiskeringRight J D D) (asIso adj.counit)) colim ≪≫
          isoWhiskerRight whiskeringRightObjIdIso colim ≪≫ leftUnitor colim
⊢ PreservesLimit H colim

Tactic:
preservesLimit_of_natIso _ e

Premises used: CategoryTheory.Limits.preservesLimit_of_natIso
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
F : Functor.{v, v'', u, u''} C D
G : Functor.{v'', v, u'', u} D C
adj : F ⊣ G
inst_2 : G.Full
inst_3 : G.Faithful
J : Type u'
inst_4 : Category.{v', u'} J
inst_5 : HasColimitsOfShape.{v', u', v, u} J C
inst_6 : HasColimitsOfShape.{v', u', v'', u''} J D
inst_7 : HasExactColimitsOfShape.{v, v', u, u'} J C
inst_8 : HasFiniteLimits.{v'', u''} D
inst_9 : PreservesFiniteLimits F
K : Type
x : SmallCategory K
x_1 : FinCategory K
H : K ⥤ Functor.{v', v'', u', u''} J D
this_1 : PreservesLimitsOfSize.{0, 0, v'', v, u'', u} G
this : PreservesColimitsOfSize.{v', u', v, v'', u, u''} F
e : Iso (C := Functor.{v', v'', u', u''} J D ⥤ D) (obj (whiskeringRight J D C) G ⋙ colim ⋙ F) colim :=
  isoWhiskerLeft (obj (whiskeringRight J D C) G) (preservesColimitNatIso F) ≪≫
    Iso.symm (associator (obj (whiskeringRight J D C) G) (obj (whiskeringRight J C D) F) colim) ≪≫
      isoWhiskerRight (G.whiskeringRightObjCompIso F) colim ≪≫
        isoWhiskerRight (mapIso (whiskeringRight J D D) (asIso adj.counit)) colim ≪≫
          isoWhiskerRight whiskeringRightObjIdIso colim ≪≫ leftUnitor colim
⊢ PreservesLimit H colim

Tactic:
exact preservesLimit_of_natIso _ e

Premises used: CategoryTheory.Limits.preservesLimit_of_natIso
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
F : Functor.{v, v'', u, u''} C D
G : Functor.{v'', v, u'', u} D C
adj : F ⊣ G
inst_2 : F.Full
inst_3 : F.Faithful
J : Type u'
inst_4 : Category.{v', u'} J
inst_5 : HasLimitsOfShape.{v', u', v, u} J C
inst_6 : HasLimitsOfShape.{v', u', v'', u''} J D
inst_7 : HasExactLimitsOfShape.{v'', v', u'', u'} J D
inst_8 : HasFiniteColimits.{v, u} C
inst_9 : PreservesFiniteColimits G
K : Type
x : SmallCategory K
x_1 : FinCategory K
H : K ⥤ Functor.{v', v, u', u} J C
⊢ PreservesLimitsOfSize.{v', u', v'', v, u'', u} G

Tactic:
have : PreservesLimitsOfSize.{v', u'} G := adj.rightAdjoint_preservesLimits
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
F : Functor.{v, v'', u, u''} C D
G : Functor.{v'', v, u'', u} D C
adj : F ⊣ G
inst_2 : F.Full
inst_3 : F.Faithful
J : Type u'
inst_4 : Category.{v', u'} J
inst_5 : HasLimitsOfShape.{v', u', v, u} J C
inst_6 : HasLimitsOfShape.{v', u', v'', u''} J D
inst_7 : HasExactLimitsOfShape.{v'', v', u'', u'} J D
inst_8 : HasFiniteColimits.{v, u} C
inst_9 : PreservesFiniteColimits G
K : Type
x : SmallCategory K
x_1 : FinCategory K
H : K ⥤ Functor.{v', v, u', u} J C
this : PreservesLimitsOfSize.{v', u', v'', v, u'', u} G
⊢ PreservesColimitsOfSize.{0, 0, v, v'', u, u''} F

Tactic:
have : PreservesColimitsOfSize.{0, 0} F := adj.leftAdjoint_preservesColimits
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
F : Functor.{v, v'', u, u''} C D
G : Functor.{v'', v, u'', u} D C
adj : F ⊣ G
inst_2 : F.Full
inst_3 : F.Faithful
J : Type u'
inst_4 : Category.{v', u'} J
inst_5 : HasLimitsOfShape.{v', u', v, u} J C
inst_6 : HasLimitsOfShape.{v', u', v'', u''} J D
inst_7 : HasExactLimitsOfShape.{v'', v', u'', u'} J D
inst_8 : HasFiniteColimits.{v, u} C
inst_9 : PreservesFiniteColimits G
K : Type
x : SmallCategory K
x_1 : FinCategory K
H : K ⥤ Functor.{v', v, u', u} J C
this_1 : PreservesLimitsOfSize.{v', u', v'', v, u'', u} G
this : PreservesColimitsOfSize.{0, 0, v, v'', u, u''} F
e : Iso (C := Functor.{v', v, u', u} J C ⥤ C) (obj (whiskeringRight J C D) F ⋙ lim ⋙ G) lim :=
  isoWhiskerLeft (obj (whiskeringRight J C D) F) (preservesLimitNatIso G) ≪≫
    Iso.symm (associator (obj (whiskeringRight J C D) F) (obj (whiskeringRight J D C) G) lim) ≪≫
      isoWhiskerRight (F.whiskeringRightObjCompIso G) lim ≪≫
        isoWhiskerRight (mapIso (whiskeringRight J C C) (asIso adj.unit).symm) lim ≪≫
          isoWhiskerRight whiskeringRightObjIdIso lim ≪≫ leftUnitor lim
⊢ PreservesColimit H lim

Tactic:
preservesColimit_of_natIso _ e

Premises used: CategoryTheory.Limits.preservesColimit_of_natIso
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
F : Functor.{v, v'', u, u''} C D
G : Functor.{v'', v, u'', u} D C
adj : F ⊣ G
inst_2 : F.Full
inst_3 : F.Faithful
J : Type u'
inst_4 : Category.{v', u'} J
inst_5 : HasLimitsOfShape.{v', u', v, u} J C
inst_6 : HasLimitsOfShape.{v', u', v'', u''} J D
inst_7 : HasExactLimitsOfShape.{v'', v', u'', u'} J D
inst_8 : HasFiniteColimits.{v, u} C
inst_9 : PreservesFiniteColimits G
K : Type
x : SmallCategory K
x_1 : FinCategory K
H : K ⥤ Functor.{v', v, u', u} J C
this_1 : PreservesLimitsOfSize.{v', u', v'', v, u'', u} G
this : PreservesColimitsOfSize.{0, 0, v, v'', u, u''} F
e : Iso (C := Functor.{v', v, u', u} J C ⥤ C) (obj (whiskeringRight J C D) F ⋙ lim ⋙ G) lim :=
  isoWhiskerLeft (obj (whiskeringRight J C D) F) (preservesLimitNatIso G) ≪≫
    Iso.symm (associator (obj (whiskeringRight J C D) F) (obj (whiskeringRight J D C) G) lim) ≪≫
      isoWhiskerRight (F.whiskeringRightObjCompIso G) lim ≪≫
        isoWhiskerRight (mapIso (whiskeringRight J C C) (asIso adj.unit).symm) lim ≪≫
          isoWhiskerRight whiskeringRightObjIdIso lim ≪≫ leftUnitor lim
⊢ PreservesColimit H lim

Tactic:
exact preservesColimit_of_natIso _ e

Premises used: CategoryTheory.Limits.preservesColimit_of_natIso
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts C
inst_2 : AB4OfSize.{max w w', v, u} C
⊢ AB4OfSize.{w, v, u} C

Tactic:
haveI := hasCoproducts_shrink.{w, w'} (C := C)
  ⟨fun J ↦ HasExactColimitsOfShape.of_domain_equivalence C
    (Discrete.equivalence Equiv.ulift : Discrete (ULift.{w'} J) ≌ _)⟩

Premises used: Equiv.ulift, CategoryTheory.Discrete.equivalence, CategoryTheory.AB4OfSize.mk, CategoryTheory.HasExactColimitsOfShape.of_domain_equivalence
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : AB4OfSize.{w, v, u} C
⊢ AB4OfSize.{0, v, u} C

Tactic:
AB4OfSize_shrink C

Premises used: CategoryTheory.AB4OfSize_shrink
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts C
inst_2 : AB4StarOfSize.{max w w', v, u} C
⊢ AB4StarOfSize.{w, v, u} C

Tactic:
haveI := hasProducts_shrink.{w, w'} (C := C)
  ⟨fun J ↦ HasExactLimitsOfShape.of_domain_equivalence C
    (Discrete.equivalence Equiv.ulift : Discrete (ULift.{w'} J) ≌ _)⟩

Premises used: CategoryTheory.HasExactLimitsOfShape.of_domain_equivalence, Equiv.ulift, CategoryTheory.Discrete.equivalence, CategoryTheory.AB4StarOfSize.mk
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{w, v, u} C
inst_2 : AB4StarOfSize.{w, v, u} C
⊢ AB4StarOfSize.{0, v, u} C

Tactic:
AB4StarOfSize_shrink C

Premises used: CategoryTheory.AB4StarOfSize_shrink
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{0, v, u} C
inst_2 : AB4OfSize.{0, v, u} C
⊢ CountableAB4.{v, u} C

Tactic:
⟨inferInstance⟩

Premises used: inferInstance, CategoryTheory.CountableAB4.mk
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{0, v, u} C
inst_2 : AB4StarOfSize.{0, v, u} C
⊢ CountableAB4Star.{v, u} C

Tactic:
⟨inferInstance⟩

Premises used: inferInstance, CategoryTheory.CountableAB4Star.mk
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFilteredColimitsOfSize.{w₂, w₂', v, u} C
inst_2 : UnivLE.{w, w₂}
inst_3 : UnivLE.{w', w₂'}
inst_4 : AB5OfSize.{w₂, w₂', v, u} C
⊢ HasFilteredColimitsOfSize.{w, w', v, u} C

Tactic:
haveI : HasFilteredColimitsOfSize.{w, w'} C := hasFilteredColimitsOfSize_of_univLE.{w}
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFilteredColimitsOfSize.{w₂, w₂', v, u} C
inst_2 : UnivLE.{w, w₂}
inst_3 : UnivLE.{w', w₂'}
inst_4 : AB5OfSize.{w₂, w₂', v, u} C
this : HasFilteredColimitsOfSize.{w, w', v, u} C
ofShape :
  ∀ (J : Type w') [inst_5 : Category.{w, w'} J] [inst_6 : IsFiltered.{w, w'} J],
    HasExactColimitsOfShape.{v, w, u, w'} J C
⊢ AB5OfSize.{w, w', v, u} C

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFilteredColimitsOfSize.{w₂, w₂', v, u} C
inst_2 : UnivLE.{w, w₂}
inst_3 : UnivLE.{w', w₂'}
inst_4 : AB5OfSize.{w₂, w₂', v, u} C
this : HasFilteredColimitsOfSize.{w, w', v, u} C
J : Type w'
ofShape : ∀ [inst_5 : Category.{w, w'} J] [inst_6 : IsFiltered.{w, w'} J], HasExactColimitsOfShape.{v, w, u, w'} J C
⊢ ∀ [inst_5 : Category.{w, w'} J] [inst_6 : IsFiltered.{w, w'} J], HasExactColimitsOfShape.{v, w, u, w'} J C

Tactic:
_
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFilteredColimitsOfSize.{w₂, w₂', v, u} C
inst_2 : UnivLE.{w, w₂}
inst_3 : UnivLE.{w', w₂'}
inst_4 : AB5OfSize.{w₂, w₂', v, u} C
this : HasFilteredColimitsOfSize.{w, w', v, u} C
J : Type w'
inst_5 : Category.{w, w'} J
ofShape : ∀ [inst_6 : IsFiltered.{w, w'} J], HasExactColimitsOfShape.{v, w, u, w'} J C
⊢ ∀ [inst_6 : IsFiltered.{w, w'} J], HasExactColimitsOfShape.{v, w, u, w'} J C

Tactic:
_
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFilteredColimitsOfSize.{w₂, w₂', v, u} C
inst_2 : UnivLE.{w, w₂}
inst_3 : UnivLE.{w', w₂'}
inst_4 : AB5OfSize.{w₂, w₂', v, u} C
this : HasFilteredColimitsOfSize.{w, w', v, u} C
J : Type w'
inst_5 : Category.{w, w'} J
inst_6 : IsFiltered.{w, w'} J
⊢ IsFiltered.{w₂, w₂'} (Shrink.{w₂', w'} (ShrinkHoms.{w'} J))

Tactic:
haveI := IsFiltered.of_equivalence ((ShrinkHoms.equivalence.{w₂} J).trans <|
    Shrink.equivalence.{w₂', w₂} (ShrinkHoms.{w'} J))
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFilteredColimitsOfSize.{w₂, w₂', v, u} C
inst_2 : UnivLE.{w, w₂}
inst_3 : UnivLE.{w', w₂'}
inst_4 : AB5OfSize.{w₂, w₂', v, u} C
this_1 : HasFilteredColimitsOfSize.{w, w', v, u} C
J : Type w'
inst_5 : Category.{w, w'} J
inst_6 : IsFiltered.{w, w'} J
this : IsFiltered.{w₂, w₂'} (Shrink.{w₂', w'} (ShrinkHoms.{w'} J))
⊢ HasExactColimitsOfShape.{v, w, u, w'} J C

Tactic:
HasExactColimitsOfShape.of_domain_equivalence _ ((ShrinkHoms.equivalence.{w₂} J).trans <|
    Shrink.equivalence.{w₂', w₂} (ShrinkHoms.{w'} J)).symm

Premises used: CategoryTheory.ShrinkHoms.equivalence, CategoryTheory.Shrink.equivalence, CategoryTheory.HasExactColimitsOfShape.of_domain_equivalence, CategoryTheory.Equivalence.trans, CategoryTheory.ShrinkHoms, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFilteredColimitsOfSize.{w₂, w₂', v, u} C
inst_2 : UnivLE.{w, w₂}
inst_3 : UnivLE.{w', w₂'}
inst_4 : AB5OfSize.{w₂, w₂', v, u} C
this_1 : HasFilteredColimitsOfSize.{w, w', v, u} C
J : Type w'
inst_5 : Category.{w, w'} J
inst_6 : IsFiltered.{w, w'} J
this : IsFiltered.{w₂, w₂'} (Shrink.{w₂', w'} (ShrinkHoms.{w'} J))
⊢ HasExactColimitsOfShape.{v, w, u, w'} J C

Tactic:
exact HasExactColimitsOfShape.of_domain_equivalence _ ((ShrinkHoms.equivalence.{w₂} J).trans <|
    Shrink.equivalence.{w₂', w₂} (ShrinkHoms.{w'} J)).symm
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFilteredColimitsOfSize.{max w w₂, max w' w₂', v, u} C
inst_2 : AB5OfSize.{max w w₂, max w' w₂', v, u} C
⊢ AB5OfSize.{w, w', v, u} C

Tactic:
AB5OfSize_of_univLE C

Premises used: CategoryTheory.AB5OfSize_of_univLE
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCofilteredLimitsOfSize.{w₂, w₂', v, u} C
inst_2 : UnivLE.{w, w₂}
inst_3 : UnivLE.{w', w₂'}
inst_4 : AB5StarOfSize.{w₂, w₂', v, u} C
⊢ HasCofilteredLimitsOfSize.{w, w', v, u} C

Tactic:
haveI : HasCofilteredLimitsOfSize.{w, w'} C := hasCofilteredLimitsOfSize_of_univLE.{w}