awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X Y : C
h : IsIso.{v, u} (C := C) (X := X) (Y := Y) 0
h' : (X ≅ 0) × (Y ≅ 0) := (isIsoZeroEquivIsoZero X Y : (a : IsIso 0) → (X ≅ 0) × (Y ≅ 0)) h
⊢ IsZero.{v, u} X ∧ IsZero.{v, u} Y

Tactic:
exact ⟨(isZero_zero _).of_iso h'.1, (isZero_zero _).of_iso h'.2⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X Y : C
hX : IsZero.{v, u} X
hY : IsZero.{v, u} Y
⊢ IsIso.{v, u} (C := C) (X := X) (Y := Y) 0

Tactic:
(isIsoZeroEquivIsoZero _ _).symm ⟨hX.isoZero, hY.isoZero⟩

Premises used: Prod.mk, CategoryTheory.Limits.isIsoZeroEquivIsoZero, Equiv.symm, DFunLike.coe, CategoryTheory.Limits.IsZero.isoZero
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X Y : C
hX : IsZero.{v, u} X
hY : IsZero.{v, u} Y
⊢ IsIso.{v, u} (C := C) (X := X) (Y := Y) 0

Tactic:
exact (isIsoZeroEquivIsoZero _ _).symm ⟨hX.isoZero, hY.isoZero⟩

Premises used: Prod.mk, CategoryTheory.Limits.isIsoZeroEquivIsoZero, Equiv.symm, DFunLike.coe, CategoryTheory.Limits.IsZero.isoZero
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X Y : C
f : X ⟶ Y
i : X ≅ 0
j : Y ≅ 0
rw : IsIso.{v, u} (C := C) (X := X) (Y := Y) 0
⊢ IsIso f

Tactic:
rw [zero_of_source_iso_zero f i]

Premises used: CategoryTheory.Limits.zero_of_source_iso_zero
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X Y : C
f : X ⟶ Y
i : X ≅ 0
j : Y ≅ 0
⊢ IsIso.{v, u} (C := C) (X := X) (Y := Y) 0

Tactic:
(isIsoZeroEquivIsoZero _ _).invFun ⟨i, j⟩

Premises used: Prod.mk, CategoryTheory.Limits.isIsoZeroEquivIsoZero, Equiv.invFun
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X Y : C
f : X ⟶ Y
i : X ≅ 0
j : Y ≅ 0
⊢ IsIso.{v, u} (C := C) (X := X) (Y := Y) 0

Tactic:
exact (isIsoZeroEquivIsoZero _ _).invFun ⟨i, j⟩

Premises used: Prod.mk, CategoryTheory.Limits.isIsoZeroEquivIsoZero, Equiv.invFun
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasInitial.{v, u} C
refine : ∀ (X : C) (f : X ⟶ initial.{v, u} C), f = default
⊢ HasZeroObject.{v, u} C

Tactic:
refine ⟨⟨⊥_ C, fun X => ⟨⟨⟨0⟩, by cat_disch⟩⟩, fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasInitial.{v, u} C
X : C
f : X ⟶ initial.{v, u} C
⊢ f = f ≫ 𝟙 (initial.{v, u} C)

Tactic:
(Category.comp_id _).symm

Premises used: CategoryTheory.Category.comp_id, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasInitial.{v, u} C
X : C
f : X ⟶ initial.{v, u} C
h : Eq.{v + 1} (α := initial.{v, u} C ⟶ initial.{v, u} C) (𝟙 (initial.{v, u} C)) 0
⊢ f ≫ 𝟙 (initial.{v, u} C) = f ≫ 0

Tactic:
congr!
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasInitial.{v, u} C
X : C
f : X ⟶ initial.{v, u} C
⊢ Eq.{v + 1} (α := initial.{v, u} C ⟶ initial.{v, u} C) (𝟙 (initial.{v, u} C)) 0

Tactic:
subsingleton
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasInitial.{v, u} C
X : C
f : X ⟶ initial.{v, u} C
⊢ Eq (α := X ⟶ initial.{v, u} C) (f ≫ 0) 0

