awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : HasCoproduct.{w, v, u} f
b : β
Z : C
x x_1 : f b ⟶ Z
e : Eq (α := sigmaObj.{w, v, u} f ⟶ Z) (Sigma.π f b ≫ x) (Sigma.π f b ≫ x_1)
⊢ x = x_1

Tactic:
simpa using congrArg (Sigma.ι f b ≫ ·) e

Premises used: congrArg, CategoryTheory.Limits.Sigma.ι, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
inst_2 : HasBinaryProduct.{v, u} X Y
⊢ Eq.{v + 1} (α := X ⟶ X) (CategoryStruct.comp (Y := prod.{v, u} X Y) (inl X Y) fst) (𝟙 X)

Tactic:
simp [prod.inl]

Premises used: CategoryTheory.Limits.prod.inl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
inst_2 : HasBinaryProduct.{v, u} X Y
⊢ Eq.{v + 1} (α := X ⟶ Y) (CategoryStruct.comp (Y := prod.{v, u} X Y) (inl X Y) snd) 0

Tactic:
simp [prod.inl]

Premises used: CategoryTheory.Limits.prod.inl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
inst_2 : HasBinaryProduct.{v, u} X Y
⊢ Eq.{v + 1} (α := Y ⟶ X) (CategoryStruct.comp (Y := prod.{v, u} X Y) (inr X Y) fst) 0

Tactic:
simp [prod.inr]

Premises used: CategoryTheory.Limits.prod.inr
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
inst_2 : HasBinaryProduct.{v, u} X Y
⊢ Eq.{v + 1} (α := Y ⟶ Y) (CategoryStruct.comp (Y := prod.{v, u} X Y) (inr X Y) snd) (𝟙 Y)

Tactic:
simp [prod.inr]

Premises used: CategoryTheory.Limits.prod.inr
-- 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 : HasBinaryProduct.{v, u} X Y
Z : C
x x_1 : Z ⟶ X
e : Eq (α := Z ⟶ prod.{v, u} X Y) (x ≫ prod.inl X Y) (x_1 ≫ prod.inl X Y)
⊢ x = x_1

Tactic:
simpa using congrArg (· ≫ prod.fst) e

Premises used: congrArg, CategoryTheory.Limits.prod.fst, 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
X Y : C
inst_3 : HasBinaryProduct.{v, u} X Y
Z : C
x x_1 : Z ⟶ Y
e : Eq (α := Z ⟶ prod.{v, u} X Y) (x ≫ prod.inr X Y) (x_1 ≫ prod.inr X Y)
⊢ x = x_1

Tactic:
simpa using congrArg (· ≫ prod.snd) e

Premises used: congrArg, CategoryTheory.Limits.prod.snd, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
inst_2 : HasBinaryCoproduct.{v, u} X Y
⊢ Eq.{v + 1} (α := X ⟶ X) (CategoryStruct.comp (Y := coprod.{v, u} X Y) inl (fst X Y)) (𝟙 X)

Tactic:
simp [coprod.fst]

Premises used: CategoryTheory.Limits.coprod.fst
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
inst_2 : HasBinaryCoproduct.{v, u} X Y
⊢ Eq.{v + 1} (α := Y ⟶ X) (CategoryStruct.comp (Y := coprod.{v, u} X Y) inr (fst X Y)) 0

Tactic:
simp [coprod.fst]

Premises used: CategoryTheory.Limits.coprod.fst
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
inst_2 : HasBinaryCoproduct.{v, u} X Y
⊢ Eq.{v + 1} (α := X ⟶ Y) (CategoryStruct.comp (Y := coprod.{v, u} X Y) inl (snd X Y)) 0

Tactic:
simp [coprod.snd]

Premises used: CategoryTheory.Limits.coprod.snd
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
inst_2 : HasBinaryCoproduct.{v, u} X Y
⊢ Eq.{v + 1} (α := Y ⟶ Y) (CategoryStruct.comp (Y := coprod.{v, u} X Y) inr (snd X Y)) (𝟙 Y)

Tactic:
simp [coprod.snd]

