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 : HasZeroObject.{v, u} C
X Y Z : C
f : Y ⟶ Z
change :
  Eq (α := X ⟶ Z) (CategoryStruct.comp (Y := 0) default default ≫ f) (CategoryStruct.comp (Y := 0) default default)
⊢ Eq (α := X ⟶ Z) (0 ≫ f) 0

Tactic:
change ((default : X ⟶ 0) ≫ default) ≫ f = (default : X ⟶ 0) ≫ default

Premises used: Inhabited.default, 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 : HasZeroObject.{v, u} C
X Y Z : C
f : Y ⟶ Z
rw : Eq (α := X ⟶ Z) (CategoryStruct.comp (Y := 0) default (default ≫ f)) (CategoryStruct.comp (Y := 0) default default)
⊢ Eq (α := X ⟶ Z) (CategoryStruct.comp (Y := 0) default default ≫ f) (CategoryStruct.comp (Y := 0) default default)

Tactic:
rw [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- 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 : HasZeroObject.{v, u} C
X Y Z : C
f : Y ⟶ Z
e_a : Eq (α := 0 ⟶ Z) (default ≫ f) default
⊢ Eq (α := X ⟶ Z) (CategoryStruct.comp (Y := 0) default (default ≫ f)) (CategoryStruct.comp (Y := 0) default default)

Tactic:
congr
-- 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 : HasZeroObject.{v, u} C
X Y Z : C
f : Y ⟶ Z
⊢ Eq (α := 0 ⟶ Z) (default ≫ f) default

Tactic:
simp only [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
X : C
t : IsInitial.{v, u} X
⊢ Eq (α := 0 ⟶ X) (Iso.hom (zeroIsoIsInitial t)) 0

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
X : C
t : IsInitial.{v, u} X
⊢ Eq (α := X ⟶ 0) (Iso.inv (zeroIsoIsInitial t)) 0

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
X : C
t : IsTerminal.{v, u} X
⊢ Eq (α := 0 ⟶ X) (Iso.hom (zeroIsoIsTerminal t)) 0

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
X : C
t : IsTerminal.{v, u} X
⊢ Eq (α := X ⟶ 0) (Iso.inv (zeroIsoIsTerminal t)) 0

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasInitial.{v, u} C
⊢ Eq.{v + 1} (α := 0 ⟶ initial.{v, u} C) (Iso.hom zeroIsoInitial) 0

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasInitial.{v, u} C
⊢ Eq.{v + 1} (α := initial.{v, u} C ⟶ 0) (Iso.inv zeroIsoInitial) 0

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasTerminal.{v, u} C
⊢ Eq.{v + 1} (α := 0 ⟶ terminal.{v, u} C) (Iso.hom zeroIsoTerminal) 0

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasTerminal.{v, u} C
⊢ Eq.{v + 1} (α := terminal.{v, u} C ⟶ 0) (Iso.inv zeroIsoTerminal) 0

Tactic:
ext
-- 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 : HasZeroObject.{v, u} C
B : Type u_1
inst_3 : Category.{v_1, u_1} B
⊢ HasZeroObject (Functor.{v_1, v, u_1, u} B C)

Tactic:
(((CategoryTheory.Functor.const B).obj (0 : C)).isZero fun _ => isZero_zero _).hasZeroObject

Premises used: CategoryTheory.Functor.isZero, CategoryTheory.Limits.isZero_zero, CategoryTheory.Limits.IsZero.hasZeroObject, CategoryTheory.Functor.const, OfNat.ofNat, CategoryTheory.Functor.obj
-- 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 : HasZeroObject.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
F : Functor.{v, v', u, u'} C D
hF : IsZero F
X Y : C
f : X ⟶ Y
⊢ F.map f = 0

Tactic:
(hF.obj _).eq_of_src _ _

Premises used: CategoryTheory.Limits.IsZero.obj, CategoryTheory.Limits.IsZero.eq_of_src
-- 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 : HasZeroObject.{v', u'} D
X : C
⊢ IsZero.{v', u'} (C := D) (Functor.obj.{v, v', u, u'} 0 X)

Tactic:
(isZero_zero _).obj _

Premises used: CategoryTheory.Limits.isZero_zero, CategoryTheory.Limits.IsZero.obj
-- 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 : HasZeroObject.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
X Y : C
f : X ⟶ Y
⊢ Eq.{v' + 1} (α := Quiver.Hom.{v', u'} (V := D) (Functor.obj.{v, v', u, u'} 0 X) (Functor.obj.{v, v', u, u'} 0 Y))
    (Functor.map 0 f) 0

Tactic:
(isZero_zero _).map _

Premises used: CategoryTheory.Limits.isZero_zero, CategoryTheory.Limits.IsZero.map
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
⊢ Eq.{v + 1} (α := Quiver.Hom.{v, u} (V := C) 0 0) (𝟙 0) 0

Tactic:
apply HasZeroObject.from_zero_ext

Premises used: CategoryTheory.Limits.HasZeroObject.from_zero_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
X : C
f : X ⟶ 0
⊢ f = 0

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
i : Y ≅ 0
⊢ f = f ≫ i.hom ≫ 𝟙 0 ≫ i.inv

Tactic:
simp only [Iso.hom_inv_id, id_comp, comp_id]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
i : Y ≅ 0
⊢ f = f ≫ i.hom ≫ 𝟙 0 ≫ i.inv

Tactic:
have h : f = f ≫ i.hom ≫ 𝟙 0 ≫ i.inv := by simp only [Iso.hom_inv_id, id_comp, comp_id]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
i : Y ≅ 0
h : f = f ≫ i.hom ≫ 𝟙 0 ≫ i.inv
⊢ f = 0

Tactic:
simpa using h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
X : C
f : 0 ⟶ X
⊢ f = 0

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
i : X ≅ 0
⊢ f = i.hom ≫ 𝟙 0 ≫ i.inv ≫ f

Tactic:
simp only [Iso.hom_inv_id_assoc, id_comp]

Premises used: CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
i : X ≅ 0
⊢ f = i.hom ≫ 𝟙 0 ≫ i.inv ≫ f

Tactic:
have h : f = i.hom ≫ 𝟙 0 ≫ i.inv ≫ f := by simp only [Iso.hom_inv_id_assoc, id_comp]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
i : X ≅ 0
h : f = i.hom ≫ 𝟙 0 ≫ i.inv ≫ f
⊢ f = 0

Tactic:
simpa using h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
i : IsIsomorphic.{v, u} X 0
⊢ f = 0

Tactic:
zero_of_source_iso_zero f (Nonempty.some i)

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

Tactic:
zero_of_target_iso_zero f (Nonempty.some i)

Premises used: Nonempty.some, CategoryTheory.Limits.zero_of_target_iso_zero
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
i : X ≅ 0
Z : C
g h : Z ⟶ X
h_1 : g ≫ f = h ≫ f
rw : 0 = h
rw₁ rw₂ : Eq.{v + 1} (α := Z ⟶ X) 0 0
⊢ g = h

Tactic:
rw [zero_of_target_iso_zero g i, zero_of_target_iso_zero h i]

Premises used: CategoryTheory.Limits.zero_of_target_iso_zero
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
i : Y ≅ 0
Z : C
g h : Y ⟶ Z
h_1 : f ≫ g = f ≫ h
rw : 0 = h
rw₁ rw₂ : Eq.{v + 1} (α := Y ⟶ Z) 0 0
⊢ g = h

Tactic:
rw [zero_of_source_iso_zero g i, zero_of_source_iso_zero h 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 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
X : C
h : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0
⊢ Eq.{v + 1} (α := X ⟶ 0) (Iso.hom ((idZeroEquivIsoZero X : (a : 𝟙 X = 0) → X ≅ 0) h)) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
X : C
h : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0
⊢ Eq.{v + 1} (α := 0 ⟶ X) (Iso.inv ((idZeroEquivIsoZero X : (a : 𝟙 X = 0) → X ≅ 0) h)) 0

Tactic:
rfl

Premises used: rfl
-- 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 : HasZeroObject.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
X Y : C
h : Mono.{v, u} (C := C) (X := X) (Y := Y) 0
⊢ Eq.{v + 1} (α := X ⟶ Y) (CategoryStruct.comp (Y := X) (CategoryStruct.comp (Y := 0) 0 0) 0) (𝟙 X ≫ 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 : HasZeroObject.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
X Y : C
h : Epi.{v, u} (C := C) (X := X) (Y := Y) 0
⊢ Eq.{v + 1} (α := X ⟶ Y) (CategoryStruct.comp (Y := Y) 0 (CategoryStruct.comp (Y := 0) 0 0)) (0 ≫ 𝟙 Y)

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 : HasZeroObject.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_4 : Mono f
h : f = 0
⊢ Mono.{v, u} (C := C) (X := X) (Y := Y) 0

Tactic:
subst 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 : HasZeroObject.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
X Y : C
inst_4 : Mono.{v, u} (C := C) (X := X) (Y := Y) 0
⊢ X ≅ 0

Tactic:
apply isoZeroOfMonoZero (Y := Y) ‹_›

Premises used: CategoryTheory.Limits.isoZeroOfMonoZero
-- 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 : HasZeroObject.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_4 : Epi f
h : f = 0
⊢ Epi.{v, u} (C := C) (X := X) (Y := Y) 0

Tactic:
subst 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 : HasZeroObject.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
X Y : C
inst_4 : Epi.{v, u} (C := C) (X := X) (Y := Y) 0
⊢ Y ≅ 0

Tactic:
apply isoZeroOfEpiZero (X := X) ‹_›

Premises used: CategoryTheory.Limits.isoZeroOfEpiZero
-- 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 : HasZeroObject.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
X : C
P : IsIsomorphic.{v, u} X 0
have : ∀ (P : X ≅ 0), Eq.{v + 1} (α := X ⟶ X) (CategoryStruct.comp (Y := 0) 0 0) (𝟙 X)
⊢ Eq.{v + 1} (α := X ⟶ X) (CategoryStruct.comp (Y := 0) 0 0) (𝟙 X)

Tactic:
have P := P.some
-- 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 : HasZeroObject.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
X : C
P_1 : IsIsomorphic.{v, u} X 0
P : X ≅ 0
rw : CategoryStruct.comp (Y := 0) 0 0 = P.hom ≫ 𝟙 0 ≫ P.inv
⊢ Eq.{v + 1} (α := X ⟶ X) (CategoryStruct.comp (Y := 0) 0 0) (𝟙 X)

Tactic:
rw [← P.hom_inv_id, ← Category.id_comp P.inv]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Iso.inv, CategoryTheory.Category.id_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 : HasZeroObject.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
X : C
P_1 : IsIsomorphic.{v, u} X 0
P : X ≅ 0
h : P.hom ≫ 𝟙 0 ≫ P.inv = CategoryStruct.comp (Y := 0) 0 0
⊢ CategoryStruct.comp (Y := 0) 0 0 = P.hom ≫ 𝟙 0 ≫ P.inv

Tactic:
apply Eq.symm

Premises used: Eq.symm
-- 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 : HasZeroObject.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
X : C
P_1 : IsIsomorphic.{v, u} X 0
P : X ≅ 0
h : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0
⊢ P.hom ≫ 𝟙 0 ≫ P.inv = CategoryStruct.comp (Y := 0) 0 0

Tactic:
simp only [id_comp, Iso.hom_inv_id, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.id_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 : HasZeroObject.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
X : C
P_1 : IsIsomorphic.{v, u} X 0
P : X ≅ 0
⊢ Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0

Tactic:
apply (idZeroEquivIsoZero X).invFun P

Premises used: Equiv.invFun, CategoryTheory.Limits.idZeroEquivIsoZero
-- 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 : HasZeroObject.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
X : C
P : IsIsomorphic.{v, u} X 0
⊢ Eq.{v + 1} (α := Quiver.Hom.{v, u} (V := C) 0 0) (CategoryStruct.comp (Y := X) 0 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
inst_2 : HasZeroMorphisms.{v, u} C
X Y : C
i : IsIso.{v, u} (C := C) (X := X) (Y := Y) 0
rw : Eq.{v + 1} (α := X ⟶ X) (CategoryStruct.comp (Y := Y) 0 (inv 0)) 0 ∧ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0
⊢ Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 ∧ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0

Tactic:
rw [← IsIso.hom_inv_id (0 : X ⟶ Y)]

Premises used: CategoryTheory.IsIso.hom_inv_id, 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
i : IsIso.{v, u} (C := C) (X := X) (Y := Y) 0
rw :
  Eq.{v + 1} (α := X ⟶ X) (CategoryStruct.comp (Y := Y) 0 (inv 0)) 0 ∧
    Eq.{v + 1} (α := Y ⟶ Y) (CategoryStruct.comp (Y := X) (inv 0) 0) 0
⊢ Eq.{v + 1} (α := X ⟶ X) (CategoryStruct.comp (Y := Y) 0 (inv 0)) 0 ∧ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0

Tactic:
rw [← IsIso.inv_hom_id (0 : X ⟶ Y)]

Premises used: CategoryTheory.IsIso.inv_hom_id, 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
i : IsIso.{v, u} (C := C) (X := X) (Y := Y) 0
⊢ Eq.{v + 1} (α := X ⟶ X) (CategoryStruct.comp (Y := Y) 0 (inv 0)) 0 ∧
    Eq.{v + 1} (α := Y ⟶ Y) (CategoryStruct.comp (Y := X) (inv 0) 0) 0

Tactic:
simp only [comp_zero, and_self, zero_comp]

Premises used: and_self, CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.zero_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 : C
⊢ IsIso.{v, u} (C := C) (X := X) (Y := X) 0 ≃ Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0

Tactic:
simpa using isIsoZeroEquiv X X

Premises used: CategoryTheory.Limits.isIsoZeroEquiv
-- 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
refine : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 ∧ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0 ≃ (X ≅ 0) × (Y ≅ 0)
⊢ IsIso.{v, u} (C := C) (X := X) (Y := Y) 0 ≃ (X ≅ 0) × (Y ≅ 0)

Tactic:
refine (isIsoZeroEquiv X Y).trans ?_

Premises used: Equiv.trans, CategoryTheory.Limits.isIsoZeroEquiv
-- 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
symm : (X ≅ 0) × (Y ≅ 0) ≃ Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 ∧ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0
⊢ Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 ∧ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0 ≃ (X ≅ 0) × (Y ≅ 0)

Tactic:
symm
-- 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
toFun : ∀ (a : (X ≅ 0) × (Y ≅ 0)), Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 ∧ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0
invFun : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 ∧ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0 → (X ≅ 0) × (Y ≅ 0)
left_inv :
  autoParam
    (Function.LeftInverse
      (fun (a : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 ∧ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0) ↦
        And.casesOn (motive := fun (x : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 ∧ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0) ↦
          (X ≅ 0) × (Y ≅ 0)) a fun (hX : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0) (hY : Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0) ↦
          ((idZeroEquivIsoZero X : (a : 𝟙 X = 0) → X ≅ 0) hX, (idZeroEquivIsoZero Y : (a : 𝟙 Y = 0) → Y ≅ 0) hY))
      ⋯)
    Equiv.left_inv._autoParam
right_inv :
  autoParam
    (Function.RightInverse
      (fun (a : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 ∧ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0) ↦
        And.casesOn (motive := fun (x : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 ∧ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0) ↦
          (X ≅ 0) × (Y ≅ 0)) a fun (hX : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0) (hY : Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0) ↦
          ((idZeroEquivIsoZero X : (a : 𝟙 X = 0) → X ≅ 0) hX, (idZeroEquivIsoZero Y : (a : 𝟙 Y = 0) → Y ≅ 0) hY))
      ⋯)
    Equiv.right_inv._autoParam
⊢ (X ≅ 0) × (Y ≅ 0) ≃ Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 ∧ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0

Tactic:
fconstructor
-- 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
eX : X ≅ 0
eY : Y ≅ 0
toFun : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0
toFun₁ : Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0
⊢ Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 ∧ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0

Tactic:
fconstructor
-- 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
eX : X ≅ 0
eY : Y ≅ 0
⊢ Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0

Tactic:
(idZeroEquivIsoZero X).symm eX

Premises used: Equiv.symm, DFunLike.coe, CategoryTheory.Limits.idZeroEquivIsoZero
-- 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
eX : X ≅ 0
eY : Y ≅ 0
⊢ Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0

Tactic:
exact (idZeroEquivIsoZero X).symm eX

Premises used: Equiv.symm, DFunLike.coe, CategoryTheory.Limits.idZeroEquivIsoZero
-- 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
eX : X ≅ 0
eY : Y ≅ 0
⊢ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0

Tactic:
(idZeroEquivIsoZero Y).symm eY

Premises used: Equiv.symm, DFunLike.coe, CategoryTheory.Limits.idZeroEquivIsoZero
-- 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
eX : X ≅ 0
eY : Y ≅ 0
⊢ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0

Tactic:
exact (idZeroEquivIsoZero Y).symm eY

Premises used: Equiv.symm, DFunLike.coe, CategoryTheory.Limits.idZeroEquivIsoZero
-- 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
hX : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0
hY : Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0
invFun : X ≅ 0
invFun₁ : Y ≅ 0
⊢ (X ≅ 0) × (Y ≅ 0)

Tactic:
fconstructor
-- 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
hX : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0
hY : Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0
⊢ X ≅ 0

Tactic:
exact (idZeroEquivIsoZero X) hX

Premises used: DFunLike.coe, CategoryTheory.Limits.idZeroEquivIsoZero
-- 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
hX : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0
hY : Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0
⊢ Y ≅ 0

Tactic:
exact (idZeroEquivIsoZero Y) hY

Premises used: DFunLike.coe, CategoryTheory.Limits.idZeroEquivIsoZero
-- 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
mp : IsIso.{v, u} (C := C) (X := X) (Y := Y) 0 → IsZero.{v, u} X ∧ IsZero.{v, u} Y
mpr : IsZero.{v, u} X ∧ IsZero.{v, u} Y → IsIso.{v, u} (C := C) (X := X) (Y := Y) 0
⊢ IsIso.{v, u} (C := C) (X := X) (Y := Y) 0 ↔ IsZero.{v, u} X ∧ IsZero.{v, u} Y

Tactic:
constructor
-- 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:
⟨(isZero_zero _).of_iso h'.1, (isZero_zero _).of_iso h'.2⟩

Premises used: CategoryTheory.Limits.isZero_zero, Prod.fst, CategoryTheory.Limits.IsZero.of_iso, And.intro, Prod.snd