awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasZeroMorphisms.{v_1, u_1} C
X : C
⊢ HasBinaryCoproduct.{v_1, u_1} 0 X

Tactic:
HasColimit.mk ⟨_, binaryCofanZeroLeftIsColimit X⟩

Premises used: CategoryTheory.Limits.HasColimit.mk, CategoryTheory.Limits.binaryCofanZeroLeftIsColimit, CategoryTheory.Limits.ColimitCocone.mk
-- Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasZeroMorphisms.{v_1, u_1} C
X : C
dsimp :
  Eq.{v_1 + 1} (α := X ⟶ X)
    (CategoryStruct.comp (Y := coprod.{v_1, u_1} 0 X) coprod.inr
        (Iso.hom
          (colimit.isoColimitCocone
            { cocone := BinaryCofan.mk 0 (𝟙 X), isColimit := binaryCofanZeroLeftIsColimit X })) :
      X ⟶ X)
    (𝟙 X : X ⟶ X)
⊢ Eq.{v_1 + 1} (α := X ⟶ X)
    (CategoryStruct.comp (Y := coprod.{v_1, u_1} 0 X) (coprod.inr : X ⟶ coprod.{v_1, u_1} 0 X)
      (Iso.hom (zeroCoprodIso X) : coprod.{v_1, u_1} 0 X ⟶ X))
    (𝟙 X)

Tactic:
dsimp [zeroCoprodIso, binaryCofanZeroLeft]