Premises used: CategoryTheory.Limits.coprod.snd
-- 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 : HasBinaryCoproduct.{v, u} X Y
Z : C
x x_1 : X ⟶ Z
e : Eq (α := coprod.{v, u} X Y ⟶ Z) (coprod.fst X Y ≫ x) (coprod.fst X Y ≫ x_1)
⊢ x = x_1

Tactic:
simpa using congrArg (coprod.inl ≫ ·) e

Premises used: congrArg, CategoryTheory.Limits.coprod.inl, 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
X Y : C
inst_3 : HasBinaryCoproduct.{v, u} X Y
Z : C
x x_1 : Y ⟶ Z
e : Eq (α := coprod.{v, u} X Y ⟶ Z) (coprod.snd X Y ≫ x) (coprod.snd X Y ≫ x_1)
⊢ x = x_1

Tactic:
simpa using congrArg (coprod.inr ≫ ·) e

Premises used: congrArg, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.coprod.inr
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
X Y : P.FullSubcategory
⊢ Eq.{v_1 + 1} (α := X ⟶ Y) (homMk (P := P) 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
X Y : P.FullSubcategory
⊢ Eq.{v_1 + 1} (α := X.obj (P := P) ⟶ Y.obj (P := P)) (InducedCategory.Hom.hom 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : IsZero.{v, u} X
f : X ⟶ Y
⊢ f = h.to_ Y

Tactic:
@Unique.eq_default _ (id _) _

Premises used: Unique.eq_default, CategoryTheory.Limits.IsZero.to_
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : IsZero.{v, u} X
f : X ⟶ Y
⊢ h.to_ Y = f

Tactic:
(h.eq_to f).symm

Premises used: CategoryTheory.Limits.IsZero.eq_to, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : IsZero.{v, u} X
f : Y ⟶ X
⊢ f = h.from_ Y

Tactic:
@Unique.eq_default _ (id _) _

Premises used: Unique.eq_default, CategoryTheory.Limits.IsZero.from_
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : IsZero.{v, u} X
f : Y ⟶ X
⊢ h.from_ Y = f

Tactic:
(h.eq_from f).symm

Premises used: Eq.symm, CategoryTheory.Limits.IsZero.eq_from
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
hX : IsZero.{v, u} X
f g : X ⟶ Y
⊢ f = g

Tactic:
(hX.eq_to f).trans (hX.eq_to g).symm

Premises used: CategoryTheory.Limits.IsZero.eq_to, Eq.symm, Eq.trans
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
hX : IsZero.{v, u} X
f g : Y ⟶ X
⊢ f = g

Tactic:
(hX.eq_from f).trans (hX.eq_from g).symm

Premises used: Eq.symm, CategoryTheory.Limits.IsZero.eq_from, Eq.trans
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
hX : IsZero.{v, u} X
hY : IsZero.{v, u} Y
f : X ⟶ Y
⊢ IsIso f

Tactic:
⟨hY.to_ _, hX.eq_of_src _ _, hY.eq_of_src _ _⟩

Premises used: CategoryTheory.Limits.IsZero.to_, CategoryTheory.Limits.IsZero.eq_of_src, And.intro, Exists.intro, CategoryTheory.IsIso.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
hY : IsZero.{v, u} Y
e : X ≅ Y
⊢ IsZero.{v, u} X

Tactic:
⟨fun Z => ⟨⟨⟨e.hom ≫ hY.to_ Z⟩, fun f => ?_⟩⟩,
    fun Z => ⟨⟨⟨hY.from_ Z ≫ e.inv⟩, fun f => ?_⟩⟩⟩

Premises used: Unique.mk, Nonempty.intro, CategoryTheory.Limits.IsZero.to_, CategoryTheory.Limits.IsZero.from_, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv, CategoryTheory.Limits.IsZero.mk, Inhabited.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
hY : IsZero.{v, u} Y
e : X ≅ Y
refine_1 : ∀ (Z : C) (f : X ⟶ Z), f = default
refine_2 : ∀ (Z : C) (f : Z ⟶ X), f = default
⊢ IsZero.{v, u} X

Tactic:
refine ⟨fun Z => ⟨⟨⟨e.hom ≫ hY.to_ Z⟩, fun f => ?_⟩⟩,
    fun Z => ⟨⟨⟨hY.from_ Z ≫ e.inv⟩, fun f => ?_⟩⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
hY : IsZero.{v, u} Y
e : X ≅ Y
Z : C
f : X ⟶ Z
refine_1 : e.inv ≫ f = e.inv ≫ default
⊢ f = default

Tactic:
rw [← cancel_epi e.inv]

Premises used: CategoryTheory.cancel_epi, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
hY : IsZero.{v, u} Y
e : X ≅ Y
Z : C
f : X ⟶ Z
⊢ e.inv ≫ f = e.inv ≫ default

Tactic:
apply hY.eq_of_src

Premises used: CategoryTheory.Limits.IsZero.eq_of_src
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
hY : IsZero.{v, u} Y
e : X ≅ Y
Z : C
f : Z ⟶ X
refine_2 : f ≫ e.hom = default ≫ e.hom
⊢ f = default

Tactic:
rw [← cancel_mono e.hom]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
hY : IsZero.{v, u} Y
e : X ≅ Y
Z : C
f : Z ⟶ X
⊢ f ≫ e.hom = default ≫ e.hom

Tactic:
apply hY.eq_of_tgt

Premises used: CategoryTheory.Limits.IsZero.eq_of_tgt
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
Goal:
C : Type u
inst : Category.{v, u} C
X : C
h : IsZero.{v, u} X
⊢ IsZero.{v, u} (Opposite.op X)

Tactic:
⟨fun Y => ⟨⟨⟨(h.from_ (Opposite.unop Y)).op⟩, fun _ => Quiver.Hom.unop_inj (h.eq_of_tgt _ _)⟩⟩,
    fun Y => ⟨⟨⟨(h.to_ (Opposite.unop Y)).op⟩, fun _ => Quiver.Hom.unop_inj (h.eq_of_src _ _)⟩⟩⟩

Premises used: Inhabited.default, Unique.mk, Quiver.Hom.op, Quiver.Hom.unop, Nonempty.intro, Quiver.Hom.unop_inj, CategoryTheory.Limits.IsZero.to_, CategoryTheory.Limits.IsZero.eq_of_src, CategoryTheory.Limits.IsZero.eq_of_tgt, CategoryTheory.Limits.IsZero.from_, Opposite.unop, CategoryTheory.Limits.IsZero.mk, Inhabited.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
Goal:
C : Type u
inst : Category.{v, u} C
X : Cᵒᵖ
h : IsZero.{v, u} X
⊢ IsZero.{v, u} (Opposite.unop X)

Tactic:
⟨fun Y => ⟨⟨⟨(h.from_ (Opposite.op Y)).unop⟩, fun _ => Quiver.Hom.op_inj (h.eq_of_tgt _ _)⟩⟩,
    fun Y => ⟨⟨⟨(h.to_ (Opposite.op Y)).unop⟩, fun _ => Quiver.Hom.op_inj (h.eq_of_src _ _)⟩⟩⟩

Premises used: Inhabited.default, Unique.mk, Quiver.Hom.op, Quiver.Hom.op_inj, Quiver.Hom.unop, Nonempty.intro, Opposite.op, CategoryTheory.Limits.IsZero.to_, CategoryTheory.Limits.IsZero.eq_of_src, CategoryTheory.Limits.IsZero.eq_of_tgt, CategoryTheory.Limits.IsZero.from_, CategoryTheory.Limits.IsZero.mk, Inhabited.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
e : X ≅ Y
⊢ IsZero.{v, u} X ↔ IsZero.{v, u} Y

Tactic:
⟨fun h => h.of_iso e.symm, fun h => h.of_iso e⟩

Premises used: CategoryTheory.Limits.IsZero.of_iso, Iff.intro, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
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
hF : ∀ (X : C), IsZero.{v', u'} (F.obj X)
unique_to : ∀ (Y : Functor.{v, v', u, u'} C D), Nonempty (Unique (F ⟶ Y))
unique_from : ∀ (Y : Functor.{v, v', u, u'} C D), Nonempty (Unique (Y ⟶ F))
⊢ IsZero F

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
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
hF : ∀ (X : C), IsZero.{v', u'} (F.obj X)
G : Functor.{v, v', u, u'} C D
⊢ Nonempty (Unique (F ⟶ G))

Tactic:
⟨⟨⟨?_⟩, ?_⟩⟩

Premises used: Unique.mk, Nonempty.intro, Inhabited.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
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
hF : ∀ (X : C), IsZero.{v', u'} (F.obj X)
G : Functor.{v, v', u, u'} C D
unique_to : F ⟶ G
unique_to₁ : ∀ (a : F ⟶ G), a = default
⊢ Nonempty (Unique (F ⟶ G))

Tactic:
refine ⟨⟨⟨?_⟩, ?_⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
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
hF : ∀ (X : C), IsZero.{v', u'} (F.obj X)
G : Functor.{v, v', u, u'} C D
⊢ Nonempty (Unique (G ⟶ F))

Tactic:
⟨⟨⟨?_⟩, ?_⟩⟩

Premises used: Unique.mk, Nonempty.intro, Inhabited.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
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
hF : ∀ (X : C), IsZero.{v', u'} (F.obj X)
G : Functor.{v, v', u, u'} C D
unique_from : G ⟶ F
unique_from₁ : ∀ (a : G ⟶ F), a = default
⊢ Nonempty (Unique (G ⟶ F))

Tactic:
refine ⟨⟨⟨?_⟩, ?_⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
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
hF : ∀ (X : C), IsZero.{v', u'} (F.obj X)
G : Functor.{v, v', u, u'} C D
unique_to : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.map f ≫ ⋯.to_ (G.obj Y) = ⋯.to_ (G.obj X) ≫ G.map f
⊢ F ⟶ G

Tactic:
refine
      { app := fun X => (hF _).to_ _
        naturality := ?_ }
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
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
hF : ∀ (X : C), IsZero.{v', u'} (F.obj X)
G : Functor.{v, v', u, u'} C D
X Y : C
f : X ⟶ Y
⊢ F.map f ≫ ⋯.to_ (G.obj Y) = ⋯.to_ (G.obj X) ≫ G.map f

Tactic:
(hF _).eq_of_src _ _

Premises used: CategoryTheory.Limits.IsZero.eq_of_src
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
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
hF : ∀ (X : C), IsZero.{v', u'} (F.obj X)
G : Functor.{v, v', u, u'} C D
X Y : C
f : X ⟶ Y
⊢ F.map f ≫ ⋯.to_ (G.obj Y) = ⋯.to_ (G.obj X) ≫ G.map f

Tactic:
exact (hF _).eq_of_src _ _

Premises used: CategoryTheory.Limits.IsZero.eq_of_src
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
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
hF : ∀ (X : C), IsZero.{v', u'} (F.obj X)
G : Functor.{v, v', u, u'} C D
f : F ⟶ G
unique_to : ∀ (x : C), f.app x = NatTrans.app default x
⊢ f = default

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
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
hF : ∀ (X : C), IsZero.{v', u'} (F.obj X)
G : Functor.{v, v', u, u'} C D
f : F ⟶ G
x : C
⊢ f.app x = NatTrans.app default x

Tactic:
apply (hF _).eq_of_src _ _

Premises used: CategoryTheory.Limits.IsZero.eq_of_src
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
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
hF : ∀ (X : C), IsZero.{v', u'} (F.obj X)
G : Functor.{v, v', u, u'} C D
unique_from : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), G.map f ≫ ⋯.from_ (G.obj Y) = ⋯.from_ (G.obj X) ≫ F.map f
⊢ G ⟶ F

Tactic:
refine
      { app := fun X => (hF _).from_ _
        naturality := ?_ }
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
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
hF : ∀ (X : C), IsZero.{v', u'} (F.obj X)
G : Functor.{v, v', u, u'} C D
X Y : C
f : X ⟶ Y
⊢ G.map f ≫ ⋯.from_ (G.obj Y) = ⋯.from_ (G.obj X) ≫ F.map f

Tactic:
(hF _).eq_of_tgt _ _

Premises used: CategoryTheory.Limits.IsZero.eq_of_tgt
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
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
hF : ∀ (X : C), IsZero.{v', u'} (F.obj X)
G : Functor.{v, v', u, u'} C D
X Y : C
f : X ⟶ Y
⊢ G.map f ≫ ⋯.from_ (G.obj Y) = ⋯.from_ (G.obj X) ≫ F.map f

Tactic:
exact (hF _).eq_of_tgt _ _

Premises used: CategoryTheory.Limits.IsZero.eq_of_tgt
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
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
hF : ∀ (X : C), IsZero.{v', u'} (F.obj X)
G : Functor.{v, v', u, u'} C D
f : G ⟶ F
unique_from : ∀ (x : C), f.app x = NatTrans.app default x
⊢ f = default

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
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
hF : ∀ (X : C), IsZero.{v', u'} (F.obj X)
G : Functor.{v, v', u, u'} C D
f : G ⟶ F
x : C
⊢ f.app x = NatTrans.app default x

Tactic:
apply (hF _).eq_of_tgt _ _

Premises used: CategoryTheory.Limits.IsZero.eq_of_tgt
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
x : Discrete PUnit.{u_1 + 1}
⊢ ∀ (a : { as := PUnit.unit : Discrete PUnit.{u_1 + 1} } ⟶ { as := PUnit.unit }), a = 𝟙 { as := PUnit.unit }

Tactic:
subsingleton
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
⊢ IsZero.{v, u} (C := C) 0

Tactic:
HasZeroObject.zero.choose_spec

Premises used: Exists.choose_spec, CategoryTheory.Limits.HasZeroObject.zero
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroObject.{v, u} C
⊢ HasZeroObject.{v, u} Cᵒᵖ

Tactic:
⟨⟨Opposite.op 0, IsZero.op (isZero_zero C)⟩⟩

Premises used: CategoryTheory.Limits.IsZero.op, CategoryTheory.Limits.HasZeroObject.mk, CategoryTheory.Limits.isZero_zero, Opposite.op, Exists.intro, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} Cᵒᵖ
⊢ HasZeroObject.{v, u} C