Tactic:
HasZeroMorphisms.comp_zero _ _

Premises used: CategoryTheory.Limits.HasZeroMorphisms.comp_zero
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasInitial.{v, u} C
X : C
f : X ⟶ initial.{v, u} C
f₁ : f ≫ 𝟙 (initial.{v, u} C) = f ≫ 0
⊢ f = default

Tactic:
calc
    f = f ≫ 𝟙 _ := (Category.comp_id _).symm
    _ = f ≫ 0 := by congr!; subsingleton
    _ = 0 := HasZeroMorphisms.comp_zero _ _

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Category.comp_id, Eq.symm, CategoryTheory.Limits.HasZeroMorphisms.comp_zero
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasTerminal.{v, u} C
refine : ∀ (X : C) (f : terminal.{v, u} C ⟶ X), f = default
⊢ HasZeroObject.{v, u} C

Tactic:
refine ⟨⟨⊤_ C, fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩, fun X => ⟨⟨⟨0⟩, by cat_disch⟩⟩⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasTerminal.{v, u} C
X : C
f : terminal.{v, u} C ⟶ X
⊢ f = 𝟙 (terminal.{v, u} C) ≫ f

Tactic:
(Category.id_comp _).symm

Premises used: Eq.symm, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasTerminal.{v, u} C
X : C
f : terminal.{v, u} C ⟶ X
h : Eq.{v + 1} (α := terminal.{v, u} C ⟶ terminal.{v, u} C) (𝟙 (terminal.{v, u} C)) 0
⊢ 𝟙 (terminal.{v, u} C) ≫ f = 0 ≫ f

Tactic:
congr!
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasTerminal.{v, u} C
X : C
f : terminal.{v, u} C ⟶ X
⊢ Eq.{v + 1} (α := terminal.{v, u} C ⟶ terminal.{v, u} C) (𝟙 (terminal.{v, u} C)) 0

Tactic:
subsingleton
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasTerminal.{v, u} C
X : C
f : terminal.{v, u} C ⟶ X
⊢ Eq (α := terminal.{v, u} C ⟶ X) (0 ≫ f) 0

Tactic:
zero_comp

Premises used: CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasTerminal.{v, u} C
X : C
f : terminal.{v, u} C ⟶ X
f₁ : 𝟙 (terminal.{v, u} C) ≫ f = 0 ≫ f
⊢ f = default

Tactic:
calc
    f = 𝟙 _ ≫ f := (Category.id_comp _).symm
    _ = 0 ≫ f := by congr!; subsingleton
    _ = 0 := zero_comp

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.zero_comp, Eq.symm, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_2 : HasImage f
inst_3 : Epi (Y := image f) (factorThruImage f)
h : f ≫ g = 0
⊢ CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f ≫ g) = 0

Tactic:
simp [h]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_2 : HasImage g
h : f ≫ g = 0
⊢ CategoryStruct.comp (Y := image g) (f ≫ factorThruImage g) (image.ι g) = 0

Tactic:
simp [h]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasZeroObject.{v, u} C
X Y : C
⊢ HasImage.{v, u} (C := C) (X := X) (Y := Y) 0

Tactic:
HasImage.mk <| imageFactorisationZero _ _

Premises used: CategoryTheory.Limits.HasImage.mk, CategoryTheory.Limits.imageFactorisationZero
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X Y : C
inst_3 : HasImage.{v, u} (C := C) (X := X) (Y := Y) 0
rw :
  Eq.{v + 1} (α := image.{v, u} (X := X) (Y := Y) 0 ⟶ Y)
    (CategoryStruct.comp (Y := MonoFactorisation.I.{v, u} (f := 0) (monoFactorisationZero X Y))
      (lift (monoFactorisationZero X Y)) (MonoFactorisation.m (monoFactorisationZero X Y)))
    0
⊢ Eq.{v + 1} (α := image.{v, u} (X := X) (Y := Y) 0 ⟶ Y) (ι 0) 0