Premises used: CategoryTheory.Limits.zeroCoprodIso, CategoryTheory.Limits.binaryCofanZeroLeft
-- Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasZeroMorphisms.{v_1, u_1} C
X : C
⊢ Eq.{v_1 + 1} (α := X ⟶ X)
    (CategoryStruct.comp (Y := coprod.{v_1, u_1} 0 X) coprod.inr
        (Iso.hom
          (colimit.isoColimitCocone
            { cocone := BinaryCofan.mk 0 (𝟙 X), isColimit := binaryCofanZeroLeftIsColimit X })) :
      X ⟶ X)
    (𝟙 X : X ⟶ X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasZeroMorphisms.{v_1, u_1} C
X : C
⊢ Eq.{v_1 + 1} (α := X ⟶ coprod.{v_1, u_1} 0 X) (Iso.inv (zeroCoprodIso X) : X ⟶ coprod.{v_1, u_1} 0 X)
    (coprod.inr : X ⟶ coprod.{v_1, u_1} 0 X)

Tactic:
rfl

Premises used: rfl, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasZeroMorphisms.{v_1, u_1} C
X : C
⊢ ∀ (s : BinaryCofan.{v_1, u_1} X 0), 𝟙 X ≫ (fun (s : BinaryCofan.{v_1, u_1} X 0) ↦ s.inl) s = s.inl

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasZeroMorphisms.{v_1, u_1} C
X : C
s : BinaryCofan.{v_1, u_1} X 0
m : X ⟶ s.pt
h₁ : 𝟙 X ≫ m = s.inl
h : 0 ≫ m = s.inr
⊢ m = (fun (s : BinaryCofan.{v_1, u_1} X 0) ↦ s.inl) s

Tactic:
simpa using h₁
-- Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasZeroMorphisms.{v_1, u_1} C
X : C
⊢ HasBinaryCoproduct.{v_1, u_1} X 0

Tactic:
HasColimit.mk ⟨_, binaryCofanZeroRightIsColimit X⟩

Premises used: CategoryTheory.Limits.HasColimit.mk, CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Limits.binaryCofanZeroRightIsColimit
-- Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasZeroMorphisms.{v_1, u_1} C
X : C
dsimp :
  Eq.{v_1 + 1} (α := X ⟶ X)
    (CategoryStruct.comp (Y := coprod.{v_1, u_1} X 0) coprod.inl
        (Iso.hom
          (colimit.isoColimitCocone
            { cocone := BinaryCofan.mk (𝟙 X) 0, isColimit := binaryCofanZeroRightIsColimit X })) :
      X ⟶ X)
    (𝟙 X : X ⟶ X)
⊢ Eq.{v_1 + 1} (α := X ⟶ X)
    (CategoryStruct.comp (Y := coprod.{v_1, u_1} X 0) (coprod.inl : X ⟶ coprod.{v_1, u_1} X 0)
      (Iso.hom (coprodZeroIso X) : coprod.{v_1, u_1} X 0 ⟶ X))
    (𝟙 X)

Tactic:
dsimp [coprodZeroIso, binaryCofanZeroRight]

Premises used: CategoryTheory.Limits.binaryCofanZeroRight, CategoryTheory.Limits.coprodZeroIso
-- Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasZeroMorphisms.{v_1, u_1} C
X : C
⊢ Eq.{v_1 + 1} (α := X ⟶ X)
    (CategoryStruct.comp (Y := coprod.{v_1, u_1} X 0) coprod.inl
        (Iso.hom
          (colimit.isoColimitCocone
            { cocone := BinaryCofan.mk (𝟙 X) 0, isColimit := binaryCofanZeroRightIsColimit X })) :
      X ⟶ X)
    (𝟙 X : X ⟶ X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasZeroMorphisms.{v_1, u_1} C
X : C
⊢ Eq.{v_1 + 1} (α := X ⟶ coprod.{v_1, u_1} X 0) (Iso.inv (coprodZeroIso X) : X ⟶ coprod.{v_1, u_1} X 0)
    (coprod.inl : X ⟶ coprod.{v_1, u_1} X 0)

Tactic:
rfl

Premises used: rfl, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasZeroMorphisms.{v_1, u_1} C
X Y : C
inst_3 : HasBinaryProduct.{v_1, u_1} X Y
⊢ HasPullback.{v_1, u_1} (C := C) (X := X) (Y := Y) (Z := 0) 0 0

Tactic:
HasLimit.mk
    ⟨_, isPullbackOfIsTerminalIsProduct _ _ _ _ HasZeroObject.zeroIsTerminal (prodIsProd X Y)⟩

Premises used: isPullbackOfIsTerminalIsProduct, CategoryTheory.Limits.HasZeroObject.zeroIsTerminal, CategoryTheory.Limits.prodIsProd, CategoryTheory.Limits.HasLimit.mk, CategoryTheory.Limits.LimitCone.mk
-- Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasZeroMorphisms.{v_1, u_1} C
X Y : C
inst_3 : HasBinaryProduct.{v_1, u_1} X Y
dsimp :
  Eq.{v_1 + 1} (α := prod.{v_1, u_1} X Y ⟶ X)
    (CategoryStruct.comp (Y := pullback.{v_1, u_1} (X := X) (Y := Y) (Z := 0) 0 0)
        (Iso.inv
          (limit.isoLimitCone
            { cone := PullbackCone.mk (W := prod.{v_1, u_1} X Y) prod.fst prod.snd ⋯,
              isLimit :=
                (isPullbackOfIsTerminalIsProduct 0 0 prod.fst prod.snd HasZeroObject.zeroIsTerminal (prodIsProd X Y) :
                  IsLimit.{0, v_1, 0, u_1} (C := C) (F := cospan (X := X) (Y := Y) (Z := 0) 0 0)
                    (PullbackCone.mk (W := prod.{v_1, u_1} X Y) prod.fst prod.snd ⋯)) }))
        (pullback.fst 0 0) :
      prod.{v_1, u_1} X Y ⟶ X)
    (prod.fst : prod.{v_1, u_1} X Y ⟶ X)
⊢ Eq.{v_1 + 1} (α := prod.{v_1, u_1} X Y ⟶ X)
    (CategoryStruct.comp (Y := pullback.{v_1, u_1} (X := X) (Y := Y) (Z := 0) 0 0) (Iso.inv (pullbackZeroZeroIso X Y))
      (pullback.fst 0 0))
    prod.fst

Tactic:
dsimp [pullbackZeroZeroIso]

Premises used: CategoryTheory.Limits.pullbackZeroZeroIso
-- Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasZeroMorphisms.{v_1, u_1} C
X Y : C
inst_3 : HasBinaryProduct.{v_1, u_1} X Y
⊢ Eq.{v_1 + 1} (α := prod.{v_1, u_1} X Y ⟶ X)
    (CategoryStruct.comp (Y := pullback.{v_1, u_1} (X := X) (Y := Y) (Z := 0) 0 0)
        (Iso.inv
          (limit.isoLimitCone
            { cone := PullbackCone.mk (W := prod.{v_1, u_1} X Y) prod.fst prod.snd ⋯,
              isLimit :=
                (isPullbackOfIsTerminalIsProduct 0 0 prod.fst prod.snd HasZeroObject.zeroIsTerminal (prodIsProd X Y) :
                  IsLimit.{0, v_1, 0, u_1} (C := C) (F := cospan (X := X) (Y := Y) (Z := 0) 0 0)
                    (PullbackCone.mk (W := prod.{v_1, u_1} X Y) prod.fst prod.snd ⋯)) }))
        (pullback.fst 0 0) :
      prod.{v_1, u_1} X Y ⟶ X)
    (prod.fst : prod.{v_1, u_1} X Y ⟶ X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasZeroMorphisms.{v_1, u_1} C
X Y : C
inst_3 : HasBinaryProduct.{v_1, u_1} X Y
dsimp :
  Eq.{v_1 + 1} (α := prod.{v_1, u_1} X Y ⟶ Y)
    (CategoryStruct.comp (Y := pullback.{v_1, u_1} (X := X) (Y := Y) (Z := 0) 0 0)
        (Iso.inv
          (limit.isoLimitCone
            { cone := PullbackCone.mk (W := prod.{v_1, u_1} X Y) prod.fst prod.snd ⋯,
              isLimit :=
                (isPullbackOfIsTerminalIsProduct 0 0 prod.fst prod.snd HasZeroObject.zeroIsTerminal (prodIsProd X Y) :
                  IsLimit.{0, v_1, 0, u_1} (C := C) (F := cospan (X := X) (Y := Y) (Z := 0) 0 0)
                    (PullbackCone.mk (W := prod.{v_1, u_1} X Y) prod.fst prod.snd ⋯)) }))
        (pullback.snd 0 0) :
      prod.{v_1, u_1} X Y ⟶ Y)
    (prod.snd : prod.{v_1, u_1} X Y ⟶ Y)
⊢ Eq.{v_1 + 1} (α := prod.{v_1, u_1} X Y ⟶ Y)
    (CategoryStruct.comp (Y := pullback.{v_1, u_1} (X := X) (Y := Y) (Z := 0) 0 0) (Iso.inv (pullbackZeroZeroIso X Y))
      (pullback.snd 0 0))
    prod.snd

Tactic:
dsimp [pullbackZeroZeroIso]

Premises used: CategoryTheory.Limits.pullbackZeroZeroIso
-- Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasZeroMorphisms.{v_1, u_1} C
X Y : C
inst_3 : HasBinaryProduct.{v_1, u_1} X Y
⊢ Eq.{v_1 + 1} (α := prod.{v_1, u_1} X Y ⟶ Y)
    (CategoryStruct.comp (Y := pullback.{v_1, u_1} (X := X) (Y := Y) (Z := 0) 0 0)
        (Iso.inv
          (limit.isoLimitCone
            { cone := PullbackCone.mk (W := prod.{v_1, u_1} X Y) prod.fst prod.snd ⋯,
              isLimit :=
                (isPullbackOfIsTerminalIsProduct 0 0 prod.fst prod.snd HasZeroObject.zeroIsTerminal (prodIsProd X Y) :
                  IsLimit.{0, v_1, 0, u_1} (C := C) (F := cospan (X := X) (Y := Y) (Z := 0) 0 0)
                    (PullbackCone.mk (W := prod.{v_1, u_1} X Y) prod.fst prod.snd ⋯)) }))
        (pullback.snd 0 0) :
      prod.{v_1, u_1} X Y ⟶ Y)
    (prod.snd : prod.{v_1, u_1} X Y ⟶ Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasZeroMorphisms.{v_1, u_1} C
X Y : C
inst_3 : HasBinaryProduct.{v_1, u_1} X Y
⊢ Eq.{v_1 + 1} (α := pullback.{v_1, u_1} (X := X) (Y := Y) (Z := 0) 0 0 ⟶ X)
    (CategoryStruct.comp (Y := prod.{v_1, u_1} X Y) (Iso.hom (pullbackZeroZeroIso X Y)) prod.fst :
      pullback.{v_1, u_1} (X := X) (Y := Y) (Z := 0) 0 0 ⟶ X)
    (pullback.fst 0 0 : pullback.{v_1, u_1} (X := X) (Y := Y) (Z := 0) 0 0 ⟶ X)

Tactic:
simp [← Iso.eq_inv_comp]

Premises used: CategoryTheory.Iso.eq_inv_comp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasZeroMorphisms.{v_1, u_1} C
X Y : C
inst_3 : HasBinaryProduct.{v_1, u_1} X Y
⊢ Eq.{v_1 + 1} (α := pullback.{v_1, u_1} (X := X) (Y := Y) (Z := 0) 0 0 ⟶ Y)
    (CategoryStruct.comp (Y := prod.{v_1, u_1} X Y) (Iso.hom (pullbackZeroZeroIso X Y)) prod.snd :
      pullback.{v_1, u_1} (X := X) (Y := Y) (Z := 0) 0 0 ⟶ Y)
    (pullback.snd 0 0 : pullback.{v_1, u_1} (X := X) (Y := Y) (Z := 0) 0 0 ⟶ Y)

Tactic:
simp [← Iso.eq_inv_comp]

Premises used: CategoryTheory.Iso.eq_inv_comp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasZeroMorphisms.{v_1, u_1} C
X Y : C
inst_3 : HasBinaryCoproduct.{v_1, u_1} X Y
⊢ HasPushout.{v_1, u_1} (C := C) (X := 0) (Y := X) (Z := Y) 0 0

Tactic:
HasColimit.mk
    ⟨_, isPushoutOfIsInitialIsCoproduct _ _ _ _ HasZeroObject.zeroIsInitial (coprodIsCoprod X Y)⟩

Premises used: CategoryTheory.Limits.HasZeroObject.zeroIsInitial, CategoryTheory.Limits.coprodIsCoprod, isPushoutOfIsInitialIsCoproduct, CategoryTheory.Limits.HasColimit.mk, CategoryTheory.Limits.ColimitCocone.mk
-- Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasZeroMorphisms.{v_1, u_1} C
X Y : C
inst_3 : HasBinaryCoproduct.{v_1, u_1} X Y
dsimp :
  Eq.{v_1 + 1} (α := X ⟶ coprod.{v_1, u_1} X Y)
    (CategoryStruct.comp (Y := pushout.{v_1, u_1} (X := 0) (Y := X) (Z := Y) 0 0) (pushout.inl 0 0)
        (Iso.hom
          (colimit.isoColimitCocone
            { cocone := PushoutCocone.mk (W := coprod.{v_1, u_1} X Y) coprod.inl coprod.inr ⋯,
              isColimit :=
                (isPushoutOfIsInitialIsCoproduct coprod.inl coprod.inr 0 0 HasZeroObject.zeroIsInitial
                    (coprodIsCoprod X Y) :
                  IsColimit.{0, v_1, 0, u_1} (C := C) (F := span (X := 0) (Y := X) (Z := Y) 0 0)
                    (PushoutCocone.mk (W := coprod.{v_1, u_1} X Y) coprod.inl coprod.inr ⋯)) })) :
      X ⟶ coprod.{v_1, u_1} X Y)
    (coprod.inl : X ⟶ coprod.{v_1, u_1} X Y)
⊢ Eq.{v_1 + 1} (α := X ⟶ coprod.{v_1, u_1} X Y)
    (CategoryStruct.comp (Y := pushout.{v_1, u_1} (X := 0) (Y := X) (Z := Y) 0 0) (pushout.inl 0 0)
      (Iso.hom (pushoutZeroZeroIso X Y)))
    coprod.inl

Tactic:
dsimp [pushoutZeroZeroIso]

Premises used: CategoryTheory.Limits.pushoutZeroZeroIso
-- Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasZeroMorphisms.{v_1, u_1} C
X Y : C
inst_3 : HasBinaryCoproduct.{v_1, u_1} X Y
⊢ Eq.{v_1 + 1} (α := X ⟶ coprod.{v_1, u_1} X Y)
    (CategoryStruct.comp (Y := pushout.{v_1, u_1} (X := 0) (Y := X) (Z := Y) 0 0) (pushout.inl 0 0)
        (Iso.hom
          (colimit.isoColimitCocone
            { cocone := PushoutCocone.mk (W := coprod.{v_1, u_1} X Y) coprod.inl coprod.inr ⋯,
              isColimit :=
                (isPushoutOfIsInitialIsCoproduct coprod.inl coprod.inr 0 0 HasZeroObject.zeroIsInitial
                    (coprodIsCoprod X Y) :
                  IsColimit.{0, v_1, 0, u_1} (C := C) (F := span (X := 0) (Y := X) (Z := Y) 0 0)
                    (PushoutCocone.mk (W := coprod.{v_1, u_1} X Y) coprod.inl coprod.inr ⋯)) })) :
      X ⟶ coprod.{v_1, u_1} X Y)
    (coprod.inl : X ⟶ coprod.{v_1, u_1} X Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasZeroMorphisms.{v_1, u_1} C
X Y : C
inst_3 : HasBinaryCoproduct.{v_1, u_1} X Y
dsimp :
  Eq.{v_1 + 1} (α := Y ⟶ coprod.{v_1, u_1} X Y)
    (CategoryStruct.comp (Y := pushout.{v_1, u_1} (X := 0) (Y := X) (Z := Y) 0 0) (pushout.inr 0 0)
        (Iso.hom
          (colimit.isoColimitCocone
            { cocone := PushoutCocone.mk (W := coprod.{v_1, u_1} X Y) coprod.inl coprod.inr ⋯,
              isColimit :=
                (isPushoutOfIsInitialIsCoproduct coprod.inl coprod.inr 0 0 HasZeroObject.zeroIsInitial
                    (coprodIsCoprod X Y) :
                  IsColimit.{0, v_1, 0, u_1} (C := C) (F := span (X := 0) (Y := X) (Z := Y) 0 0)
                    (PushoutCocone.mk (W := coprod.{v_1, u_1} X Y) coprod.inl coprod.inr ⋯)) })) :
      Y ⟶ coprod.{v_1, u_1} X Y)
    (coprod.inr : Y ⟶ coprod.{v_1, u_1} X Y)
⊢ Eq.{v_1 + 1} (α := Y ⟶ coprod.{v_1, u_1} X Y)
    (CategoryStruct.comp (Y := pushout.{v_1, u_1} (X := 0) (Y := X) (Z := Y) 0 0) (pushout.inr 0 0)
      (Iso.hom (pushoutZeroZeroIso X Y)))
    coprod.inr

Tactic:
dsimp [pushoutZeroZeroIso]

Premises used: CategoryTheory.Limits.pushoutZeroZeroIso
-- Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasZeroMorphisms.{v_1, u_1} C
X Y : C
inst_3 : HasBinaryCoproduct.{v_1, u_1} X Y
⊢ Eq.{v_1 + 1} (α := Y ⟶ coprod.{v_1, u_1} X Y)
    (CategoryStruct.comp (Y := pushout.{v_1, u_1} (X := 0) (Y := X) (Z := Y) 0 0) (pushout.inr 0 0)
        (Iso.hom
          (colimit.isoColimitCocone
            { cocone := PushoutCocone.mk (W := coprod.{v_1, u_1} X Y) coprod.inl coprod.inr ⋯,
              isColimit :=
                (isPushoutOfIsInitialIsCoproduct coprod.inl coprod.inr 0 0 HasZeroObject.zeroIsInitial
                    (coprodIsCoprod X Y) :
                  IsColimit.{0, v_1, 0, u_1} (C := C) (F := span (X := 0) (Y := X) (Z := Y) 0 0)
                    (PushoutCocone.mk (W := coprod.{v_1, u_1} X Y) coprod.inl coprod.inr ⋯)) })) :
      Y ⟶ coprod.{v_1, u_1} X Y)
    (coprod.inr : Y ⟶ coprod.{v_1, u_1} X Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasZeroMorphisms.{v_1, u_1} C
X Y : C
inst_3 : HasBinaryCoproduct.{v_1, u_1} X Y
⊢ Eq.{v_1 + 1} (α := X ⟶ pushout.{v_1, u_1} (X := 0) (Y := X) (Z := Y) 0 0)
    (CategoryStruct.comp (Y := coprod.{v_1, u_1} X Y) coprod.inl (Iso.inv (pushoutZeroZeroIso X Y)) :
      X ⟶ pushout.{v_1, u_1} (X := 0) (Y := X) (Z := Y) 0 0)
    (pushout.inl 0 0 : X ⟶ pushout.{v_1, u_1} (X := 0) (Y := X) (Z := Y) 0 0)

Tactic:
simp [Iso.comp_inv_eq]

Premises used: CategoryTheory.Iso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasZeroMorphisms.{v_1, u_1} C
X Y : C
inst_3 : HasBinaryCoproduct.{v_1, u_1} X Y
⊢ Eq.{v_1 + 1} (α := Y ⟶ pushout.{v_1, u_1} (X := 0) (Y := X) (Z := Y) 0 0)
    (CategoryStruct.comp (Y := coprod.{v_1, u_1} X Y) coprod.inr (Iso.inv (pushoutZeroZeroIso X Y)) :
      Y ⟶ pushout.{v_1, u_1} (X := 0) (Y := X) (Z := Y) 0 0)
    (pushout.inr 0 0 : Y ⟶ pushout.{v_1, u_1} (X := 0) (Y := X) (Z := Y) 0 0)

Tactic:
simp [Iso.comp_inv_eq]

Premises used: CategoryTheory.Iso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.Limits.Creates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : CreatesLimit K F
c : Cone (K ⋙ F)
t : IsLimit c
j : J
⊢ F.map ((liftLimit t).π.app j) = ConeMorphism.hom (Iso.hom (liftedLimitMapsToOriginal t)) ≫ c.π.app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Creates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : CreatesLimit K F
c : Cone (K ⋙ F)
t : IsLimit c
j : J
rw :
  (CategoryStruct.comp (Y := F.mapCone (liftLimit t)) (Iso.inv (liftedLimitMapsToOriginal t))
          (Iso.hom (liftedLimitMapsToOriginal t))).hom ≫
      c.π.app j =
    c.π.app j
⊢ ConeMorphism.hom (Iso.inv (liftedLimitMapsToOriginal t)) ≫ F.map ((liftLimit t).π.app j) = c.π.app j

Tactic:
rw [show F.map ((liftLimit t).π.app j) = (liftedLimitMapsToOriginal t).hom.hom ≫ c.π.app j
    from (by simp), ← Category.assoc, ← Cone.category_comp_hom]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Cone.category_comp_hom
-- Module: Mathlib.CategoryTheory.Limits.Creates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : CreatesLimit K F
c : Cone (K ⋙ F)
t : IsLimit c
j : J
⊢ (CategoryStruct.comp (Y := F.mapCone (liftLimit t)) (Iso.inv (liftedLimitMapsToOriginal t))
          (Iso.hom (liftedLimitMapsToOriginal t))).hom ≫
      c.π.app j =
    c.π.app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Creates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : CreatesLimit K F
c : Cone (K ⋙ F)
t : IsLimit c
j : J
rw :
  ConeMorphism.hom (Iso.hom (liftedLimitMapsToOriginal t)) ≫
      ConeMorphism.hom (Iso.inv (liftedLimitMapsToOriginal t)) ≫ F.map ((liftLimit t).π.app j) =
    F.map ((liftLimit t).π.app j)
⊢ ConeMorphism.hom (Iso.hom (liftedLimitMapsToOriginal t)) ≫ c.π.app j = F.map ((liftLimit t).π.app j)

Tactic:
rw [← liftedLimitMapsToOriginal_inv_map_π (t := t)]

Premises used: CategoryTheory.liftedLimitMapsToOriginal_inv_map_π
-- Module: Mathlib.CategoryTheory.Limits.Creates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : CreatesLimit K F
c : Cone (K ⋙ F)
t : IsLimit c
j : J
⊢ ConeMorphism.hom (Iso.hom (liftedLimitMapsToOriginal t)) ≫
      ConeMorphism.hom (Iso.inv (liftedLimitMapsToOriginal t)) ≫ F.map ((liftLimit t).π.app j) =
    F.map ((liftLimit t).π.app j)

Tactic:
simp only [Functor.mapCone_pt, Functor.comp_obj, ← Category.assoc, ← Cone.category_comp_hom,
    Iso.hom_inv_id, Cone.category_id_hom, Category.id_comp, Functor.const_obj_obj]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Limits.Cone.category_id_hom, CategoryTheory.Functor.mapCone_pt, CategoryTheory.Limits.Cone.category_comp_hom, CategoryTheory.Functor.const_obj_obj, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Creates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : HasLimit (K ⋙ F)
inst_4 : CreatesLimit K F
⊢ HasLimit K

Tactic:
HasLimit.mk
    { cone := liftLimit (limit.isLimit (K ⋙ F))
      isLimit := liftedLimitIsLimit _ }

Premises used: CategoryTheory.liftLimit, CategoryTheory.Functor.comp, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.HasLimit.mk, CategoryTheory.liftedLimitIsLimit, CategoryTheory.Limits.LimitCone.mk
-- Module: Mathlib.CategoryTheory.Limits.Creates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : HasLimitsOfShape.{w', w, v₂, u₂} J D
inst_4 : CreatesLimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F
⊢ HasLimitsOfShape.{w', w, v₁, u₁} J C

Tactic:
⟨fun G => hasLimit_of_created G F⟩

Premises used: CategoryTheory.hasLimit_of_created, CategoryTheory.Limits.HasLimitsOfShape.mk
-- Module: Mathlib.CategoryTheory.Limits.Creates
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
inst_2 : HasLimitsOfSize.{w, w', v₂, u₂} D
inst_3 : CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
⊢ HasLimitsOfSize.{w, w', v₁, u₁} C

Tactic:
⟨fun _ _ => hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape F⟩

Premises used: CategoryTheory.Limits.HasLimitsOfSize.mk, CategoryTheory.hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape
-- Module: Mathlib.CategoryTheory.Limits.Creates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : HasColimit (K ⋙ F)
inst_4 : CreatesColimit K F
⊢ HasColimit K

Tactic:
HasColimit.mk
    { cocone := liftColimit (colimit.isColimit (K ⋙ F))
      isColimit := liftedColimitIsColimit _ }

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.HasColimit.mk, CategoryTheory.liftedColimitIsColimit, CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.liftColimit
-- Module: Mathlib.CategoryTheory.Limits.Creates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : HasColimitsOfShape.{w', w, v₂, u₂} J D
inst_4 : CreatesColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F
⊢ HasColimitsOfShape.{w', w, v₁, u₁} J C

Tactic:
⟨fun G => hasColimit_of_created G F⟩

Premises used: CategoryTheory.Limits.HasColimitsOfShape.mk, CategoryTheory.hasColimit_of_created