Tactic:
⟨⟨Opposite.unop 0, IsZero.unop (isZero_zero Cᵒᵖ)⟩⟩

Premises used: Opposite, CategoryTheory.Limits.HasZeroObject.mk, CategoryTheory.Limits.isZero_zero, Exists.intro, OfNat.ofNat, Opposite.unop, CategoryTheory.Limits.IsZero.unop
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
Goal:
C : Type u
inst : Category.{v, u} C
X : C
hX : IsZero.{v, u} X
⊢ HasZeroObject.{v, u} C

Tactic:
⟨⟨X, hX⟩⟩

Premises used: CategoryTheory.Limits.HasZeroObject.mk, Exists.intro
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroObject.{v', u'} D
F : Functor.{v, v', u, u'} C D
hF : IsZero F
X : C
G : Functor.{v, v', u, u'} C D := Functor.obj (Functor.const C) 0
⊢ IsZero G

Tactic:
have hG : IsZero G := Functor.isZero _ fun _ => isZero_zero _
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroObject.{v', u'} D
F : Functor.{v, v', u, u'} C D
hF : IsZero F
X : C
G : Functor.{v, v', u, u'} C D := Functor.obj (Functor.const C) 0
hG : IsZero G
e : F ≅ G := hF.iso hG
⊢ IsZero.{v', u'} (F.obj X)