Tactic:
rw [← image.lift_fac (monoFactorisationZero X Y)]

Premises used: CategoryTheory.Limits.image.lift_fac, CategoryTheory.Limits.monoFactorisationZero
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X Y : C
inst_3 : HasImage.{v, u} (C := C) (X := X) (Y := Y) 0
⊢ Eq.{v + 1} (α := image.{v, u} (X := X) (Y := Y) 0 ⟶ Y)
    (CategoryStruct.comp (Y := MonoFactorisation.I.{v, u} (f := 0) (monoFactorisationZero X Y))
      (lift (monoFactorisationZero X Y)) (MonoFactorisation.m (monoFactorisationZero X Y)))
    0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasEqualizers.{v, u} C
X Y : C
f : X ⟶ Y
h : f = 0
inst_4 : HasImage f
rw : Eq (α := image f ⟶ Y) (CategoryStruct.comp (Y := image.{v, u} (X := X) (Y := Y) 0) (Iso.hom (eqToIso h)) (ι 0)) 0
⊢ Eq (α := image f ⟶ Y) (ι f) 0

Tactic:
rw [image.eq_fac h]

Premises used: CategoryTheory.Limits.image.eq_fac
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasEqualizers.{v, u} C
X Y : C
f : X ⟶ Y
h : f = 0
inst_4 : HasImage f
⊢ Eq (α := image f ⟶ Y) (CategoryStruct.comp (Y := image.{v, u} (X := X) (Y := Y) 0) (Iso.hom (eqToIso h)) (ι 0)) 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
β : Type u'
inst_2 : HasZeroMorphisms.{v, u} C
f : β → C
inst_3 : HasColimit.{u', u', v, u} (Discrete.functor f)
b : β
⊢ IsSplitMono.{v, u} (Y := sigmaObj.{u', v, u} f) (Sigma.ι f b)

Tactic:
IsSplitMono.mk' { retraction := Sigma.desc <| Pi.single b (𝟙 _) }

Premises used: CategoryTheory.SplitMono.mk, CategoryTheory.CategoryStruct.id, Pi.single, CategoryTheory.IsSplitMono.mk', CategoryTheory.Limits.Sigma.desc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
β : Type u'
inst_2 : HasZeroMorphisms.{v, u} C
f : β → C
inst_3 : HasColimit.{u', u', v, u} (Discrete.functor f)
b : β
⊢ IsSplitMono.{v, u} (Y := sigmaObj.{u', v, u} f) (Sigma.ι f b)

Tactic:
exact IsSplitMono.mk' { retraction := Sigma.desc <| Pi.single b (𝟙 _) }

Premises used: CategoryTheory.SplitMono.mk, CategoryTheory.CategoryStruct.id, Pi.single, CategoryTheory.IsSplitMono.mk', CategoryTheory.Limits.Sigma.desc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
β : Type u'
inst_2 : HasZeroMorphisms.{v, u} C
f : β → C
inst_3 : HasColimit.{u', u', v, u} (Discrete.functor f)
b : β
⊢ IsSplitMono.{v, u} (Y := sigmaObj.{u', v, u} f) (Sigma.ι f b)

Tactic:
classical exact IsSplitMono.mk' { retraction := Sigma.desc <| Pi.single b (𝟙 _) }
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
β : Type u'
inst_2 : HasZeroMorphisms.{v, u} C
f : β → C
inst_3 : HasLimit.{u', u', v, u} (Discrete.functor f)
b : β
⊢ IsSplitEpi.{v, u} (X := piObj.{u', v, u} f) (Pi.π f b)

Tactic:
IsSplitEpi.mk' { section_ := Pi.lift <| Pi.single b (𝟙 _) }

Premises used: CategoryTheory.CategoryStruct.id, Pi.single, CategoryTheory.SplitEpi.mk, CategoryTheory.Limits.Pi.lift, CategoryTheory.IsSplitEpi.mk'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
β : Type u'
inst_2 : HasZeroMorphisms.{v, u} C
f : β → C
inst_3 : HasLimit.{u', u', v, u} (Discrete.functor f)
b : β
⊢ IsSplitEpi.{v, u} (X := piObj.{u', v, u} f) (Pi.π f b)

Tactic:
exact IsSplitEpi.mk' { section_ := Pi.lift <| Pi.single b (𝟙 _) }

Premises used: CategoryTheory.CategoryStruct.id, Pi.single, CategoryTheory.SplitEpi.mk, CategoryTheory.Limits.Pi.lift, CategoryTheory.IsSplitEpi.mk'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
β : Type u'
inst_2 : HasZeroMorphisms.{v, u} C
f : β → C
inst_3 : HasLimit.{u', u', v, u} (Discrete.functor f)
b : β
⊢ IsSplitEpi.{v, u} (X := piObj.{u', v, u} f) (Pi.π f b)

Tactic:
classical exact IsSplitEpi.mk' { section_ := Pi.lift <| Pi.single b (𝟙 _) }
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroMorphisms.{v, u} C
X Y : C
inst_3 : HasColimit.{0, 0, v, u} (pair X Y)
⊢ IsSplitMono.{v, u} (C := C) (X := X) (Y := coprod.{v, u} X Y) coprod.inl

Tactic:
IsSplitMono.mk' { retraction := coprod.desc (𝟙 X) 0 }

Premises used: CategoryTheory.Limits.coprod.desc, CategoryTheory.SplitMono.mk, CategoryTheory.CategoryStruct.id, CategoryTheory.IsSplitMono.mk', OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroMorphisms.{v, u} C
X Y : C
inst_3 : HasColimit.{0, 0, v, u} (pair X Y)
⊢ IsSplitMono.{v, u} (C := C) (X := Y) (Y := coprod.{v, u} X Y) coprod.inr

Tactic:
IsSplitMono.mk' { retraction := coprod.desc 0 (𝟙 Y) }

Premises used: CategoryTheory.Limits.coprod.desc, CategoryTheory.SplitMono.mk, CategoryTheory.CategoryStruct.id, CategoryTheory.IsSplitMono.mk', OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroMorphisms.{v, u} C
X Y : C
inst_3 : HasLimit.{0, 0, v, u} (pair X Y)
⊢ IsSplitEpi.{v, u} (C := C) (X := prod.{v, u} X Y) prod.fst

Tactic:
IsSplitEpi.mk' { section_ := prod.lift (𝟙 X) 0 }

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.SplitEpi.mk, OfNat.ofNat, CategoryTheory.IsSplitEpi.mk', CategoryTheory.Limits.prod.lift
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroMorphisms.{v, u} C
X Y : C
inst_3 : HasLimit.{0, 0, v, u} (pair X Y)
⊢ IsSplitEpi.{v, u} (C := C) (X := prod.{v, u} X Y) prod.snd

Tactic:
IsSplitEpi.mk' { section_ := prod.lift 0 (𝟙 Y) }

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.SplitEpi.mk, OfNat.ofNat, CategoryTheory.IsSplitEpi.mk', CategoryTheory.Limits.prod.lift
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasZeroObject.{v, u} C
F : Functor.{v', v, u', u} D C
c : Cone F
hc : IsLimit c
hF : IsZero F
⊢ IsZero.{v, u} c.pt

Tactic:
(isZero_zero C).of_iso (IsLimit.conePointUniqueUpToIso hc
    (IsLimit.ofIsZero (Cone.mk 0 0) hF (isZero_zero C)))

Premises used: CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso, CategoryTheory.Limits.isZero_zero, CategoryTheory.Limits.IsZero.of_iso, OfNat.ofNat, CategoryTheory.Limits.IsLimit.ofIsZero, CategoryTheory.Limits.Cone.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasZeroObject.{v, u} C
F : Functor.{v', v, u', u} D C
c : Cocone F
hc : IsColimit c
hF : IsZero F
⊢ IsZero.{v, u} c.pt

Tactic:
(isZero_zero C).of_iso (IsColimit.coconePointUniqueUpToIso hc
    (IsColimit.ofIsZero (Cocone.mk 0 0) hF (isZero_zero C)))

Premises used: CategoryTheory.Limits.isZero_zero, CategoryTheory.Limits.Cocone.mk, CategoryTheory.Limits.IsZero.of_iso, OfNat.ofNat, CategoryTheory.Limits.IsColimit.ofIsZero, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasZeroObject.{v, u} C
F : Functor.{v', v, u', u} D C
hF : F.FullyFaithful
X Y : D
f : X ⟶ Y
x : D
apply : Eq (α := F.obj X ⟶ F.obj x) (F.map (f ≫ 0)) (F.map 0)
⊢ Eq (α := X ⟶ x) (f ≫ 0) 0

Tactic:
apply hF.map_injective

Premises used: CategoryTheory.Functor.FullyFaithful.map_injective
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasZeroObject.{v, u} C
F : Functor.{v', v, u', u} D C
hF : F.FullyFaithful
X Y : D
f : X ⟶ Y
x : D
change : Eq (α := F.obj X ⟶ F.obj x) (F.map (f ≫ hF.preimage 0)) (F.map (hF.preimage 0))
⊢ Eq (α := F.obj X ⟶ F.obj x) (F.map (f ≫ 0)) (F.map 0)

Tactic:
change F.map (f ≫ (hF.preimage _)) = F.map (hF.preimage _)

Premises used: CategoryTheory.Functor.map, CategoryTheory.Functor.FullyFaithful.preimage, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasZeroObject.{v, u} C
F : Functor.{v', v, u', u} D C
hF : F.FullyFaithful
X Y : D
f : X ⟶ Y
x : D
⊢ Eq (α := F.obj X ⟶ F.obj x) (F.map (f ≫ hF.preimage 0)) (F.map (hF.preimage 0))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasZeroObject.{v, u} C
F : Functor.{v', v, u', u} D C
hF : F.FullyFaithful
x x_1 x_2 : D
f : x_1 ⟶ x_2
apply : Eq (α := F.obj x ⟶ F.obj x_2) (F.map (0 ≫ f)) (F.map 0)
⊢ Eq (α := x ⟶ x_2) (0 ≫ f) 0

Tactic:
apply hF.map_injective

Premises used: CategoryTheory.Functor.FullyFaithful.map_injective
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasZeroObject.{v, u} C
F : Functor.{v', v, u', u} D C
hF : F.FullyFaithful
x x_1 x_2 : D
f : x_1 ⟶ x_2
change : Eq (α := F.obj x ⟶ F.obj x_2) (F.map (hF.preimage 0 ≫ f)) (F.map (hF.preimage 0))
⊢ Eq (α := F.obj x ⟶ F.obj x_2) (F.map (0 ≫ f)) (F.map 0)

Tactic:
change F.map ((hF.preimage _) ≫ f) = F.map (hF.preimage _)

Premises used: CategoryTheory.Functor.map, CategoryTheory.Functor.FullyFaithful.preimage, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasZeroObject.{v, u} C
F : Functor.{v', v, u', u} D C
hF : F.FullyFaithful
x x_1 x_2 : D
f : x_1 ⟶ x_2
⊢ Eq (α := F.obj x ⟶ F.obj x_2) (F.map (hF.preimage 0 ≫ f)) (F.map (hF.preimage 0))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroMorphisms.{v, u} C
F : Functor.{v', v, u', u} D C
hF : F.FullyFaithful
X Y : D
⊢ Eq (α := X ⟶ Y) 0 (hF.preimage 0)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X : C
hX : IsTerminal.{v, u} X
rw : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0
⊢ IsZero.{v, u} X

Tactic:
rw [IsZero.iff_id_eq_zero]

Premises used: CategoryTheory.Limits.IsZero.iff_id_eq_zero
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X : C
hX : IsTerminal.{v, u} X
⊢ Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0

Tactic:
apply hX.hom_ext

Premises used: CategoryTheory.Limits.IsTerminal.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X : C
hX : IsInitial.{v, u} X
rw : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0
⊢ IsZero.{v, u} X

Tactic:
rw [IsZero.iff_id_eq_zero]

Premises used: CategoryTheory.Limits.IsZero.iff_id_eq_zero
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X : C
hX : IsInitial.{v, u} X
⊢ Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0

Tactic:
apply hX.hom_ext

Premises used: CategoryTheory.Limits.IsInitial.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
β : Type w
inst_2 : DecidableEq β
f : β → C
inst_3 : HasProduct.{w, v, u} f
b : β
⊢ Eq.{v + 1} (α := f b ⟶ f b) (CategoryStruct.comp (Y := piObj.{w, v, u} f) (ι f b) (π f b)) (𝟙 (f b))

Tactic:
simp [Pi.ι]

Premises used: CategoryTheory.Limits.Pi.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
β : Type w
inst_2 : DecidableEq β
f : β → C
inst_3 : HasProduct.{w, v, u} f
b c : β
h : b ≠ c
⊢ Eq.{v + 1} (α := f b ⟶ f c) (CategoryStruct.comp (Y := piObj.{w, v, u} f) (ι f b) (π f c)) 0

Tactic:
simp [Pi.ι, Function.update_of_ne h.symm]

Premises used: CategoryTheory.Limits.Pi.ι, Ne.symm, Function.update_of_ne
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
β : Type w
inst_2 : DecidableEq β
f : β → C
inst_3 : HasProduct.{w, v, u} f
b c : β
⊢ Eq.{v + 1} (α := f b ⟶ f c) (CategoryStruct.comp (Y := piObj.{w, v, u} f) (ι f b) (π f c))
    (if h : b = c then eqToHom ⋯ else 0)

Tactic:
grind [CategoryTheory.eqToHom_refl]

Premises used: CategoryTheory.eqToHom_refl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroMorphisms.{v, u} C
β : Type w
inst_3 : DecidableEq β
f : β → C
inst_4 : HasProduct.{w, v, u} f
b : β
Z : C
x x_1 : Z ⟶ f b
e : Eq (α := Z ⟶ piObj.{w, v, u} f) (x ≫ Pi.ι f b) (x_1 ≫ Pi.ι f b)
⊢ x = x_1

Tactic:
simpa using congrArg (· ≫ Pi.π f b) e

Premises used: congrArg, CategoryTheory.Limits.Pi.π, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
β : Type w
inst_2 : DecidableEq β
f : β → C
inst_3 : HasCoproduct.{w, v, u} f
b : β
⊢ Eq.{v + 1} (α := f b ⟶ f b) (CategoryStruct.comp (Y := sigmaObj.{w, v, u} f) (ι f b) (π f b)) (𝟙 (f b))

Tactic:
simp [Sigma.π]

Premises used: CategoryTheory.Limits.Sigma.π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
β : Type w
inst_2 : DecidableEq β
f : β → C
inst_3 : HasCoproduct.{w, v, u} f
b c : β
h : b ≠ c
⊢ Eq.{v + 1} (α := f b ⟶ f c) (CategoryStruct.comp (Y := sigmaObj.{w, v, u} f) (ι f b) (π f c)) 0

Tactic:
simp [Sigma.π, Function.update_of_ne h]

Premises used: CategoryTheory.Limits.Sigma.π, Function.update_of_ne
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
β : Type w
inst_2 : DecidableEq β
f : β → C
inst_3 : HasCoproduct.{w, v, u} f
b c : β
⊢ Eq.{v + 1} (α := f b ⟶ f c) (CategoryStruct.comp (Y := sigmaObj.{w, v, u} f) (ι f b) (π f c))
    (if h : b = c then eqToHom ⋯ else 0)

Tactic:
grind [CategoryTheory.eqToHom_refl]

Premises used: CategoryTheory.eqToHom_refl