case intro
C : Type u₁
inst✝³ : Category C
X Y Z : C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
A B : C
h : A ⟶ ⊥.obj.left
⊢ h ≫ MonoOver.arrow ⊥ = 0
C : Type u₁
inst✝³ : Category C
X Y Z : C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
A B : C
f : A ⟶ B
⊢ Factors ⊥ f → f = 0
rintro ⟨h, rfl⟩
no goals
case intro
C : Type u₁
inst✝³ : Category C
X Y Z : C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
A B : C
h : A ⟶ ⊥.obj.left
⊢ h ≫ MonoOver.arrow ⊥ = 0
simp only [MonoOver.bot_arrow_eq_zero, Functor.id_obj, Functor.const_obj_obj,
  MonoOver.bot_left, comp_zero]
C : Type u₁
inst✝³ : Category C
X Y Z : C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
A B : C
⊢ Factors ⊥ 0
C : Type u₁
inst✝³ : Category C
X Y Z : C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
A B : C
f : A ⟶ B
⊢ f = 0 → Factors ⊥ f
rintro rfl
no goals
C : Type u₁
inst✝³ : Category C
X Y Z : C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
A B : C
⊢ Factors ⊥ 0
exact ⟨0, by simp⟩
no goals
C : Type u₁
inst✝³ : Category C
X Y Z : C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
A B : C
⊢ 0 ≫ MonoOver.arrow ⊥ = 0
simp