Tactic:
(isZero_zero _).of_iso (e.app X)

Premises used: CategoryTheory.Limits.isZero_zero, CategoryTheory.Limits.IsZero.of_iso, CategoryTheory.Iso.app
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroObject.{v', u'} D
F : Functor.{v, v', u, u'} C D
hF : IsZero F
X : C
G : Functor.{v, v', u, u'} C D := Functor.obj (Functor.const C) 0
hG : IsZero G
e : F ≅ G := hF.iso hG
⊢ IsZero.{v', u'} (F.obj X)

Tactic:
exact (isZero_zero _).of_iso (e.app X)

Premises used: CategoryTheory.Limits.isZero_zero, CategoryTheory.Limits.IsZero.of_iso, CategoryTheory.Iso.app
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
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 : F.Full
inst_3 : F.Faithful
X : C
hX : IsZero.{v', u'} (F.obj X)
have : ∀ (h : F.FullyFaithful), IsZero.{v, u} X
⊢ IsZero.{v, u} X

Tactic:
have h : F.FullyFaithful := .ofFullyFaithful _
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
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 : F.Full
inst_3 : F.Faithful
X : C
hX : IsZero.{v', u'} (F.obj X)
h : F.FullyFaithful
have : ∀ (this : (Y : C) → Unique (F.obj X ⟶ F.obj Y)), IsZero.{v, u} X
⊢ IsZero.{v, u} X

