[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X Y : C
hY : IsZero Y
e : X ≅ Y
⊢ IsZero X
[PROOFSTEP]
refine' ⟨fun Z => ⟨⟨⟨e.hom ≫ hY.to_ Z⟩, fun f => _⟩⟩, fun Z => ⟨⟨⟨hY.from_ Z ≫ e.inv⟩, fun f => _⟩⟩⟩
[GOAL]
case refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X Y : C
hY : IsZero Y
e : X ≅ Y
Z : C
f : X ⟶ Z
⊢ f = default
[PROOFSTEP]
rw [← cancel_epi e.inv]
[GOAL]
case refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X Y : C
hY : IsZero Y
e : X ≅ Y
Z : C
f : X ⟶ Z
⊢ e.inv ≫ f = e.inv ≫ default
[PROOFSTEP]
apply hY.eq_of_src
[GOAL]
case refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X Y : C
hY : IsZero Y
e : X ≅ Y
Z : C
f : Z ⟶ X
⊢ f = default
[PROOFSTEP]
rw [← cancel_mono e.hom]
[GOAL]
case refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X Y : C
hY : IsZero Y
e : X ≅ Y
Z : C
f : Z ⟶ X
⊢ f ≫ e.hom = default ≫ e.hom
[PROOFSTEP]
apply hY.eq_of_tgt
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
⊢ IsZero F
[PROOFSTEP]
constructor
[GOAL]
case unique_to
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
⊢ ∀ (Y : C ⥤ D), Nonempty (Unique (F ⟶ Y))
[PROOFSTEP]
intro G
[GOAL]
case unique_from
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
⊢ ∀ (Y : C ⥤ D), Nonempty (Unique (Y ⟶ F))
[PROOFSTEP]
intro G
[GOAL]
case unique_to
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ Nonempty (Unique (F ⟶ G))
[PROOFSTEP]
refine' ⟨⟨⟨_⟩, _⟩⟩
[GOAL]
case unique_from
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ Nonempty (Unique (G ⟶ F))
[PROOFSTEP]
refine' ⟨⟨⟨_⟩, _⟩⟩
[GOAL]
case unique_to.refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ F ⟶ G
[PROOFSTEP]
refine'
  { app := fun X => (hF _).to_ _
    naturality := _ }
[GOAL]
case unique_to.refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
    F.map f ≫ (fun X => IsZero.to_ (_ : IsZero (F.obj X)) (G.obj X)) Y =
      (fun X => IsZero.to_ (_ : IsZero (F.obj X)) (G.obj X)) X ≫ G.map f
[PROOFSTEP]
intros
[GOAL]
case unique_to.refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ F.map f✝ ≫ (fun X => IsZero.to_ (_ : IsZero (F.obj X)) (G.obj X)) Y✝ =
    (fun X => IsZero.to_ (_ : IsZero (F.obj X)) (G.obj X)) X✝ ≫ G.map f✝
[PROOFSTEP]
exact (hF _).eq_of_src _ _
[GOAL]
case unique_to.refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ ∀ (a : F ⟶ G), a = default
[PROOFSTEP]
intro f
[GOAL]
case unique_to.refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
f : F ⟶ G
⊢ f = default
[PROOFSTEP]
ext
[GOAL]
case unique_to.refine'_2.w.h
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
f : F ⟶ G
x✝ : C
⊢ NatTrans.app f x✝ = NatTrans.app default x✝
[PROOFSTEP]
apply (hF _).eq_of_src _ _
[GOAL]
case unique_from.refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ G ⟶ F
[PROOFSTEP]
refine'
  { app := fun X => (hF _).from_ _
    naturality := _ }
[GOAL]
case unique_from.refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
    G.map f ≫ (fun X => IsZero.from_ (_ : IsZero (F.obj X)) (G.obj X)) Y =
      (fun X => IsZero.from_ (_ : IsZero (F.obj X)) (G.obj X)) X ≫ F.map f
[PROOFSTEP]
intros
[GOAL]
case unique_from.refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ G.map f✝ ≫ (fun X => IsZero.from_ (_ : IsZero (F.obj X)) (G.obj X)) Y✝ =
    (fun X => IsZero.from_ (_ : IsZero (F.obj X)) (G.obj X)) X✝ ≫ F.map f✝
[PROOFSTEP]
exact (hF _).eq_of_tgt _ _
[GOAL]
case unique_from.refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ ∀ (a : G ⟶ F), a = default
[PROOFSTEP]
intro f
[GOAL]
case unique_from.refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
f : G ⟶ F
⊢ f = default
[PROOFSTEP]
ext
[GOAL]
case unique_from.refine'_2.w.h
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
f : G ⟶ F
x✝ : C
⊢ NatTrans.app f x✝ = NatTrans.app default x✝
[PROOFSTEP]
apply (hF _).eq_of_tgt _ _
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject D
F : C ⥤ D
hF : IsZero F
X : C
⊢ IsZero (F.obj X)
[PROOFSTEP]
let G : C ⥤ D := (CategoryTheory.Functor.const C).obj 0
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject D
F : C ⥤ D
hF : IsZero F
X : C
G : C ⥤ D := (Functor.const C).obj 0
⊢ IsZero (F.obj X)
[PROOFSTEP]
have hG : IsZero G := Functor.isZero _ fun _ => isZero_zero _
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject D
F : C ⥤ D
hF : IsZero F
X : C
G : C ⥤ D := (Functor.const C).obj 0
hG : IsZero G
⊢ IsZero (F.obj X)
[PROOFSTEP]
let e : F ≅ G := hF.iso hG
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject D
F : C ⥤ D
hF : IsZero F
X : C
G : C ⥤ D := (Functor.const C).obj 0
hG : IsZero G
e : F ≅ G := iso hF hG
⊢ IsZero (F.obj X)
[PROOFSTEP]
exact (isZero_zero _).of_iso (e.app X)
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject C
X : C
f g : X ≅ 0
⊢ f = g
[PROOFSTEP]
ext
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject C
X : C
f : 0 ⟶ X
Z✝ : C
g h : Z✝ ⟶ 0
x✝ : g ≫ f = h ≫ f
⊢ g = h
[PROOFSTEP]
ext
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject C
X : C
f : X ⟶ 0
Z✝ : C
g h : 0 ⟶ Z✝
x✝ : f ≫ g = f ≫ h
⊢ g = h
[PROOFSTEP]
ext
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject C
f : 0 ⟶ 0
⊢ IsIso f
[PROOFSTEP]
convert show IsIso (𝟙 (0 : C)) by infer_instance
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject C
f : 0 ⟶ 0
⊢ IsIso (𝟙 0)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject C
X : C
⊢ Mono (IsInitial.to zeroIsInitial X)
[PROOFSTEP]
infer_instance
