[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
⊢ (X Y : Discrete PEmpty) → Zero (X ⟶ Y)
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X Y : Discrete PUnit
⊢ Zero (X ⟶ Y)
[PROOFSTEP]
repeat (constructor)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X Y : Discrete PUnit
⊢ Zero (X ⟶ Y)
[PROOFSTEP]
constructor
[GOAL]
case zero
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X Y : Discrete PUnit
⊢ X ⟶ Y
[PROOFSTEP]
constructor
[GOAL]
case zero.down
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X Y : Discrete PUnit
⊢ PLift (X.as = Y.as)
[PROOFSTEP]
constructor
[GOAL]
case zero.down.down
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X Y : Discrete PUnit
⊢ X.as = Y.as
[PROOFSTEP]
constructor
[GOAL]

[PROOFSTEP]
constructor
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
I J : HasZeroMorphisms C
w : ∀ (X Y : C), Zero.zero = Zero.zero
⊢ I = J
[PROOFSTEP]
have : I.Zero = J.Zero := by
  funext X Y
  specialize w X Y
  apply congrArg Zero.mk w
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
I J : HasZeroMorphisms C
w : ∀ (X Y : C), Zero.zero = Zero.zero
⊢ Zero = Zero
[PROOFSTEP]
funext X Y
[GOAL]
case h.h
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
I J : HasZeroMorphisms C
w : ∀ (X Y : C), Zero.zero = Zero.zero
X Y : C
⊢ Zero X Y = Zero X Y
[PROOFSTEP]
specialize w X Y
[GOAL]
case h.h
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
I J : HasZeroMorphisms C
X Y : C
w : Zero.zero = Zero.zero
⊢ Zero X Y = Zero X Y
[PROOFSTEP]
apply congrArg Zero.mk w
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
I J : HasZeroMorphisms C
w : ∀ (X Y : C), Zero.zero = Zero.zero
this : Zero = Zero
⊢ I = J
[PROOFSTEP]
cases I
[GOAL]
case mk
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
J : HasZeroMorphisms C
Zero✝ : (X Y : C) → _root_.Zero (X ⟶ Y)
comp_zero✝ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
w : ∀ (X Y : C), Zero.zero = Zero.zero
this : Zero = Zero
⊢ mk = J
[PROOFSTEP]
cases J
[GOAL]
case mk.mk
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
Zero✝¹ : (X Y : C) → _root_.Zero (X ⟶ Y)
comp_zero✝¹ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝¹ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
Zero✝ : (X Y : C) → _root_.Zero (X ⟶ Y)
comp_zero✝ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
w : ∀ (X Y : C), Zero.zero = Zero.zero
this : Zero = Zero
⊢ mk = mk
[PROOFSTEP]
congr
[GOAL]
case mk.mk.h.e_4
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
Zero✝¹ : (X Y : C) → _root_.Zero (X ⟶ Y)
comp_zero✝¹ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝¹ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
Zero✝ : (X Y : C) → _root_.Zero (X ⟶ Y)
comp_zero✝ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
w : ∀ (X Y : C), Zero.zero = Zero.zero
this : Zero = Zero
⊢ HEq comp_zero✝¹ comp_zero✝
[PROOFSTEP]
apply proof_irrel_heq
[GOAL]
case mk.mk.h.e_5
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
Zero✝¹ : (X Y : C) → _root_.Zero (X ⟶ Y)
comp_zero✝¹ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝¹ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
Zero✝ : (X Y : C) → _root_.Zero (X ⟶ Y)
comp_zero✝ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
w : ∀ (X Y : C), Zero.zero = Zero.zero
this : Zero = Zero
⊢ HEq zero_comp✝¹ zero_comp✝
[PROOFSTEP]
apply proof_irrel_heq
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
I J : HasZeroMorphisms C
⊢ I = J
[PROOFSTEP]
apply ext_aux
[GOAL]
case w
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
I J : HasZeroMorphisms C
⊢ ∀ (X Y : C), Zero.zero = Zero.zero
[PROOFSTEP]
intro X Y
[GOAL]
case w
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
I J : HasZeroMorphisms C
X Y : C
⊢ Zero.zero = Zero.zero
[PROOFSTEP]
have : (I.Zero X Y).zero ≫ (J.Zero Y Y).zero = (I.Zero X Y).zero := by apply I.zero_comp X (J.Zero Y Y).zero
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
I J : HasZeroMorphisms C
X Y : C
⊢ Zero.zero ≫ Zero.zero = Zero.zero
[PROOFSTEP]
apply I.zero_comp X (J.Zero Y Y).zero
[GOAL]
case w
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
I J : HasZeroMorphisms C
X Y : C
this : Zero.zero ≫ Zero.zero = Zero.zero
⊢ Zero.zero = Zero.zero
[PROOFSTEP]
have that : (I.Zero X Y).zero ≫ (J.Zero Y Y).zero = (J.Zero X Y).zero := by apply J.comp_zero (I.Zero X Y).zero Y
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
I J : HasZeroMorphisms C
X Y : C
this : Zero.zero ≫ Zero.zero = Zero.zero
⊢ Zero.zero ≫ Zero.zero = Zero.zero
[PROOFSTEP]
apply J.comp_zero (I.Zero X Y).zero Y
[GOAL]
case w
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
I J : HasZeroMorphisms C
X Y : C
this : Zero.zero ≫ Zero.zero = Zero.zero
that : Zero.zero ≫ Zero.zero = Zero.zero
⊢ Zero.zero = Zero.zero
[PROOFSTEP]
rw [← this, ← that]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Mono g
h : f ≫ g = 0
⊢ f = 0
[PROOFSTEP]
rw [← zero_comp, cancel_mono] at h
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Mono g
h✝ : f ≫ g = 0
h : f = 0
⊢ f = 0
[PROOFSTEP]
exact h
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Epi f
h : f ≫ g = 0
⊢ g = 0
[PROOFSTEP]
rw [← comp_zero, cancel_epi] at h
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Epi f
h✝ : f ≫ g = 0
h : g = 0
⊢ g = 0
[PROOFSTEP]
exact h
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
w : image.ι f = 0
⊢ f = 0
[PROOFSTEP]
rw [← image.fac f, w, HasZeroMorphisms.comp_zero]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
X✝ Y✝ : C ⥤ D
η : X✝ ⟶ Y✝
H : C ⥤ D
⊢ η ≫ 0 = 0
[PROOFSTEP]
ext X
[GOAL]
case w.h
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
X✝ Y✝ : C ⥤ D
η : X✝ ⟶ Y✝
H : C ⥤ D
X : C
⊢ NatTrans.app (η ≫ 0) X = NatTrans.app 0 X
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
X✝ Y✝ : C ⥤ D
η : X✝ ⟶ Y✝
H : C ⥤ D
X : C
⊢ NatTrans.app η X ≫ NatTrans.app 0 X = NatTrans.app 0 X
[PROOFSTEP]
apply comp_zero
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
F G H : C ⥤ D
η : G ⟶ H
⊢ 0 ≫ η = 0
[PROOFSTEP]
ext X
[GOAL]
case w.h
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
F G H : C ⥤ D
η : G ⟶ H
X : C
⊢ NatTrans.app (0 ≫ η) X = NatTrans.app 0 X
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
F G H : C ⥤ D
η : G ⟶ H
X : C
⊢ NatTrans.app 0 X ≫ NatTrans.app η X = NatTrans.app 0 X
[PROOFSTEP]
apply zero_comp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms C
X : C
h : 𝟙 X = 0
Y : C
f : X ⟶ Y
⊢ f = default
[PROOFSTEP]
rw [← id_comp f, ← id_comp (0 : X ⟶ Y), h, zero_comp, zero_comp]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms C
X : C
h : 𝟙 X = 0
Y : C
f : X ⟶ Y
⊢ 0 = default
[PROOFSTEP]
simp only
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms C
X : C
h : 𝟙 X = 0
Y : C
f : Y ⟶ X
⊢ f = default
[PROOFSTEP]
rw [← comp_id f, ← comp_id (0 : Y ⟶ X), h, comp_zero, comp_zero]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms C
X : C
h : 𝟙 X = 0
Y : C
f : Y ⟶ X
⊢ 0 = default
[PROOFSTEP]
simp only
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Mono 0
⊢ 𝟙 X ≫ 0 = 0 ≫ 0
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Epi 0
⊢ 0 ≫ 𝟙 Y = 0 ≫ 0
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : f = 0
⊢ IsZero X
[PROOFSTEP]
subst h
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Mono 0
⊢ IsZero X
[PROOFSTEP]
apply of_mono_zero X Y
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
h : f = 0
⊢ IsZero Y
[PROOFSTEP]
subst h
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Epi 0
⊢ IsZero Y
[PROOFSTEP]
apply of_epi_zero X Y
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
⊢ IsZero X ↔ f = 0
[PROOFSTEP]
rw [iff_id_eq_zero]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
⊢ 𝟙 X = 0 ↔ f = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
⊢ 𝟙 X = 0 → f = 0
[PROOFSTEP]
intro h
[GOAL]
case mp
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
h : 𝟙 X = 0
⊢ f = 0
[PROOFSTEP]
rw [← Category.id_comp f, h, zero_comp]
[GOAL]
case mpr
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
⊢ f = 0 → 𝟙 X = 0
[PROOFSTEP]
intro h
[GOAL]
case mpr
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
h : f = 0
⊢ 𝟙 X = 0
[PROOFSTEP]
rw [← IsSplitMono.id f]
[GOAL]
case mpr
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
h : f = 0
⊢ f ≫ retraction f = 0
[PROOFSTEP]
simp [h]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitEpi f
⊢ IsZero Y ↔ f = 0
[PROOFSTEP]
rw [iff_id_eq_zero]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitEpi f
⊢ 𝟙 Y = 0 ↔ f = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitEpi f
⊢ 𝟙 Y = 0 → f = 0
[PROOFSTEP]
intro h
[GOAL]
case mp
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitEpi f
h : 𝟙 Y = 0
⊢ f = 0
[PROOFSTEP]
rw [← Category.comp_id f, h, comp_zero]
[GOAL]
case mpr
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitEpi f
⊢ f = 0 → 𝟙 Y = 0
[PROOFSTEP]
intro h
[GOAL]
case mpr
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitEpi f
h : f = 0
⊢ 𝟙 Y = 0
[PROOFSTEP]
rw [← IsSplitEpi.id f]
[GOAL]
case mpr
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitEpi f
h : f = 0
⊢ section_ f ≫ f = 0
[PROOFSTEP]
simp [h]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
i : IsZero Y
⊢ IsZero X
[PROOFSTEP]
have hf := i.eq_zero_of_tgt f
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
i : IsZero Y
hf : f = 0
⊢ IsZero X
[PROOFSTEP]
subst hf
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
X Y : C
i : IsZero Y
inst✝ : Mono 0
⊢ IsZero X
[PROOFSTEP]
exact IsZero.of_mono_zero X Y
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
i : IsZero X
⊢ IsZero Y
[PROOFSTEP]
have hf := i.eq_zero_of_src f
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
i : IsZero X
hf : f = 0
⊢ IsZero Y
[PROOFSTEP]
subst hf
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
X Y : C
i : IsZero X
inst✝ : Epi 0
⊢ IsZero Y
[PROOFSTEP]
exact IsZero.of_epi_zero X Y
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
O : C
hO : IsZero O
X Y : C
f : X ⟶ Y
Z : C
⊢ f ≫ 0 = 0
[PROOFSTEP]
change f ≫ (hO.from_ Y ≫ hO.to_ Z) = hO.from_ X ≫ hO.to_ Z
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
O : C
hO : IsZero O
X Y : C
f : X ⟶ Y
Z : C
⊢ f ≫ IsZero.from_ hO Y ≫ IsZero.to_ hO Z = IsZero.from_ hO X ≫ IsZero.to_ hO Z
[PROOFSTEP]
rw [← Category.assoc]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
O : C
hO : IsZero O
X Y : C
f : X ⟶ Y
Z : C
⊢ (f ≫ IsZero.from_ hO Y) ≫ IsZero.to_ hO Z = IsZero.from_ hO X ≫ IsZero.to_ hO Z
[PROOFSTEP]
congr
[GOAL]
case e_a
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
O : C
hO : IsZero O
X Y : C
f : X ⟶ Y
Z : C
⊢ f ≫ IsZero.from_ hO Y = IsZero.from_ hO X
[PROOFSTEP]
apply hO.eq_of_tgt
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
O : C
hO : IsZero O
X Y Z : C
f : Y ⟶ Z
⊢ 0 ≫ f = 0
[PROOFSTEP]
change (hO.from_ X ≫ hO.to_ Y) ≫ f = hO.from_ X ≫ hO.to_ Z
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
O : C
hO : IsZero O
X Y Z : C
f : Y ⟶ Z
⊢ (IsZero.from_ hO X ≫ IsZero.to_ hO Y) ≫ f = IsZero.from_ hO X ≫ IsZero.to_ hO Z
[PROOFSTEP]
rw [Category.assoc]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
O : C
hO : IsZero O
X Y Z : C
f : Y ⟶ Z
⊢ IsZero.from_ hO X ≫ IsZero.to_ hO Y ≫ f = IsZero.from_ hO X ≫ IsZero.to_ hO Z
[PROOFSTEP]
congr
[GOAL]
case e_a
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
O : C
hO : IsZero O
X Y Z : C
f : Y ⟶ Z
⊢ IsZero.to_ hO Y ≫ f = IsZero.to_ hO Z
[PROOFSTEP]
apply hO.eq_of_src
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
Z : C
⊢ f ≫ 0 = 0
[PROOFSTEP]
change f ≫ (default : Y ⟶ 0) ≫ default = (default : X ⟶ 0) ≫ default
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
Z : C
⊢ f ≫ default ≫ default = default ≫ default
[PROOFSTEP]
rw [← Category.assoc]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
Z : C
⊢ (f ≫ default) ≫ default = default ≫ default
[PROOFSTEP]
congr
[GOAL]
case e_a
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
Z : C
⊢ f ≫ default = default
[PROOFSTEP]
simp only [eq_iff_true_of_subsingleton]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject C
X Y Z : C
f : Y ⟶ Z
⊢ 0 ≫ f = 0
[PROOFSTEP]
change ((default : X ⟶ 0) ≫ default) ≫ f = (default : X ⟶ 0) ≫ default
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject C
X Y Z : C
f : Y ⟶ Z
⊢ (default ≫ default) ≫ f = default ≫ default
[PROOFSTEP]
rw [Category.assoc]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject C
X Y Z : C
f : Y ⟶ Z
⊢ default ≫ default ≫ f = default ≫ default
[PROOFSTEP]
congr
[GOAL]
case e_a
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject C
X Y Z : C
f : Y ⟶ Z
⊢ default ≫ f = default
[PROOFSTEP]
simp only [eq_iff_true_of_subsingleton]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
t : IsInitial X
⊢ (zeroIsoIsInitial t).hom = 0
[PROOFSTEP]
ext
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
t : IsInitial X
⊢ (zeroIsoIsInitial t).inv = 0
[PROOFSTEP]
ext
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
t : IsTerminal X
⊢ (zeroIsoIsTerminal t).hom = 0
[PROOFSTEP]
ext
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
t : IsTerminal X
⊢ (zeroIsoIsTerminal t).inv = 0
[PROOFSTEP]
ext
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasInitial C
⊢ zeroIsoInitial.hom = 0
[PROOFSTEP]
ext
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasInitial C
⊢ zeroIsoInitial.inv = 0
[PROOFSTEP]
ext
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasTerminal C
⊢ zeroIsoTerminal.hom = 0
[PROOFSTEP]
ext
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasTerminal C
⊢ zeroIsoTerminal.inv = 0
[PROOFSTEP]
ext
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
⊢ 𝟙 0 = 0
[PROOFSTEP]
apply HasZeroObject.from_zero_ext
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
f : X ⟶ 0
⊢ f = 0
[PROOFSTEP]
ext
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
i : Y ≅ 0
⊢ f = 0
[PROOFSTEP]
have h : f = f ≫ i.hom ≫ 𝟙 0 ≫ i.inv := by simp only [Iso.hom_inv_id, id_comp, comp_id]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
i : Y ≅ 0
⊢ f = f ≫ i.hom ≫ 𝟙 0 ≫ i.inv
[PROOFSTEP]
simp only [Iso.hom_inv_id, id_comp, comp_id]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
i : Y ≅ 0
h : f = f ≫ i.hom ≫ 𝟙 0 ≫ i.inv
⊢ f = 0
[PROOFSTEP]
simpa using h
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
f : 0 ⟶ X
⊢ f = 0
[PROOFSTEP]
ext
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
i : X ≅ 0
⊢ f = 0
[PROOFSTEP]
have h : f = i.hom ≫ 𝟙 0 ≫ i.inv ≫ f := by simp only [Iso.hom_inv_id_assoc, id_comp, comp_id]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
i : X ≅ 0
⊢ f = i.hom ≫ 𝟙 0 ≫ i.inv ≫ f
[PROOFSTEP]
simp only [Iso.hom_inv_id_assoc, id_comp, comp_id]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
i : X ≅ 0
h : f = i.hom ≫ 𝟙 0 ≫ i.inv ≫ f
⊢ f = 0
[PROOFSTEP]
simpa using h
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
i : X ≅ 0
Z : C
g h : Z ⟶ X
x✝ : g ≫ f = h ≫ f
⊢ g = h
[PROOFSTEP]
rw [zero_of_target_iso_zero g i, zero_of_target_iso_zero h i]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
i : Y ≅ 0
Z : C
g h : Y ⟶ Z
x✝ : f ≫ g = f ≫ h
⊢ g = h
[PROOFSTEP]
rw [zero_of_source_iso_zero g i, zero_of_source_iso_zero h i]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ Function.LeftInverse (_ : (X ≅ 0) → 𝟙 X = 0) fun h => Iso.mk 0 0
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ Function.RightInverse (_ : (X ≅ 0) → 𝟙 X = 0) fun h => Iso.mk 0 0
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
h : Mono 0
⊢ (0 ≫ 0) ≫ 0 = 𝟙 X ≫ 0
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
h : Epi 0
⊢ 0 ≫ 0 ≫ 0 = 0 ≫ 𝟙 Y
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : f = 0
⊢ X ≅ 0
[PROOFSTEP]
subst h
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Mono 0
⊢ X ≅ 0
[PROOFSTEP]
apply isoZeroOfMonoZero ‹_›
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
h : f = 0
⊢ Y ≅ 0
[PROOFSTEP]
subst h
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Epi 0
⊢ Y ≅ 0
[PROOFSTEP]
apply isoZeroOfEpiZero ‹_›
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
P : IsIsomorphic X 0
⊢ 0 ≫ 0 = 𝟙 X
[PROOFSTEP]
cases' P with P
[GOAL]
case intro
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
P : X ≅ 0
⊢ 0 ≫ 0 = 𝟙 X
[PROOFSTEP]
rw [← P.hom_inv_id, ← Category.id_comp P.inv]
[GOAL]
case intro
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
P : X ≅ 0
⊢ 0 ≫ 0 = P.hom ≫ 𝟙 0 ≫ P.inv
[PROOFSTEP]
apply Eq.symm
[GOAL]
case intro.h
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
P : X ≅ 0
⊢ P.hom ≫ 𝟙 0 ≫ P.inv = 0 ≫ 0
[PROOFSTEP]
simp only [id_comp, Iso.hom_inv_id, comp_zero]
[GOAL]
case intro.h
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
P : X ≅ 0
⊢ 𝟙 X = 0
[PROOFSTEP]
apply (idZeroEquivIsoZero X).invFun P
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
P : IsIsomorphic X 0
⊢ 0 ≫ 0 = 𝟙 0
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms C
X Y : C
⊢ IsIso 0 → 𝟙 X = 0 ∧ 𝟙 Y = 0
[PROOFSTEP]
intro i
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms C
X Y : C
i : IsIso 0
⊢ 𝟙 X = 0 ∧ 𝟙 Y = 0
[PROOFSTEP]
rw [← IsIso.hom_inv_id (0 : X ⟶ Y)]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms C
X Y : C
i : IsIso 0
⊢ 0 ≫ inv 0 = 0 ∧ 𝟙 Y = 0
[PROOFSTEP]
rw [← IsIso.inv_hom_id (0 : X ⟶ Y)]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms C
X Y : C
i : IsIso 0
⊢ 0 ≫ inv 0 = 0 ∧ inv 0 ≫ 0 = 0
[PROOFSTEP]
simp only [eq_self_iff_true, comp_zero, and_self, zero_comp]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms C
X Y : C
h : 𝟙 X = 0 ∧ 𝟙 Y = 0
⊢ 0 ≫ 0 = 𝟙 X ∧ 0 ≫ 0 = 𝟙 Y
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms C
X Y : C
⊢ Function.LeftInverse (_ : 𝟙 X = 0 ∧ 𝟙 Y = 0 → IsIso 0) (_ : IsIso 0 → 𝟙 X = 0 ∧ 𝟙 Y = 0)
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms C
X Y : C
⊢ Function.RightInverse (_ : 𝟙 X = 0 ∧ 𝟙 Y = 0 → IsIso 0) (_ : IsIso 0 → 𝟙 X = 0 ∧ 𝟙 Y = 0)
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms C
X : C
⊢ IsIso 0 ≃ 𝟙 X = 0
[PROOFSTEP]
simpa using isIsoZeroEquiv X X
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
⊢ IsIso 0 ≃ (X ≅ 0) × (Y ≅ 0)
[PROOFSTEP]
refine' (isIsoZeroEquiv X Y).trans _
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
⊢ 𝟙 X = 0 ∧ 𝟙 Y = 0 ≃ (X ≅ 0) × (Y ≅ 0)
[PROOFSTEP]
symm
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
⊢ (X ≅ 0) × (Y ≅ 0) ≃ 𝟙 X = 0 ∧ 𝟙 Y = 0
[PROOFSTEP]
fconstructor
[GOAL]
case toFun
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
⊢ (X ≅ 0) × (Y ≅ 0) → 𝟙 X = 0 ∧ 𝟙 Y = 0
[PROOFSTEP]
rintro ⟨eX, eY⟩
[GOAL]
case toFun.mk
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
eX : X ≅ 0
eY : Y ≅ 0
⊢ 𝟙 X = 0 ∧ 𝟙 Y = 0
[PROOFSTEP]
fconstructor
[GOAL]
case toFun.mk.left
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
eX : X ≅ 0
eY : Y ≅ 0
⊢ 𝟙 X = 0
case toFun.mk.right
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
eX : X ≅ 0
eY : Y ≅ 0
⊢ 𝟙 Y = 0
[PROOFSTEP]
exact (idZeroEquivIsoZero X).symm eX
[GOAL]
case toFun.mk.right
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
eX : X ≅ 0
eY : Y ≅ 0
⊢ 𝟙 Y = 0
[PROOFSTEP]
exact (idZeroEquivIsoZero Y).symm eY
[GOAL]
case invFun
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
⊢ 𝟙 X = 0 ∧ 𝟙 Y = 0 → (X ≅ 0) × (Y ≅ 0)
[PROOFSTEP]
rintro ⟨hX, hY⟩
[GOAL]
case invFun.intro
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
hX : 𝟙 X = 0
hY : 𝟙 Y = 0
⊢ (X ≅ 0) × (Y ≅ 0)
[PROOFSTEP]
fconstructor
[GOAL]
case invFun.intro.fst
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
hX : 𝟙 X = 0
hY : 𝟙 Y = 0
⊢ X ≅ 0
case invFun.intro.snd
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
hX : 𝟙 X = 0
hY : 𝟙 Y = 0
⊢ Y ≅ 0
[PROOFSTEP]
exact (idZeroEquivIsoZero X) hX
[GOAL]
case invFun.intro.snd
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
hX : 𝟙 X = 0
hY : 𝟙 Y = 0
⊢ Y ≅ 0
[PROOFSTEP]
exact (idZeroEquivIsoZero Y) hY
[GOAL]
case left_inv
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
⊢ Function.LeftInverse (fun a => And.casesOn a fun hX hY => (↑(idZeroEquivIsoZero X) hX, ↑(idZeroEquivIsoZero Y) hY))
    (_ : (X ≅ 0) × (Y ≅ 0) → 𝟙 X = 0 ∧ 𝟙 Y = 0)
[PROOFSTEP]
aesop_cat
[GOAL]
case right_inv
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
⊢ Function.RightInverse (fun a => And.casesOn a fun hX hY => (↑(idZeroEquivIsoZero X) hX, ↑(idZeroEquivIsoZero Y) hY))
    (_ : (X ≅ 0) × (Y ≅ 0) → 𝟙 X = 0 ∧ 𝟙 Y = 0)
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
i : X ≅ 0
j : Y ≅ 0
⊢ IsIso f
[PROOFSTEP]
rw [zero_of_source_iso_zero f i]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
i : X ≅ 0
j : Y ≅ 0
⊢ IsIso 0
[PROOFSTEP]
exact (isIsoZeroEquivIsoZero _ _).invFun ⟨i, j⟩
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasInitial C
⊢ HasZeroObject C
[PROOFSTEP]
refine' ⟨⟨⊥_ C, fun X => ⟨⟨⟨0⟩, by aesop_cat⟩⟩, fun X => ⟨⟨⟨0⟩, fun f => _⟩⟩⟩⟩
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasInitial C
X : C
⊢ ∀ (a : ⊥_ C ⟶ X), a = default
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasInitial C
X : C
f : X ⟶ ⊥_ C
⊢ f = default
[PROOFSTEP]
calc
  f = f ≫ 𝟙 _ := (Category.comp_id _).symm
  _ = f ≫ 0 := by congr!
  _ = 0 := HasZeroMorphisms.comp_zero _ _
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasInitial C
X : C
f : X ⟶ ⊥_ C
⊢ f ≫ 𝟙 (⊥_ C) = f ≫ 0
[PROOFSTEP]
congr!
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasTerminal C
⊢ HasZeroObject C
[PROOFSTEP]
refine' ⟨⟨⊤_ C, fun X => ⟨⟨⟨0⟩, fun f => _⟩⟩, fun X => ⟨⟨⟨0⟩, by aesop_cat⟩⟩⟩⟩
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasTerminal C
X : C
⊢ ∀ (a : X ⟶ ⊤_ C), a = default
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasTerminal C
X : C
f : ⊤_ C ⟶ X
⊢ f = default
[PROOFSTEP]
calc
  f = 𝟙 _ ≫ f := (Category.id_comp _).symm
  _ = 0 ≫ f := by congr!
  _ = 0 := zero_comp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasTerminal C
X : C
f : ⊤_ C ⟶ X
⊢ 𝟙 (⊤_ C) ≫ f = 0 ≫ f
[PROOFSTEP]
congr!
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : HasImage f
inst✝ : Epi (factorThruImage f)
h : f ≫ g = 0
⊢ factorThruImage f ≫ image.ι f ≫ g = 0
[PROOFSTEP]
simp [h]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : HasImage g
h : f ≫ g = 0
⊢ (f ≫ factorThruImage g) ≫ image.ι g = 0
[PROOFSTEP]
simp [h]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X Y : C
inst✝ : HasImage 0
⊢ ι 0 = 0
[PROOFSTEP]
rw [← image.lift_fac (monoFactorisationZero X Y)]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X Y : C
inst✝ : HasImage 0
⊢ lift (monoFactorisationZero X Y) ≫ (monoFactorisationZero X Y).m = 0
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
inst✝¹ : HasEqualizers C
X Y : C
f : X ⟶ Y
h : f = 0
inst✝ : HasImage f
⊢ ι f = 0
[PROOFSTEP]
rw [image.eq_fac h]
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
inst✝¹ : HasEqualizers C
X Y : C
f : X ⟶ Y
h : f = 0
inst✝ : HasImage f
⊢ (eqToIso h).hom ≫ ι 0 = 0
[PROOFSTEP]
simp