Tactic:
have (Y : C) := (hX.unique_to (F.obj Y)).some
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
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 : F.Full
inst_3 : F.Faithful
X : C
hX : IsZero.{v', u'} (F.obj X)
h : F.FullyFaithful
this : (Y : C) → Unique (F.obj X ⟶ F.obj Y)
have : ∀ (this : (Y : C) → Unique (F.obj Y ⟶ F.obj X)), IsZero.{v, u} X
⊢ IsZero.{v, u} X

Tactic:
have (Y : C) := (hX.unique_from (F.obj Y)).some
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
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 : F.Full
inst_3 : F.Faithful
X : C
hX : IsZero.{v', u'} (F.obj X)
h : F.FullyFaithful
this_1 : (Y : C) → Unique (F.obj X ⟶ F.obj Y)
this : (Y : C) → Unique (F.obj Y ⟶ F.obj X)
⊢ IsZero.{v, u} X

Tactic:
⟨fun Y ↦ ⟨h.homEquiv.unique⟩, fun Y ↦ ⟨h.homEquiv.unique⟩⟩

Premises used: Equiv.unique, CategoryTheory.Functor.FullyFaithful.homEquiv, Nonempty.intro, CategoryTheory.Limits.IsZero.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
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 : F.Full
inst_3 : F.Faithful
X : C
hX : IsZero.{v', u'} (F.obj X)
h : F.FullyFaithful
this_1 : (Y : C) → Unique (F.obj X ⟶ F.obj Y)
this : (Y : C) → Unique (F.obj Y ⟶ F.obj X)
⊢ IsZero.{v, u} X

