C : Type u
inst✝³ : Category C
D : Type u'
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasTerminal C
X : C
f : ⊤_ C ⟶ X
⊢ f = default
C : Type u
inst✝³ : Category C
D : Type u'
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasTerminal C
⊢ HasZeroObject C
refine' ⟨⟨⊤_ C, fun X => ⟨⟨⟨0⟩, fun f => _⟩⟩, fun X => ⟨⟨⟨0⟩, by aesop_cat⟩⟩⟩⟩
no goals
C : Type u
inst✝³ : Category C
D : Type u'
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasTerminal C
X : C
f : ⊤_ C ⟶ X
⊢ f = default
calc
  f = 𝟙 _ ≫ f := (Category.id_comp _).symm
  _ = 0 ≫ f := by congr!
  _ = 0 := zero_comp
no goals
C : Type u
inst✝³ : Category C
D : Type u'
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasTerminal C
X : C
⊢ ∀ (a : X ⟶ ⊤_ C), a = default
aesop_cat
no goals
C : Type u
inst✝³ : Category C
D : Type u'
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasTerminal C
X : C
f : ⊤_ C ⟶ X
⊢ 𝟙 (⊤_ C) ≫ f = 0 ≫ f
congr!