Tactic:
exact ⟨fun Y ↦ ⟨h.homEquiv.unique⟩, fun Y ↦ ⟨h.homEquiv.unique⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
X : C
f g : X ⟶ 0
⊢ f = g

Tactic:
(isZero_zero C).eq_of_tgt _ _

Premises used: CategoryTheory.Limits.isZero_zero, CategoryTheory.Limits.IsZero.eq_of_tgt
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
X : C
f g : 0 ⟶ X
⊢ f = g

Tactic:
(isZero_zero C).eq_of_src _ _

Premises used: CategoryTheory.Limits.isZero_zero, CategoryTheory.Limits.IsZero.eq_of_src
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroObject.{v, u} C
X : C
f g : X ≅ 0
⊢ f = g

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroObject.{v, u} C
X : C
f : 0 ⟶ X
Z : C
g h : Z ⟶ 0
h_1 : g ≫ f = h ≫ f
⊢ g = h

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroObject.{v, u} C
X : C
f : X ⟶ 0
Z : C
g h : 0 ⟶ Z
h_1 : f ≫ g = f ≫ h
⊢ g = h

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroObject.{v, u} C
f : Quiver.Hom.{v, u} (V := C) 0 0
⊢ IsIso.{v, u} (C := C) (X := 0) (𝟙 0)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroObject.{v, u} C
f : Quiver.Hom.{v, u} (V := C) 0 0
h : f = 𝟙 0
⊢ IsIso f

Tactic:
convert! show IsIso (𝟙 (0 : C)) by infer_instance